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.

source

class AlgebraicGeometry.SurjectiveOnStalks {X Y : 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.

stalkMap_surjective (x : ↥X) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Instances

source

theorem AlgebraicGeometry.surjectiveOnStalks_iff {X Y : Scheme} (f : X ⟶ Y) :

SurjectiveOnStalks f ↔ ∀ (x : ↥X), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

source

theorem AlgebraicGeometry.Scheme.Hom.stalkMap_surjective {X Y : Scheme} (f : X ⟶ Y) [self : SurjectiveOnStalks f] (x : ↥X) :

Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (stalkMap f x))

Alias of AlgebraicGeometry.SurjectiveOnStalks.stalkMap_surjective.

source

@[deprecated AlgebraicGeometry.Scheme.Hom.stalkMap_surjective (since := "2026-01-20")]

theorem AlgebraicGeometry.SurjectiveOnStalks.surj_on_stalks {X Y : Scheme} (f : X ⟶ Y) [self : SurjectiveOnStalks f] (x : ↥X) :

Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Alias of AlgebraicGeometry.SurjectiveOnStalks.stalkMap_surjective.

source

@[instance 900]

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

SurjectiveOnStalks f

source

instance AlgebraicGeometry.SurjectiveOnStalks.instIsMultiplicativeScheme :

CategoryTheory.MorphismProperty.IsMultiplicative @SurjectiveOnStalks

source

instance AlgebraicGeometry.SurjectiveOnStalks.comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [SurjectiveOnStalks f] [SurjectiveOnStalks g] :

SurjectiveOnStalks (CategoryTheory.CategoryStruct.comp f g)

source

theorem AlgebraicGeometry.SurjectiveOnStalks.eq_stalkwise :

@SurjectiveOnStalks = stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) => Function.Surjective ⇑x

source

instance AlgebraicGeometry.SurjectiveOnStalks.instIsZariskiLocalAtTarget :

IsZariskiLocalAtTarget @SurjectiveOnStalks

source

instance AlgebraicGeometry.SurjectiveOnStalks.instIsZariskiLocalAtSource :

IsZariskiLocalAtSource @SurjectiveOnStalks

source

theorem AlgebraicGeometry.SurjectiveOnStalks.Spec_iff {R S : CommRingCat} {φ : R ⟶ S} :

SurjectiveOnStalks (Spec.map φ) ↔ (CommRingCat.Hom.hom φ).SurjectiveOnStalks

source

instance AlgebraicGeometry.SurjectiveOnStalks.instHasRingHomPropertySurjectiveOnStalks :

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

source

theorem AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine {X Y : Scheme} {f : X ⟶ Y} [IsAffine X] [IsAffine Y] :

SurjectiveOnStalks f ↔ (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤)).SurjectiveOnStalks

source

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

SurjectiveOnStalks f

source

instance AlgebraicGeometry.SurjectiveOnStalks.stableUnderBaseChange :

CategoryTheory.MorphismProperty.IsStableUnderBaseChange @SurjectiveOnStalks

source

theorem AlgebraicGeometry.SurjectiveOnStalks.mono_of_injective {X Y : Scheme} {f : X ⟶ Y} [SurjectiveOnStalks f] (hf : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f.base)) :

CategoryTheory.Mono f

source

theorem AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [SurjectiveOnStalks g] :

Topology.IsEmbedding fun (x : ↥(CategoryTheory.Limits.pullback f g)) => ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g).base) x, (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.

Documentation

Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Morphisms surjective on stalks #