Documentation

Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale

Weakly étale morphisms #

A morphism of schemes is weakly étale if it is flat and its diagonal is flat. As the name suggests any étale morphism is weakly étale and every weakly étale morphism of finite presentation is étale.

Main definitions #

AlgebraicGeometry.WeaklyEtale: The class of weakly étale morphisms.

TODOs #

When weakly étale ring homomorphisms are in mathlib, show HasRingHomProperty WeaklyEtale RingHom.WeaklyEtale (@chrisflav).
Deduce from this that weakly étale morphisms of finite presentation are étale (@chrisflav).

class AlgebraicGeometry.WeaklyEtale {X Y : Scheme} (f : X ⟶ Y) :

A morphism is weakly étale if it is flat and the diagonal map is flat.

flat : Flat f
flat_diagonal : Flat (CategoryTheory.Limits.pullback.diagonal f)

Instances

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

WeaklyEtale f ↔ autoParam (Flat f) WeaklyEtale.flat._autoParam ∧ autoParam (Flat (CategoryTheory.Limits.pullback.diagonal f)) WeaklyEtale.flat_diagonal._autoParam

theorem AlgebraicGeometry.WeaklyEtale.weaklyEtale_eq_flat_inf_diagonal_flat :

@WeaklyEtale = @Flat ⊓ CategoryTheory.MorphismProperty.diagonal @Flat

@[instance 900]

instance AlgebraicGeometry.WeaklyEtale.instOfEtale {X Y : Scheme} (f : X ⟶ Y) [Etale f] :

Etale morphisms are weakly étale.

instance AlgebraicGeometry.WeaklyEtale.instRespectsIsoScheme :

CategoryTheory.MorphismProperty.RespectsIso @WeaklyEtale

instance AlgebraicGeometry.WeaklyEtale.instIsMultiplicativeScheme :

CategoryTheory.MorphismProperty.IsMultiplicative @WeaklyEtale

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

WeaklyEtale (CategoryTheory.CategoryStruct.comp f g)

instance AlgebraicGeometry.WeaklyEtale.instIsStableUnderBaseChangeScheme :

CategoryTheory.MorphismProperty.IsStableUnderBaseChange @WeaklyEtale

instance AlgebraicGeometry.WeaklyEtale.instIsZariskiLocalAtSource :

IsZariskiLocalAtSource @WeaklyEtale

instance AlgebraicGeometry.WeaklyEtale.instIsZariskiLocalAtTarget :

IsZariskiLocalAtTarget @WeaklyEtale

instance AlgebraicGeometry.WeaklyEtale.instFstScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [WeaklyEtale g] :

WeaklyEtale (CategoryTheory.Limits.pullback.fst f g)

instance AlgebraicGeometry.WeaklyEtale.instSndScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [WeaklyEtale f] :

WeaklyEtale (CategoryTheory.Limits.pullback.snd f g)

instance AlgebraicGeometry.WeaklyEtale.instMorphismRestrict {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) [WeaklyEtale f] :

WeaklyEtale (f ∣_ V)

instance AlgebraicGeometry.WeaklyEtale.instResLE {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens) (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [WeaklyEtale f] :

WeaklyEtale (Scheme.Hom.resLE f V U e)

instance AlgebraicGeometry.WeaklyEtale.instDiagonalScheme {X Y : Scheme} (f : X ⟶ Y) [WeaklyEtale f] :

WeaklyEtale (CategoryTheory.Limits.pullback.diagonal f)

instance AlgebraicGeometry.WeaklyEtale.instHasOfPostcompPropertyScheme :

CategoryTheory.MorphismProperty.HasOfPostcompProperty @WeaklyEtale @WeaklyEtale

Stacks Tag 0951

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