Structures · Geometry
AlgebraicGeometry.IsImmersion
A morphism of schemes f : X ⟶ Y is an immersion if
1. the underlying map of topological spaces is an embedding
2. the range of the map is locally closed
3. the induced morphisms of stalks are all surjective.
- Shape
- One type argument · adds isLocallyClosed_range
Extends1
Extended by2
Forgetful instances
Every AlgebraicGeometry.IsImmersion is also a
Provided automatically by
Concrete types that are instances3
- CategoryTheory.Limits.pullback
- AlgebraicGeometry.Scheme.Opens.toScheme
- CategoryTheory.Limits.equalizer
How is a type an instance?
Loading the hierarchy index…
Assumed by27
- AlgebraicGeometry.Scheme.Hom.coborderRange
- AlgebraicGeometry.Scheme.Hom.liftCoborder
- AlgebraicGeometry.Scheme.Hom.liftCoborder_ι
- AlgebraicGeometry.Scheme.Hom.liftCoborder_preimage
- AlgebraicGeometry.IsImmersion.of_comp
- AlgebraicGeometry.isIso_of_comp_eq_sigmaSpec
- AlgebraicGeometry.liftCoborder_app
- AlgebraicGeometry.IsImmersion.isLocallyClosed_range
- AlgebraicGeometry.IsLocallyArtinian.of_isImmersion
- AlgebraicGeometry.IsImmersion.comp
- AlgebraicGeometry.IsImmersion.isPullback_toImage_liftCoborder
- AlgebraicGeometry.Scheme.Hom.liftCoborder_ι_assoc
- AlgebraicGeometry.IsImmersion.instFstScheme
- AlgebraicGeometry.IsImmersion.comp_iff
- AlgebraicGeometry.IsImmersion.instIsOpenImmersionToImageOfQuasiCompact
- AlgebraicGeometry.IsImmersion.toIsPreimmersion
- AlgebraicGeometry.Scheme.IsQuasiAffine.of_isImmersion
- AlgebraicGeometry.IsImmersion.instResLE
- AlgebraicGeometry.instIsClosedImmersionLiftCoborder
- AlgebraicGeometry.IsImmersion.instLocallyOfFiniteType
- AlgebraicGeometry.IsImmersion.instToImage
- AlgebraicGeometry.instIsDominantιCoborderRange
- AlgebraicGeometry.Scheme.Hom.isLocallyClosed_range
- AlgebraicGeometry.IsImmersion.instSndScheme
- AlgebraicGeometry.instLocallyQuasiFiniteOfIsImmersion
- AlgebraicGeometry.Scheme.Hom.coborderRange.congr_simp
- AlgebraicGeometry.IsImmersion.instMorphismRestrict