Morphisms surjective on stalks

We define the class 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.

structure AlgebraicGeometry.SurjectiveOnStalks {X Y : Scheme} (f : Quiver.Hom 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.carrier.carrier) : Function.Surjective (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap f x)))

theorem AlgebraicGeometry.surjectiveOnStalks_iff {X Y : Scheme} (f : Quiver.Hom X Y) : Iff (SurjectiveOnStalks f) (∀ (x : X.carrier.carrier), Function.Surjective (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap f x))))

theorem AlgebraicGeometry.Scheme.Hom.stalkMap_surjective {X Y : Scheme} (f : X.Hom Y) [SurjectiveOnStalks f] (x : X.carrier.carrier) : Function.Surjective (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (f.stalkMap x)))

theorem AlgebraicGeometry.SurjectiveOnStalks.instOfIsOpenImmersion {X Y : Scheme} (f : Quiver.Hom X Y) [IsOpenImmersion f] : SurjectiveOnStalks f

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

theorem AlgebraicGeometry.SurjectiveOnStalks.comp {X Y Z : Scheme} (f : Quiver.Hom X Y) (g : Quiver.Hom Y Z) [SurjectiveOnStalks f] [SurjectiveOnStalks g] : SurjectiveOnStalks (CategoryTheory.CategoryStruct.comp f g)

theorem AlgebraicGeometry.SurjectiveOnStalks.eq_stalkwise : Eq (@SurjectiveOnStalks) (stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : RingHom R S) => Function.Surjective (DFunLike.coe x))

theorem AlgebraicGeometry.SurjectiveOnStalks.instIsLocalAtTarget : IsLocalAtTarget @SurjectiveOnStalks

theorem AlgebraicGeometry.SurjectiveOnStalks.instIsLocalAtSource : IsLocalAtSource @SurjectiveOnStalks

theorem AlgebraicGeometry.SurjectiveOnStalks.Spec_iff {R S : CommRingCat} {φ : Quiver.Hom R S} : Iff (SurjectiveOnStalks (Spec.map φ)) (CommRingCat.Hom.hom φ).SurjectiveOnStalks

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

theorem AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine {X Y : Scheme} {f : Quiver.Hom X Y} [IsAffine X] [IsAffine Y] : Iff (SurjectiveOnStalks f) (CommRingCat.Hom.hom (Scheme.Hom.app f Top.top)).SurjectiveOnStalks

theorem AlgebraicGeometry.SurjectiveOnStalks.of_comp {X Y Z : Scheme} (f : Quiver.Hom X Y) (g : Quiver.Hom Y Z) [SurjectiveOnStalks (CategoryTheory.CategoryStruct.comp f g)] : SurjectiveOnStalks f

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

theorem AlgebraicGeometry.SurjectiveOnStalks.mono_of_injective {X Y : Scheme} {f : Quiver.Hom X Y} [SurjectiveOnStalks f] (hf : Function.Injective (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f.base))) : CategoryTheory.Mono f

theorem AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback {X Y S : Scheme} (f : Quiver.Hom X S) (g : Quiver.Hom Y S) [SurjectiveOnStalks g] : Topology.IsEmbedding fun (x : (CategoryTheory.Limits.pullback f g).carrier.carrier) => { fst := DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g).base) x, snd := DFunLike.coe (CategoryTheory.ConcreteCategory.hom (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.