Unramified morphisms

An R-algebra A is formally unramified if Ω[A⁄R] is trivial. This is equivalent to the standard definition "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 v) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] : Algebra.FormallyUnramified R A ↔ Subsingleton (Ω[A⁄R])

class Algebra.FormallyUnramified (R : Type v) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] : Prop

An R-algebra A is formally unramified if Ω[A⁄R] is trivial.

This is equivalent to "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 Algebra.FormallyUnramified.iff_comp_injective.

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

• subsingleton_kaehlerDifferential : Subsingleton (Ω[A⁄R])

theorem Algebra.FormallyUnramified.subsingleton_kaehlerDifferential {R : Type v} : ∀ {inst : CommRing R} {A : Type u} {inst_1 : CommRing A} {inst_2 : Algebra R A} [self : Algebra.FormallyUnramified R A], Subsingleton (Ω[A⁄R])

theorem Algebra.FormallyUnramified.comp_injective {R : Type v} [CommRing R] {A : Type u} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] (I : Ideal B) [Algebra.FormallyUnramified R A] (hI : I ^ 2 = ⊥) : Function.Injective (Ideal.Quotient.mkₐ R I).comp

theorem Algebra.FormallyUnramified.iff_comp_injective {R : Type v} [CommRing R] {A : Type u} [CommRing 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

theorem Algebra.FormallyUnramified.lift_unique {R : Type v} [CommRing R] {A : Type u} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [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 v} [CommRing R] {A : Type u} [CommRing A] [Algebra R A] {B : Type w} [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 v} [CommRing R] {A : Type u} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] [Algebra.FormallyUnramified R A] {C : Type u_1} [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 v} [CommRing R] {A : Type u} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] [Algebra.FormallyUnramified R A] {C : Type u_1} [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 v} [CommRing R] {A : Type u} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] [Algebra.FormallyUnramified R A] {C : Type u_1} [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₂

instance Algebra.FormallyUnramified.inst {R : Type u_1} [CommRing R] : Algebra.FormallyUnramified R R

Equations

• ⋯ = ⋯

theorem Algebra.FormallyUnramified.of_equiv {R : Type u_1} [CommRing R] {A : Type u_2} {B : Type u_3} [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Algebra.FormallyUnramified R A] (e : A ≃ₐ[R] B) : Algebra.FormallyUnramified R B

theorem Algebra.FormallyUnramified.comp (R : Type u_1) [CommRing R] (A : Type u_2) [CommRing A] [Algebra R A] (B : Type u_3) [CommRing 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_1) [CommRing R] (A : Type u_2) [CommRing A] [Algebra R A] (B : Type u_3) [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [Algebra.FormallyUnramified R B] : Algebra.FormallyUnramified A B

theorem Algebra.FormallyUnramified.of_surjective {R : Type u_1} [CommRing R] {A : Type u_2} {B : Type u_3} [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Algebra.FormallyUnramified R A] (f : A →ₐ[R] B) (H : Function.Surjective ⇑f) : Algebra.FormallyUnramified R B

This holds in general for epimorphisms.

instance Algebra.FormallyUnramified.quotient {R : Type u_1} [CommRing R] {A : Type u_4} [CommRing A] [Algebra R A] [Algebra.FormallyUnramified R A] (I : Ideal A) : Algebra.FormallyUnramified R (A ⧸ I)

Equations

• ⋯ = ⋯

theorem Algebra.FormallyUnramified.iff_of_equiv {R : Type u_1} [CommRing R] {A : Type u_2} {B : Type u_3} [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] (e : A ≃ₐ[R] B) : Algebra.FormallyUnramified R A ↔ Algebra.FormallyUnramified R B

instance Algebra.FormallyUnramified.base_change {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] (B : Type u_3) [CommRing B] [Algebra R B] [Algebra.FormallyUnramified R A] : Algebra.FormallyUnramified B (TensorProduct R B A)

Equations

• ⋯ = ⋯

theorem Algebra.FormallyUnramified.of_isLocalization {R : Type u_1} {Rₘ : Type u_3} [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_1} {Rₘ : Type u_3} {Sₘ : Type u_4} [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_1} {S : Type u_2} {Rₘ : Type u_3} {Sₘ : Type u_4} [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_1) [CommRing R] (A : Type u_2) [CommRing A] [Algebra R A] : Prop

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.

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

theorem Algebra.Unramified.formallyUnramified {R : Type u_1} : ∀ {inst : CommRing R} {A : Type u_2} {inst_1 : CommRing A} {inst_2 : Algebra R A} [self : Algebra.Unramified R A], Algebra.FormallyUnramified R A

theorem Algebra.Unramified.finiteType {R : Type u_1} : ∀ {inst : CommRing R} {A : Type u_2} {inst_1 : CommRing A} {inst_2 : Algebra R A} [self : Algebra.Unramified R A], Algebra.FiniteType R A

theorem Algebra.Unramified.of_equiv {R : Type u_1} [CommRing R] {A : Type u_2} {B : Type u_3} [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_1} [CommRing R] {A : Type u_2} [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_1) [CommRing R] (A : Type u_2) (B : Type u_3) [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.

instance Algebra.Unramified.baseChange (R : Type u_1) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Algebra.Unramified R A] : Algebra.Unramified B (TensorProduct R B A)

Unramified is stable under base change.

Equations

• ⋯ = ⋯