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.

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.

• surj_on_stalks (x : ↑↑X.toPresheafedSpace) : Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.stalkMap f x).hom

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).hom

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).hom

@[instance 900]

instance AlgebraicGeometry.SurjectiveOnStalks.instOfIsOpenImmersion {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] : AlgebraicGeometry.SurjectiveOnStalks f

instance AlgebraicGeometry.SurjectiveOnStalks.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.SurjectiveOnStalks

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)

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

instance AlgebraicGeometry.SurjectiveOnStalks.instIsLocalAtTarget : AlgebraicGeometry.IsLocalAtTarget @AlgebraicGeometry.SurjectiveOnStalks

instance AlgebraicGeometry.SurjectiveOnStalks.instIsLocalAtSource : AlgebraicGeometry.IsLocalAtSource @AlgebraicGeometry.SurjectiveOnStalks

theorem AlgebraicGeometry.SurjectiveOnStalks.Spec_iff {R S : CommRingCat} {φ : R ⟶ S} : AlgebraicGeometry.SurjectiveOnStalks (AlgebraicGeometry.Spec.map φ) ↔ φ.hom.SurjectiveOnStalks

instance AlgebraicGeometry.SurjectiveOnStalks.instHasRingHomPropertySurjectiveOnStalks : AlgebraicGeometry.HasRingHomProperty @AlgebraicGeometry.SurjectiveOnStalks fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.SurjectiveOnStalks

theorem AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] : AlgebraicGeometry.SurjectiveOnStalks f ↔ (AlgebraicGeometry.Scheme.Hom.app f ⊤).hom.SurjectiveOnStalks

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

instance AlgebraicGeometry.SurjectiveOnStalks.stableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.SurjectiveOnStalks

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.