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.
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)))
Instances For
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)
:
theorem
AlgebraicGeometry.SurjectiveOnStalks.instOfIsOpenImmersion
{X Y : Scheme}
(f : Quiver.Hom X Y)
[IsOpenImmersion f]
:
theorem
AlgebraicGeometry.SurjectiveOnStalks.comp
{X Y Z : Scheme}
(f : Quiver.Hom X Y)
(g : Quiver.Hom Y Z)
[SurjectiveOnStalks f]
[SurjectiveOnStalks 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.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]
:
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)]
:
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)))
:
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.