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.

TODO

• Show that unramified is stable under base change.

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 (AlgHom.comp (Ideal.Quotient.mkₐ R I))

class Algebra.FormallyUnramified (R : Type u) [CommSemiring R] (A : Type u) [Semiring A] [Algebra R A] : Prop

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.

• comp_injective : ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B), I ^ 2 = ⊥ → Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R I))

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 : AlgHom.comp (Ideal.Quotient.mkₐ R I) g₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) 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 : RingHom.comp f ↑g₁ = RingHom.comp f ↑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 : AlgHom.comp f g₁ = AlgHom.comp f g₂) : g₁ = g₂

theorem Algebra.FormallyUnramified.of_equiv {R : Type u} [CommSemiring R] {A : Type u} {B : Type u} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Algebra.FormallyUnramified R A] (e : A ≃ₐ[R] B) : Algebra.FormallyUnramified R B

theorem Algebra.FormallyUnramified.comp (R : Type u) [CommSemiring R] (A : Type u) [CommSemiring A] [Algebra R A] (B : Type u) [Semiring B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [Algebra.FormallyUnramified R A] [Algebra.FormallyUnramified A B] : Algebra.FormallyUnramified R B

theorem Algebra.FormallyUnramified.of_comp (R : Type u) [CommSemiring R] (A : Type u) [CommSemiring A] [Algebra R A] (B : Type u) [Semiring B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [Algebra.FormallyUnramified R B] : Algebra.FormallyUnramified A B

instance Algebra.FormallyUnramified.base_change {R : Type u} [CommSemiring R] {A : Type u} [Semiring A] [Algebra R A] (B : Type u) [CommSemiring B] [Algebra R B] [Algebra.FormallyUnramified R A] : Algebra.FormallyUnramified B (TensorProduct R B A)

Equations

• ⋯ = ⋯

theorem Algebra.FormallyUnramified.of_isLocalization {R : Type u} {Rₘ : Type u} [CommRing R] [CommRing Rₘ] (M : Submonoid R) [Algebra R Rₘ] [IsLocalization M Rₘ] : Algebra.FormallyUnramified R Rₘ

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ₘ] : 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] : Algebra.FormallyUnramified Rₘ Sₘ

class Algebra.Unramified (R : Type u) [CommSemiring R] (A : Type u) [Semiring A] [Algebra R A] : Prop

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

• formallyUnramified : Algebra.FormallyUnramified R A
• finiteType : Algebra.FiniteType R A

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) : Algebra.Unramified R B

Being unramified is transported via algebra isomorphisms.

theorem Algebra.Unramified.of_isLocalization_Away {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R A] (r : R) [IsLocalization.Away r A] : Algebra.Unramified R A

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] : Algebra.Unramified R B

Unramified is stable under composition.