Documentation

Mathlib.RingTheory.Unramified.Basic

Unramified morphisms #

An R-algebra A is formally unramified if for every R-algebra, every square-zero ideal I : Ideal B and f : A →ₐ[R] B ⧸ I, there exists at most one lift A →ₐ[R] B. It is unramified if it is formally unramified and of finite type.

Note that there are multiple definitions in the literature. The definition we give is equivalent to the one in the Stacks Project https://stacks.math.columbia.edu/tag/00US. Note that in EGA unramified is defined as formally unramified and of finite presentation.

We show that the property extends onto nilpotent ideals, and that it is stable under R-algebra homomorphisms and compositions.

We show that unramified is stable under algebra isomorphisms, composition and localization at an element.

theorem Algebra.formallyUnramified_iff (R : Type u) [CommSemiring R] (A : Type u) [Semiring A] [Algebra R A] :
Algebra.FormallyUnramified R A ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B), I ^ 2 = Function.Injective (Ideal.Quotient.mkₐ R I).comp

An R-algebra A is formally unramified if for every R-algebra, every square-zero ideal I : Ideal B and f : A →ₐ[R] B ⧸ I, there exists at most one lift A →ₐ[R] B.

See https://stacks.math.columbia.edu/tag/00UM.

Instances
    theorem Algebra.FormallyUnramified.lift_unique {R : Type u} [CommSemiring R] {A : Type u} [Semiring A] [Algebra R A] {B : Type u} [CommRing B] [_RB : Algebra R B] [Algebra.FormallyUnramified R A] (I : Ideal B) (hI : IsNilpotent I) (g₁ : A →ₐ[R] B) (g₂ : A →ₐ[R] B) (h : (Ideal.Quotient.mkₐ R I).comp g₁ = (Ideal.Quotient.mkₐ R I).comp g₂) :
    g₁ = g₂
    theorem Algebra.FormallyUnramified.ext {R : Type u} [CommSemiring R] {A : Type u} [Semiring A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B] (I : Ideal B) [Algebra.FormallyUnramified R A] (hI : IsNilpotent I) {g₁ : A →ₐ[R] B} {g₂ : A →ₐ[R] B} (H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)) :
    g₁ = g₂
    theorem Algebra.FormallyUnramified.lift_unique_of_ringHom {R : Type u} [CommSemiring R] {A : Type u} [Semiring A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B] [Algebra.FormallyUnramified R A] {C : Type u} [CommRing C] (f : B →+* C) (hf : IsNilpotent (RingHom.ker f)) (g₁ : A →ₐ[R] B) (g₂ : A →ₐ[R] B) (h : f.comp g₁ = f.comp g₂) :
    g₁ = g₂
    theorem Algebra.FormallyUnramified.ext' {R : Type u} [CommSemiring R] {A : Type u} [Semiring A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B] [Algebra.FormallyUnramified R A] {C : Type u} [CommRing C] (f : B →+* C) (hf : IsNilpotent (RingHom.ker f)) (g₁ : A →ₐ[R] B) (g₂ : A →ₐ[R] B) (h : ∀ (x : A), f (g₁ x) = f (g₂ x)) :
    g₁ = g₂
    theorem Algebra.FormallyUnramified.lift_unique' {R : Type u} [CommSemiring R] {A : Type u} [Semiring A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B] [Algebra.FormallyUnramified R A] {C : Type u} [CommRing C] [Algebra R C] (f : B →ₐ[R] C) (hf : IsNilpotent (RingHom.ker f)) (g₁ : A →ₐ[R] B) (g₂ : A →ₐ[R] B) (h : f.comp g₁ = f.comp g₂) :
    g₁ = g₂

    This holds in general for epimorphisms.

    theorem Algebra.FormallyUnramified.localization_base {R : Type u} {Rₘ : Type u} {Sₘ : Type u} [CommRing R] [CommRing Rₘ] [CommRing Sₘ] (M : Submonoid R) [Algebra R Sₘ] [Algebra R Rₘ] [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ] [Algebra.FormallyUnramified R Sₘ] :

    This actually does not need the localization instance, and is stated here again for consistency. See Algebra.FormallyUnramified.of_comp instead.

    The intended use is for copying proofs between Formally{Unramified, Smooth, Etale} without the need to change anything (including removing redundant arguments).

    theorem Algebra.FormallyUnramified.localization_map {R : Type u} {S : Type u} {Rₘ : Type u} {Sₘ : Type u} [CommRing R] [CommRing S] [CommRing Rₘ] [CommRing Sₘ] (M : Submonoid R) [Algebra R S] [Algebra R Sₘ] [Algebra S Sₘ] [Algebra R Rₘ] [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ] [Algebra.FormallyUnramified R S] :
    class Algebra.Unramified (R : Type u) [CommSemiring R] (A : Type u) [Semiring A] [Algebra R A] :

    An R-algebra A is unramified if it is formally unramified and of finite type.

    Note that the Stacks project has a different definition of unramified, and tag https://stacks.math.columbia.edu/tag/00UU shows that their definition is the same as this one.

    Instances
      theorem Algebra.Unramified.of_equiv {R : Type u} [CommRing R] {A : Type u} {B : Type u} [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Algebra.Unramified R A] (e : A ≃ₐ[R] B) :

      Being unramified is transported via algebra isomorphisms.

      Localization at an element is unramified.

      theorem Algebra.Unramified.comp (R : Type u) [CommRing R] (A : Type u) (B : Type u) [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [Algebra.Unramified R A] [Algebra.Unramified A B] :

      Unramified is stable under composition.

      Unramified is stable under base change.

      Equations
      • =