Structures · Geometry
AlgebraicGeometry.IsPreimmersion
A morphism of schemes f : X ⟶ Y is a preimmersion if the underlying map of
topological spaces is an embedding and the induced morphisms of stalks are all surjective.
- Shape
- One type argument · adds isEmbedding
Extends1
Extended by2
Forgetful instances
Every AlgebraicGeometry.IsPreimmersion is also a
Provided automatically by
Concrete types that are instances7
- CategoryTheory.Limits.pullback
- AlgebraicGeometry.Scheme.Hom.fiber
- AlgebraicGeometry.Scheme.Opens.toScheme
- AlgebraicGeometry.Spec
- AlgebraicGeometry.Scheme.IdealSheafData.subscheme
- AlgebraicGeometry.Scheme.GlueData.glued
- AlgebraicGeometry.Scheme.IdealSheafData.glueDataObj
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- AlgebraicGeometry.Scheme.Hom.isEmbedding
- AlgebraicGeometry.IsClosedImmersion.of_isPreimmersion
- AlgebraicGeometry.IsPreimmersion.isEmbedding
- AlgebraicGeometry.IsPreimmersion.of_comp
- AlgebraicGeometry.instLocallyQuasiFiniteOfIsPreimmersion
- AlgebraicGeometry.IsPreimmersion.instMonoScheme
- AlgebraicGeometry.IsPreimmersion.instFstScheme
- AlgebraicGeometry.IsPreimmersion.toSurjectiveOnStalks
- AlgebraicGeometry.IsPreimmersion.comp_iff
- AlgebraicGeometry.IsPreimmersion.base_embedding
- AlgebraicGeometry.IsPreimmersion.instMorphismRestrict
- AlgebraicGeometry.IsPreimmersion.instSndScheme
- AlgebraicGeometry.IsPreimmersion.comp