Extension of Scalars for Algebra Extensions

This file provides APIs for extending the base ring of an algebra extension P : Extension R S to its own extension ring P.Ring. We introduce canonical maps and isomorphisms between the cotangent spaces and the first homology of naive cotangent complex associated with P.extendScalars and P. We provide commutativity results of these maps and ismorphisms (See https://github.com/leanprover-community/mathlib4/pull/39520 for an image of the full diagram). In particular, we show the boundary map of the Jacobi-Zariski sequence of R → P.Ring → S coincides with P.cotangentComplex via a canonical isomorphism P.h1CotangentEquivCotangent.

Main definitions and results

• extendScalars: Views P : Extension R S as Extension P.Ring S.
• toExtendScalars: The canonical homomorphism from P to P.extendScalars induced by the identity map on the underlying extension rings.
• cotangentExtendScalarsEquiv : The linear equivalence between the cotangent spaces of P.extensScalars and P induced by the identity map.
• h1CotangentExtendScalarsEquiv: P.extensScalars can be used to compute the first homology of the naive cotangent complex of S over P.Ring.
• h1CotangentEquivOfSurjective: If R → P.Ring is surjective, this is the linear isomorphism induced by P.h1Cotangentι.
• h1CotangentEquivCotangent: This is the linear equivalence between H1Cotangent P.Ring S and P.Cotangent defined by the composition of h1CotangentExtendScalarsEquiv.symm, h1CotangentEquivOfSurjective and cotangentExtendScalarsEquiv.
• cotangentComplex_comp_h1CotangentEquivCotangent, h1CotangentEquivCotangent_comp_map: commutativity results.

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

Given an extension P of S over R, P.extendScalars is the same extension but viewed as an extension of S over P.Ring.

Equations

• P.extendScalars = { Ring := P.Ring, commRing := P.commRing, algebra₁ := Algebra.id P.Ring, algebra₂ := P.algebra₂, isScalarTower := ⋯, σ := P.σ, algebraMap_σ := ⋯ }

@[simp]

theorem Algebra.Extension.extendScalars_algebra₂ {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : P.extendScalars.algebra₂ = P.algebra₂

@[simp]

theorem Algebra.Extension.extendScalars_algebra₁ {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : P.extendScalars.algebra₁ = id P.Ring

@[simp]

theorem Algebra.Extension.extendScalars_commRing {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : P.extendScalars.commRing = P.commRing

@[simp]

theorem Algebra.Extension.extendScalars_σ {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) (a✝ : S) : P.extendScalars.σ a✝ = P.σ a✝

@[simp]

theorem Algebra.Extension.extendScalars_Ring {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : P.extendScalars.Ring = P.Ring

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

The canonical homomorphism from P to P.extendScalars induced by the identity map on the underlying extension rings.

Equations

• P.toExtendScalars = Algebra.Extension.Hom.ofAlgHom (IsScalarTower.toAlgHom R P.Ring P.extendScalars.Ring) ⋯

@[simp]

theorem Algebra.Extension.toExtendScalars_toRingHom_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) (x : P.Ring) : P.toExtendScalars.toRingHom x = x

noncomputable def Algebra.Extension.cotangentExtendScalarsEquiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : P.extendScalars.Cotangent ≃ₗ[S] P.Cotangent

Extension.extendScalars does not change the cotangent space of an extension.

Equations

• P.cotangentExtendScalarsEquiv = LinearEquiv.refl S P.extendScalars.Cotangent

@[simp]

theorem Algebra.Extension.cotangentExtendScalarsEquiv_symm_toLinearMap {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : ↑P.cotangentExtendScalarsEquiv.symm = Cotangent.map P.toExtendScalars

theorem Algebra.Extension.H1Cotangent.map_toExtendScalars_injective {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : Function.Injective ⇑(map P.toExtendScalars)

noncomputable def Algebra.Extension.h1CotangentExtendScalarsEquiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : P.extendScalars.H1Cotangent ≃ₗ[S] H1Cotangent P.Ring S

The first homology of the naive cotangent complex of P.extendScalars is linearly equivalent to that of S over P.Ring.

Equations

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

@[simp]

theorem Algebra.Extension.h1CotangentExtendScalarsEquiv_toLinearMap {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : ↑P.h1CotangentExtendScalarsEquiv = H1Cotangent.map (Hom.ofAlgHom (ofId P.Ring (Generators.self P.Ring S).Ring) ⋯)

@[simp]

theorem Algebra.Extension.h1CotangentExtendScalarsEquiv_symm_toLinearMap {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : ↑P.h1CotangentExtendScalarsEquiv.symm = H1Cotangent.map (defaultHom P.Ring S P.extendScalars)

noncomputable def Algebra.Extension.h1CotangentEquivOfSurjective {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) (h : Function.Surjective ⇑(algebraMap R P.Ring)) : P.H1Cotangent ≃ₗ[S] P.Cotangent

Given an extension P of S over R such that algebraMap R P.Ring is surjective, this is the equivalence induced by P.h1Cotangentι.

Equations

• P.h1CotangentEquivOfSurjective h = { toLinearMap := Algebra.Extension.h1Cotangentι, invFun := fun (x : P.Cotangent) => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Algebra.Extension.h1CotangentEquivOfSurjective_toLinearMap {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) (h : Function.Surjective ⇑(algebraMap R P.Ring)) : ↑(P.h1CotangentEquivOfSurjective h) = h1Cotangentι

noncomputable def Algebra.Extension.h1CotangentEquivCotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : H1Cotangent P.Ring S ≃ₗ[S] P.Cotangent

Given an extension P : Extension R S, this is the linear equivalence between the first homology of the naive cotangent complex of S over P.Ring and the cotangent space of P.

Equations

• P.h1CotangentEquivCotangent = (P.h1CotangentExtendScalarsEquiv.symm.trans (P.extendScalars.h1CotangentEquivOfSurjective ⋯)).trans P.cotangentExtendScalarsEquiv

theorem Algebra.Extension.cotangentComplex_comp_h1CotangentEquivCotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : P.cotangentComplex ∘ₗ ↑P.h1CotangentEquivCotangent = H1Cotangent.δ R P.Ring S

theorem Algebra.Extension.h1CotangentEquivCotangent_comp_map {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : ↑P.h1CotangentEquivCotangent ∘ₗ Algebra.H1Cotangent.map R P.Ring S S = h1Cotangentι ∘ₗ H1Cotangent.map (defaultHom R S P)

theorem Algebra.Extension.H1Cotangent.map_defaultHom_surjective {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : Function.Surjective ⇑(map (defaultHom R S P))