Mathlib Map

Structures · Geometry

AlgebraicGeometry.IsClosedImmersion

A morphism of schemes X ⟶ Y is a closed immersion if the underlying topological map is a closed embedding and the induced stalk maps are surjective.

Defined in
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Shape
One type argument · adds isClosedEmbedding
Open in Mathlib docs

Extends1

Extended by3

Forgetful instances

Every AlgebraicGeometry.IsClosedImmersion is also a

Provided automatically by

Concrete types that are instances7

  • CategoryTheory.Limits.pullback
  • AlgebraicGeometry.Scheme.Opens.toScheme
  • AlgebraicGeometry.Spec
  • CategoryTheory.Over.left
  • AlgebraicGeometry.Scheme.IdealSheafData.subscheme
  • CategoryTheory.Limits.equalizer
  • AlgebraicGeometry.Scheme.irreducibleComponent

How is a type an instance?

Loading the hierarchy index…

Assumed by33

Ancestors13