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

Instances For

source

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

Algebra R₀ P.Ring

Equations

P.instRingOfIsScalarTower = Algebra.mk ((algebraMap R P.Ring).comp (algebraMap R₀ R)) ⋯ ⋯

source

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

IsScalarTower R₀ R P.Ring

Equations

⋯ = ⋯

source

instance Algebra.Extension.instIsScalarTowerRing_1 {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.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

Equations

⋯ = ⋯

source

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

IsScalarTower R₀ P.Ring S

Equations

⋯ = ⋯

source

@[simp]

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

P.σ x • y = x * y

source

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

Function.Injective P.σ

source

theorem Algebra.Extension.algebraMap_surjective {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Extension R S) :

Function.Surjective ⇑(algebraMap P.Ring S)

source

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) :

Algebra.Extension R S

Construct Extension from a surjective algebra homomorphism.

Equations

Algebra.Extension.ofSurjective f h = Algebra.Extension.mk P (fun (x : S) => ⋯.choose) ⋯

Instances For

source

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) :

(Algebra.Extension.ofSurjective f h).Ring = P

source

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) :

(Algebra.Extension.ofSurjective f h).σ x = ⋯.choose

source

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

Algebra.Extension R S

The trivial extension of S.

Equations

Algebra.Extension.self R S = Algebra.Extension.mk S id ⋯

Instances For

source

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

(Algebra.Extension.self R S).σ a = id a

source

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

(Algebra.Extension.self R S).Ring = S

source

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 : Algebra.Extension R S) :

Algebra.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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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 : Algebra.Extension R S) :

Algebra.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.

Equations

P.baseChange = Algebra.Extension.mk (TensorProduct R T P.Ring) (Algebra.Extension.ofSurjective (Algebra.TensorProduct.map (AlgHom.id T T) (IsScalarTower.toAlgHom R P.Ring S)) ⋯).σ ⋯

Instances For

source

structure Algebra.Extension.Hom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Extension R S) {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] (P' : Algebra.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)

Instances For

source

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

x = y

source

noncomputable def Algebra.Extension.Hom.toAlgHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.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.

Equations

f.toAlgHom = { toRingHom := f.toRingHom, commutes' := ⋯ }

Instances For

source

@[simp]

theorem Algebra.Extension.Hom.toAlgHom_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_2} {S' : Type u_1} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.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

source

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

P.Hom P

The identity hom.

Equations

Algebra.Extension.Hom.id P = { toRingHom := RingHom.id P.Ring, toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }

Instances For

source

@[simp]

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

(Algebra.Extension.Hom.id P).toRingHom = RingHom.id P.Ring

source

@[simp]

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

(Algebra.Extension.Hom.id P).toAlgHom = AlgHom.id R P.Ring

source

noncomputable def Algebra.Extension.Hom.comp {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} {R'' : Type u_4} {S'' : Type u_5} [CommRing R''] [CommRing S''] [Algebra R'' S''] {P'' : Algebra.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.

Equations

f.comp g = { toRingHom := f.toRingHom.comp g.toRingHom, toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }

Instances For

source

@[simp]

theorem Algebra.Extension.Hom.comp_toRingHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} {R'' : Type u_4} {S'' : Type u_5} [CommRing R''] [CommRing S''] [Algebra R'' S''] {P'' : Algebra.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

source

@[simp]

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

f.comp (Algebra.Extension.Hom.id P) = f

source

@[simp]

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

(Algebra.Extension.Hom.id P').comp f = f

source

@[reducible, inline]

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

Ideal P.Ring

The kernel of an extension.

Equations

P.ker = RingHom.ker (algebraMap P.Ring S)

Instances For

source

def Algebra.Extension.Cotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.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.

Equations

P.Cotangent = P.ker.Cotangent

Instances For

source

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

AddCommGroup P.Cotangent

Equations

P.instAddCommGroupCotangent = inferInstanceAs (AddCommGroup P.ker.Cotangent)

source

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

P.Cotangent

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

Equations

Algebra.Extension.Cotangent.of x = x

Instances For

source

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

P.ker.Cotangent

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

Equations

x.val = x

Instances For

source

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

x = y

source

@[simp]

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

(x + y).val = x.val + y.val

source

@[simp]

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

Algebra.Extension.Cotangent.val 0 = 0

source

@[simp]

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

Algebra.Extension.Cotangent.of (w + z) = Algebra.Extension.Cotangent.of w + Algebra.Extension.Cotangent.of z

source

@[simp]

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

Algebra.Extension.Cotangent.of 0 = 0

source

@[simp]

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

Algebra.Extension.Cotangent.of x.val = x

source

@[simp]

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

(Algebra.Extension.Cotangent.of w).val = w

source

@[simp]

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

(x - y).val = x.val - y.val

source

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

p • m = 0

source

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

Module S P.Cotangent

Equations

Algebra.Extension.Cotangent.module = Module.mk ⋯ ⋯

source

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

Module R₀ P.Cotangent

Equations

Algebra.Extension.instModuleCotangent = Module.compHom P.Cotangent (algebraMap R₀ S)

source

instance Algebra.Extension.instIsScalarTowerCotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.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

Equations

⋯ = ⋯

source

theorem Algebra.Extension.Cotangent.val_smul''' {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.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.

source

@[simp]

theorem Algebra.Extension.Cotangent.val_smul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.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.

source

@[simp]

theorem Algebra.Extension.Cotangent.val_smul' {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.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.

source

@[simp]

theorem Algebra.Extension.Cotangent.val_smul'' {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.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.

source

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

↥P.ker →ₗ[P.Ring] P.Cotangent

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

Equations

Algebra.Extension.Cotangent.mk = { toFun := fun (x : ↥P.ker) => Algebra.Extension.Cotangent.of (P.ker.toCotangent x), map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

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

(Algebra.Extension.Cotangent.mk x).val = P.ker.toCotangent x

source

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

Function.Surjective ⇑Algebra.Extension.Cotangent.mk

source

noncomputable def Algebra.Extension.Cotangent.map {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.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.

Equations

Algebra.Extension.Cotangent.map f = { toFun := fun (x : P.Cotangent) => Algebra.Extension.Cotangent.of ((P.ker.mapCotangent P'.ker f.toAlgHom ⋯) x.val), map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

theorem Algebra.Extension.Cotangent.map_mk {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') (x : ↥P.ker) :

(Algebra.Extension.Cotangent.map f) (Algebra.Extension.Cotangent.mk x) = Algebra.Extension.Cotangent.mk ⟨f.toAlgHom ↑x, ⋯⟩

source

@[simp]

theorem Algebra.Extension.Cotangent.map_id {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} :

Algebra.Extension.Cotangent.map (Algebra.Extension.Hom.id P) = LinearMap.id

source

theorem Algebra.Extension.Cotangent.map_comp {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} {R'' : Type u_4} {S'' : Type u_5} [CommRing R''] [CommRing S''] [Algebra R'' S''] (P'' : Algebra.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'') :

Algebra.Extension.Cotangent.map (g.comp f) = ↑S (Algebra.Extension.Cotangent.map g) ∘ₗ Algebra.Extension.Cotangent.map f

Documentation

Mathlib.RingTheory.Extension

Extension of algebras #

Main definition #