Documentation

Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Morphisms surjective on stalks #

We define the classe of morphisms between schemes that are surjective on stalks. We show that this class is stable under composition and base change.

We also show that (AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback) if Y ⟶ S is surjective on stalks, then for every X ⟶ S, X ×ₛ Y is a subset of X × Y (cartesian product as topological spaces) with the induced topology.

source
class AlgebraicGeometry.SurjectiveOnStalks {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
Prop

The class of morphisms f : X ⟶ Y between schemes such that 𝒪_{Y, f x} ⟶ 𝒪_{X, x} is surjective for all x : X.

Instances
    source
    theorem AlgebraicGeometry.surjectiveOnStalks_iff {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
    AlgebraicGeometry.SurjectiveOnStalks f ↔ ∀ (x : ↑↑X.toPresheafedSpace), Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.stalkMap f x)
    source
    theorem AlgebraicGeometry.Scheme.Hom.stalkMap_surjective {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [AlgebraicGeometry.SurjectiveOnStalks f] (x : ↑↑X.toPresheafedSpace) :
    Function.Surjective ⇑(f.stalkMap x)
    source
    @[instance 900]
    instance AlgebraicGeometry.SurjectiveOnStalks.instOfIsOpenImmersion {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] :
    AlgebraicGeometry.SurjectiveOnStalks f
    Equations
    • ⋯ = ⋯
    source
    instance AlgebraicGeometry.SurjectiveOnStalks.instIsMultiplicativeScheme :
    CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.SurjectiveOnStalks
    Equations
    source
    instance AlgebraicGeometry.SurjectiveOnStalks.comp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.SurjectiveOnStalks f] [AlgebraicGeometry.SurjectiveOnStalks g] :
    AlgebraicGeometry.SurjectiveOnStalks (CategoryTheory.CategoryStruct.comp f g)
    Equations
    • ⋯ = ⋯
    source
    theorem AlgebraicGeometry.SurjectiveOnStalks.eq_stalkwise :
    @AlgebraicGeometry.SurjectiveOnStalks = AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) => Function.Surjective ⇑x
    source
    instance AlgebraicGeometry.SurjectiveOnStalks.instIsLocalAtTarget :
    AlgebraicGeometry.IsLocalAtTarget @AlgebraicGeometry.SurjectiveOnStalks
    Equations
    source
    instance AlgebraicGeometry.SurjectiveOnStalks.instIsLocalAtSource :
    AlgebraicGeometry.IsLocalAtSource @AlgebraicGeometry.SurjectiveOnStalks
    Equations
    source
    theorem AlgebraicGeometry.SurjectiveOnStalks.Spec_iff {R S : CommRingCat} {φ : R ⟶ S} :
    AlgebraicGeometry.SurjectiveOnStalks (AlgebraicGeometry.Spec.map φ) ↔ RingHom.SurjectiveOnStalks φ
    source
    instance AlgebraicGeometry.SurjectiveOnStalks.instHasRingHomPropertySurjectiveOnStalks :
    AlgebraicGeometry.HasRingHomProperty @AlgebraicGeometry.SurjectiveOnStalks fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.SurjectiveOnStalks
    Equations
    source
    theorem AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] :
    AlgebraicGeometry.SurjectiveOnStalks f ↔ RingHom.SurjectiveOnStalks (AlgebraicGeometry.Scheme.Hom.app f ⊤)
    source
    theorem AlgebraicGeometry.SurjectiveOnStalks.of_comp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.SurjectiveOnStalks (CategoryTheory.CategoryStruct.comp f g)] :
    AlgebraicGeometry.SurjectiveOnStalks f
    source
    instance AlgebraicGeometry.SurjectiveOnStalks.stableUnderBaseChange :
    CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.SurjectiveOnStalks
    Equations
    source
    theorem AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.SurjectiveOnStalks g] :
    Topology.IsEmbedding fun (x : ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace) => ((CategoryTheory.Limits.pullback.fst f g).base x, (CategoryTheory.Limits.pullback.snd f g).base x)

    If Y ⟶ S is surjective on stalks, then for every X ⟶ S, X ×ₛ Y is a subset of X × Y (cartesian product as topological spaces) with the induced topology.