Extension of algebras

Main definition

• Algebra.Extension: An extension of an R-algebra S is an R algebra P together with a surjection P →ₐ[R] R.

• Algebra.Extension.Hom: Given a commuting square

  R --→ P -→ S
  |          |
  ↓          ↓
  R' -→ P' → S
  

  A hom between P and P' is a ring homomorphism that makes the two squares commute.

• Algebra.Extension.Cotangent: The cotangent space wrt an extension P → S by I, i.e. the space I/I².

structure Algebra.Extension (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Type (max (max u v) (w + 1))

An extension of an R-algebra S is an R algebra P together with a surjection P →ₐ[R] S. Also see Algebra.Extension.ofSurjective.

• Ring : Type w

  The underlying algebra of an extension.

• commRing : CommRing self.Ring
• algebra₁ : Algebra R self.Ring
• algebra₂ : Algebra self.Ring S
• isScalarTower : IsScalarTower R self.Ring S
• σ : S → self.Ring

  A chosen (set-theoretic) section of an extension.

• algebraMap_σ (x : S) : (algebraMap self.Ring S) (self.σ x) = x

noncomputable instance Algebra.Extension.instRingOfIsScalarTower {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) {R₀ : Type u_1} [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] : Algebra R₀ P.Ring

instance Algebra.Extension.instIsScalarTowerRing {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) {R₀ : Type u_1} [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] : IsScalarTower R₀ R P.Ring

instance Algebra.Extension.instIsScalarTowerRing_1 {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) {R₀ : Type u_1} [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] {R₁ : Type u_2} [CommRing R₁] [Algebra R₁ R] [Algebra R₁ S] [IsScalarTower R₁ R S] [Algebra R₀ R₁] [IsScalarTower R₀ R₁ R] : IsScalarTower R₀ R₁ P.Ring

instance Algebra.Extension.instIsScalarTowerRing_2 {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) {R₀ : Type u_1} [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] : IsScalarTower R₀ P.Ring S

@[simp]

theorem Algebra.Extension.σ_smul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) (x y : S) : P.σ x • y = x * y

