Structures · Geometry
AlgebraicGeometry.Scheme.IsGermInjectiveAt
The germ map at x is injective if there exists some affine U ∋ x
such that the map Γ(X, U) ⟶ X_x is injective
- Defined in
- Mathlib.AlgebraicGeometry.SpreadingOut
- Shape
- 2 explicit arguments · adds cond
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by14
- AlgebraicGeometry.Scheme.exists_le_and_germ_injective
- AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk
- AlgebraicGeometry.spread_out_of_isGermInjective'
- AlgebraicGeometry.Scheme.IsGermInjectiveAt.cond
- AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_ofFromSpecStalk
- AlgebraicGeometry.spread_out_unique_of_isGermInjective'
- AlgebraicGeometry.spread_out_of_isGermInjective
- AlgebraicGeometry.spread_out_unique_of_isGermInjective
- AlgebraicGeometry.Scheme.PartialMap.equiv_of_fromSpecStalkOfMem_eq
- AlgebraicGeometry.exists_lift_of_germInjective
- AlgebraicGeometry.Scheme.PartialMap.mem_domain_ofFromSpecStalk
- AlgebraicGeometry.instIsGermInjectiveAtCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfIsOpenImmersion
- AlgebraicGeometry.Scheme.exists_germ_injective
- AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk_comp
Ancestors0
No ancestors.