theorem Algebra.Extension.σ_injective {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : Function.Injective P.σ

theorem Algebra.Extension.algebraMap_surjective {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : Function.Surjective ⇑(algebraMap P.Ring S)

noncomputable def Algebra.Extension.ofSurjective {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Type w} [CommRing P] [Algebra R P] (f : P →ₐ[R] S) (h : Function.Surjective ⇑f) : Extension R S

Construct Extension from a surjective algebra homomorphism.

theorem Algebra.Extension.ofSurjective_Ring {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Type w} [CommRing P] [Algebra R P] (f : P →ₐ[R] S) (h : Function.Surjective ⇑f) : (ofSurjective f h).Ring = P

theorem Algebra.Extension.ofSurjective_σ {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Type w} [CommRing P] [Algebra R P] (f : P →ₐ[R] S) (h : Function.Surjective ⇑f) (x : S) : (ofSurjective f h).σ x = ⋯.choose

noncomputable def Algebra.Extension.self (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Extension R S

The trivial extension of S.

theorem Algebra.Extension.self_Ring (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : (self R S).Ring = S

theorem Algebra.Extension.self_σ (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (a : S) : (self R S).σ a = _root_.id a

@[reducible, inline]

abbrev Algebra.Extension.ker {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : Ideal P.Ring

The kernel of an extension.

noncomputable def Algebra.Extension.localization {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (M : Submonoid S) {S' : Type u_1} [CommRing S'] [Algebra S S'] [IsLocalization M S'] [Algebra R S'] [IsScalarTower R S S'] (P : Extension R S) : Extension R S'

An R-extension P → S gives an R-extension Pₘ → Sₘ. Note that this is different from baseChange as the base does not change.

noncomputable def Algebra.Extension.baseChange {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] (P : Extension R S) : Extension T (TensorProduct R T S)

The base change of an R-extension of S to T gives a T-extension of T ⊗[R] S.

structure Algebra.Extension.Hom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] (P' : Extension R' S') [Algebra R R'] [Algebra S S'] : Type (max u_3 w)

Given a commuting square

R --→ P -→ S
|          |
↓          ↓
R' -→ P' → S

A hom between P and P' is a ring homomorphism that makes the two squares commute.

• toRingHom : P.Ring →+* P'.Ring

  The underlying ring homomorphism of a hom between extensions.

• toRingHom_algebraMap (x : R) : self.toRingHom ((algebraMap R P.Ring) x) = (algebraMap R' P'.Ring) ((algebraMap R R') x)
• algebraMap_toRingHom (x : P.Ring) : (algebraMap P'.Ring S') (self.toRingHom x) = (algebraMap S S') ((algebraMap P.Ring S) x)

theorem Algebra.Extension.Hom.ext {R : Type u} {S : Type v} {inst✝ : CommRing R} {inst✝¹ : CommRing S} {inst✝² : Algebra R S} {P : Extension R S} {R' : Type u_1} {S' : Type u_2} {inst✝³ : CommRing R'} {inst✝⁴ : CommRing S'} {inst✝⁵ : Algebra R' S'} {P' : Extension R' S'} {inst✝⁶ : Algebra R R'} {inst✝⁷ : Algebra S S'} {x y : P.Hom P'} (toRingHom : x.toRingHom = y.toRingHom) : x = y

theorem Algebra.Extension.Hom.ext_iff {R : Type u} {S : Type v} {inst✝ : CommRing R} {inst✝¹ : CommRing S} {inst✝² : Algebra R S} {P : Extension R S} {R' : Type u_1} {S' : Type u_2} {inst✝³ : CommRing R'} {inst✝⁴ : CommRing S'} {inst✝⁵ : Algebra R' S'} {P' : Extension R' S'} {inst✝⁶ : Algebra R R'} {inst✝⁷ : Algebra S S'} {x y : P.Hom P'} : x = y ↔ x.toRingHom = y.toRingHom

noncomputable def Algebra.Extension.Hom.toAlgHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') : P.Ring →ₐ[R] P'.Ring

A hom between extensions as an algebra homomorphism.

@[simp]

theorem Algebra.Extension.Hom.toAlgHom_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R' : Type u_2} {S' : Type u_1} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') (x : P.Ring) : f.toAlgHom x = f.toRingHom x

noncomputable def Algebra.Extension.Hom.id {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : P.Hom P

The identity hom.

@[simp]

theorem Algebra.Extension.Hom.id_toRingHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : (Hom.id P).toRingHom = RingHom.id P.Ring

@[simp]

theorem Algebra.Extension.Hom.toAlgHom_id {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : (Hom.id P).toAlgHom = AlgHom.id R P.Ring

noncomputable def Algebra.Extension.Hom.comp {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Extension R' S'} {R'' : Type u_4} {S'' : Type u_5} [CommRing R''] [CommRing S''] [Algebra R'' S''] {P'' : Extension R'' S''} [Algebra R R'] [Algebra R' R''] [Algebra R R''] [Algebra S S'] [Algebra S' S''] [Algebra S S''] [IsScalarTower R R' R''] [IsScalarTower S S' S''] (f : P'.Hom P'') (g : P.Hom P') : P.Hom P''

The composition of two homs.

@[simp]

theorem Algebra.Extension.Hom.comp_toRingHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Extension R' S'} {R'' : Type u_4} {S'' : Type u_5} [CommRing R''] [CommRing S''] [Algebra R'' S''] {P'' : Extension R'' S''} [Algebra R R'] [Algebra R' R''] [Algebra R R''] [Algebra S S'] [Algebra S' S''] [Algebra S S''] [IsScalarTower R R' R''] [IsScalarTower S S' S''] (f : P'.Hom P'') (g : P.Hom P') : (f.comp g).toRingHom = f.toRingHom.comp g.toRingHom

@[simp]

theorem Algebra.Extension.Hom.comp_id {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Extension R' S'} [Algebra R R'] [Algebra S S'] (f : P.Hom P') : f.comp (Hom.id P) = f

@[simp]

theorem Algebra.Extension.Hom.id_comp {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Extension R' S'} [Algebra R R'] [Algebra S S'] (f : P.Hom P') : (Hom.id P').comp f = f

def Algebra.Extension.Hom.mapKer {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Extension R' S'} [Algebra R R'] [Algebra S S'] (f : P.Hom P') [alg : Algebra P.Ring P'.Ring] (halg : algebraMap P.Ring P'.Ring = f.toRingHom) : ↥P.ker →ₗ[P.Ring] ↥P'.ker

A map between extensions induce a map between kernels.

@[simp]

theorem Algebra.Extension.Hom.mapKer_apply_coe {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Extension R' S'} [Algebra R R'] [Algebra S S'] (f : P.Hom P') [alg : Algebra P.Ring P'.Ring] (halg : algebraMap P.Ring P'.Ring = f.toRingHom) (x : ↥P.ker) : ↑((f.mapKer halg) x) = f.toRingHom ↑x

noncomputable def Algebra.Extension.infinitesimal {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : Extension R S

Given an R-algebra extension 0 → I → P → S → 0 of S, the infinitesimal extension associated to it is 0 → I/I² → P/I² → S → 0.

noncomputable def Algebra.Extension.toInfinitesimal {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : P.Hom P.infinitesimal

The canonical map P → P/I² as maps between extensions.

theorem Algebra.Extension.ker_infinitesimal {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : P.infinitesimal.ker = P.ker.cotangentIdeal

def Algebra.Extension.Cotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : Type w

The cotangent space of an extension. This is a type synonym so that P.Ring can act on it through the action of S without creating a diamond.

noncomputable instance Algebra.Extension.instAddCommGroupCotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : AddCommGroup P.Cotangent

def Algebra.Extension.Cotangent.of {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} (x : P.ker.Cotangent) : P.Cotangent

The identity map P.ker.Cotangent → P.Cotangent into the type synonym.

def Algebra.Extension.Cotangent.val {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} (x : P.Cotangent) : P.ker.Cotangent

The identity map P.Cotangent → P.ker.Cotangent from the type synonym.

theorem Algebra.Extension.Cotangent.ext {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {x y : P.Cotangent} (e : x.val = y.val) : x = y

theorem Algebra.Extension.Cotangent.ext_iff {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {x y : P.Cotangent} : x = y ↔ x.val = y.val

@[simp]

theorem Algebra.Extension.Cotangent.val_add {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} (x y : P.Cotangent) : (x + y).val = x.val + y.val

@[simp]

theorem Algebra.Extension.Cotangent.val_zero {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} : val 0 = 0

@[simp]

theorem Algebra.Extension.Cotangent.of_add {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} (w z : P.ker.Cotangent) : of (w + z) = of w + of z

@[simp]

theorem Algebra.Extension.Cotangent.of_zero {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} : of 0 = 0

@[simp]

theorem Algebra.Extension.Cotangent.of_val {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} (x : P.Cotangent) : of x.val = x

@[simp]

theorem Algebra.Extension.Cotangent.val_of {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} (w : P.ker.Cotangent) : (of w).val = w

@[simp]

theorem Algebra.Extension.Cotangent.val_sub {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} (x y : P.Cotangent) : (x - y).val = x.val - y.val

theorem Algebra.Extension.Cotangent.smul_eq_zero_of_mem {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} (p : P.Ring) (hp : p ∈ P.ker) (m : P.ker.Cotangent) : p • m = 0

noncomputable instance Algebra.Extension.Cotangent.module {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} : Module S P.Cotangent

noncomputable instance Algebra.Extension.instModuleCotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R₀ : Type u_1} [CommRing R₀] [Algebra R₀ S] : Module R₀ P.Cotangent

instance Algebra.Extension.instIsScalarTowerCotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R₁ : Type u_1} {R₂ : Type u_2} [CommRing R₁] [CommRing R₂] [Algebra R₁ S] [Algebra R₂ S] [Algebra R₁ R₂] [IsScalarTower R₁ R₂ S] : IsScalarTower R₁ R₂ P.Cotangent

theorem Algebra.Extension.Cotangent.val_smul''' {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R₀ : Type u_1} [CommRing R₀] [Algebra R₀ S] (r : R₀) (x : P.Cotangent) : (r • x).val = P.σ ((algebraMap R₀ S) r) • x.val

The action of R₀ on P.Cotangent for an extension P → S, if S is an R₀ algebra.

@[simp]

theorem Algebra.Extension.Cotangent.val_smul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} (r : S) (x : P.Cotangent) : (r • x).val = P.σ r • x.val

The action of S on P.Cotangent for an extension P → S.

@[simp]

theorem Algebra.Extension.Cotangent.val_smul' {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} (r : P.Ring) (x : P.Cotangent) : (r • x).val = r • x.val

The action of P on P.Cotangent for an extension P → S.

@[simp]

theorem Algebra.Extension.Cotangent.val_smul'' {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} (r : R) (x : P.Cotangent) : (r • x).val = r • x.val

The action of R on P.Cotangent for an R-extension P → S.

noncomputable def Algebra.Extension.Cotangent.mk {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} : ↥P.ker →ₗ[P.Ring] P.Cotangent

The quotient map from the kernel of P → S onto the cotangent space.

@[simp]

theorem Algebra.Extension.Cotangent.val_mk {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} (x : ↥P.ker) : (mk x).val = P.ker.toCotangent x

theorem Algebra.Extension.Cotangent.mk_surjective {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} : Function.Surjective ⇑mk

theorem Algebra.Extension.Cotangent.mk_eq_zero_iff {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} (x : ↥P.ker) : mk x = 0 ↔ ↑x ∈ P.ker ^ 2

noncomputable def Algebra.Extension.Cotangent.map {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') : P.Cotangent →ₗ[S] P'.Cotangent

A hom between two extensions induces a map between cotangent spaces.

@[simp]

theorem Algebra.Extension.Cotangent.map_mk {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') (x : ↥P.ker) : (map f) (mk x) = mk ⟨f.toAlgHom ↑x, ⋯⟩

@[simp]

theorem Algebra.Extension.Cotangent.map_id {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} : map (Hom.id P) = LinearMap.id

theorem Algebra.Extension.Cotangent.map_comp {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Extension R' S'} {R'' : Type u_4} {S'' : Type u_5} [CommRing R''] [CommRing S''] [Algebra R'' S''] (P'' : Extension R'' S'') [Algebra R R'] [Algebra R' R''] [Algebra R' S''] [Algebra S S'] [Algebra S' S''] [Algebra S S''] [Algebra R S'] [IsScalarTower R R' S'] [Algebra R R''] [IsScalarTower R R' R''] [IsScalarTower R' R'' S''] [Algebra R S''] [IsScalarTower R R'' S''] [IsScalarTower S S' S''] (f : P.Hom P') (g : P'.Hom P'') : map (g.comp f) = ↑S (map g) ∘ₗ map f

theorem Algebra.Extension.Cotangent.finite {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} (hP : P.ker.FG) : Module.Finite S P.Cotangent