The self-extension of a module attached to a derivation

Let A be an R-algebra, δ a derivation of A (an element of TauCeti.derivationLieAlgebra R A) and M an A-module. The pairs (u, v) of elements of M form an A-module E_δ(M) under a • (u, v) = (a • u + δ a • v, a • v); the Leibniz rule δ (a * b) = δ a * b + a * δ b is exactly what makes this action associative. The maps u ↦ (u, 0) and (u, v) ↦ v are A-linear, so E_δ(M) is an extension of M by itself: 0 → M → E_δ(M) → M → 0. Writing (u, v) = v + ε u with ε² = 0, the module E_δ(M) is M[ε] with a acting through a + ε δ a, so it is the first-order deformation of M in the direction of δ. Changing δ by the inner derivation ad b = ⁅b, -⁆ does not change the extension: (u, v) ↦ (u + b • v, v) is an isomorphism E_δ(M) ≅ E_(δ + ad b)(M) compatible with both maps. These are the extensions through which outer derivations of A give classes in Ext¹_A(M, M); this file constructs the extensions themselves, not their Ext classes.

When A carries a topology, δ is continuous and M is a discrete module, E_δ(M) is again discrete, and the short exact sequence lives in the abelian category of discrete A-modules.

Main definitions

• TauCeti.DerivationExtension δ M: the module E_δ(M), with coordinates fst = u, snd = v.
• TauCeti.DerivationExtension.inlHom, TauCeti.DerivationExtension.sndHom: the inclusion u ↦ (u, 0) and the projection (u, v) ↦ v.
• TauCeti.DerivationExtension.map: functoriality in M.
• TauCeti.DerivationExtension.innerEquiv: for δ' = δ + innerDerivation R b, the isomorphism (u, v) ↦ (u + b • v, v) from E_δ(M) to E_δ'(M).
• TauCeti.DerivationExtension.shortComplex: the short complex M → E_δ(M) → M in ModuleCat A, and TauCeti.DerivationExtension.functor: the same, as a functor of M.
• TauCeti.DerivationExtension.functorInnerIso: the natural isomorphism of short complexes induced by innerEquiv, the identity on both ends.
• TauCeti.DerivationExtension.discreteShortComplex: the short complex in the full subcategory of discrete modules, for a continuous derivation.

Main results

• TauCeti.DerivationExtension.shortExact_shortComplex: 0 → M → E_δ(M) → M → 0 is short exact.
• TauCeti.DerivationExtension.innerEquiv_zero, TauCeti.DerivationExtension.innerEquiv_trans: the comparison for b = 0 is the identity, and the comparisons for b and b' compose to the comparison for b + b'.
• TauCeti.discreteModules_derivationExtension: E_δ(M) is discrete when δ is continuous and M is discrete.
• TauCeti.DerivationExtension.shortExact_discreteShortComplex: the sequence is short exact in the category of discrete modules.

Implementation notes

DerivationExtension δ M is a structure rather than a synonym for M × M: the product already carries the componentwise A-module structure, which is a different one. The additive group is transported from M × M along DerivationExtension.equivProd.

The bodies of shortComplex, functor and discreteShortComplex are exposed: their objects and maps are the data a consumer computes with, and their simps lemmas are proved by unfolding.

References

• Edward Frenkel, Langlands Correspondence for Loop Groups, for the role of first-order deformations of modules over the completed enveloping algebra at the critical level.

structure TauCeti.DerivationExtension {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : Type v) : Type v

The self-extension E_δ(M) of a module M attached to a derivation δ: pairs (u, v) of elements of M, on which a acts by a • (u, v) = (a • u + δ a • v, a • v). The first coordinate carries the submodule M and the second the quotient M.

• fst : M

  The coordinate u of (u, v), in which the submodule M sits.

• snd : M

  The coordinate v of (u, v), the image in the quotient M.

theorem TauCeti.DerivationExtension.ext {R : Type u_1} {inst✝ : CommRing R} {A : Type u} {inst✝¹ : Ring A} {inst✝² : Algebra R A} {δ : ↥(derivationLieAlgebra R A)} {M : Type v} {x y : DerivationExtension δ M} (fst : x.fst = y.fst) (snd : x.snd = y.snd) : x = y

theorem TauCeti.DerivationExtension.ext_iff {R : Type u_1} {inst✝ : CommRing R} {A : Type u} {inst✝¹ : Ring A} {inst✝² : Algebra R A} {δ : ↥(derivationLieAlgebra R A)} {M : Type v} {x y : DerivationExtension δ M} : x = y ↔ x.fst = y.fst ∧ x.snd = y.snd

def TauCeti.DerivationExtension.equivProd {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : Type v) : DerivationExtension δ M ≃ M × M

The underlying set of E_δ(M) is M × M.

@[simp]

theorem TauCeti.DerivationExtension.equivProd_apply {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : Type v) (x : DerivationExtension δ M) : (equivProd δ M) x = (x.fst, x.snd)

@[simp]

theorem TauCeti.DerivationExtension.equivProd_symm_apply {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : Type v) (x : M × M) : (equivProd δ M).symm x = { fst := x.1, snd := x.2 }

@[instance_reducible]

instance TauCeti.DerivationExtension.instAddCommGroup {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : Type v) [AddCommGroup M] : AddCommGroup (DerivationExtension δ M)

@[simp]

theorem TauCeti.DerivationExtension.fst_zero {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} {M : Type v} [AddCommGroup M] : fst 0 = 0

@[simp]

theorem TauCeti.DerivationExtension.snd_zero {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} {M : Type v} [AddCommGroup M] : snd 0 = 0

@[simp]

theorem TauCeti.DerivationExtension.fst_add {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} {M : Type v} [AddCommGroup M] (x y : DerivationExtension δ M) : (x + y).fst = x.fst + y.fst

@[simp]

theorem TauCeti.DerivationExtension.snd_add {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} {M : Type v} [AddCommGroup M] (x y : DerivationExtension δ M) : (x + y).snd = x.snd + y.snd

@[simp]

theorem TauCeti.DerivationExtension.fst_neg {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} {M : Type v} [AddCommGroup M] (x : DerivationExtension δ M) : (-x).fst = -x.fst

@[simp]

theorem TauCeti.DerivationExtension.snd_neg {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} {M : Type v} [AddCommGroup M] (x : DerivationExtension δ M) : (-x).snd = -x.snd

@[simp]

theorem TauCeti.DerivationExtension.fst_sub {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} {M : Type v} [AddCommGroup M] (x y : DerivationExtension δ M) : (x - y).fst = x.fst - y.fst

@[simp]

theorem TauCeti.DerivationExtension.snd_sub {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} {M : Type v} [AddCommGroup M] (x y : DerivationExtension δ M) : (x - y).snd = x.snd - y.snd

@[instance_reducible]

instance TauCeti.DerivationExtension.instSMul {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} {M : Type v} [AddCommGroup M] [Module A M] : SMul A (DerivationExtension δ M)

@[simp]

theorem TauCeti.DerivationExtension.fst_smul {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} {M : Type v} [AddCommGroup M] [Module A M] (a : A) (x : DerivationExtension δ M) : (a • x).fst = a • x.fst + ↑δ a • x.snd

@[simp]

theorem TauCeti.DerivationExtension.snd_smul {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} {M : Type v} [AddCommGroup M] [Module A M] (a : A) (x : DerivationExtension δ M) : (a • x).snd = a • x.snd

@[instance_reducible]

instance TauCeti.DerivationExtension.instModule {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} {M : Type v} [AddCommGroup M] [Module A M] : Module A (DerivationExtension δ M)

def TauCeti.DerivationExtension.inlHom {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : Type v) [AddCommGroup M] [Module A M] : M →ₗ[A] DerivationExtension δ M

The inclusion u ↦ (u, 0) of the submodule M into E_δ(M).

@[simp]

theorem TauCeti.DerivationExtension.fst_inlHom {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : Type v) [AddCommGroup M] [Module A M] (u : M) : ((inlHom δ M) u).fst = u

@[simp]

theorem TauCeti.DerivationExtension.snd_inlHom {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : Type v) [AddCommGroup M] [Module A M] (u : M) : ((inlHom δ M) u).snd = 0

def TauCeti.DerivationExtension.sndHom {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : Type v) [AddCommGroup M] [Module A M] : DerivationExtension δ M →ₗ[A] M

The projection (u, v) ↦ v of E_δ(M) onto the quotient M.

@[simp]

theorem TauCeti.DerivationExtension.sndHom_apply {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : Type v) [AddCommGroup M] [Module A M] (x : DerivationExtension δ M) : (sndHom δ M) x = x.snd

theorem TauCeti.DerivationExtension.inlHom_injective {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : Type v) [AddCommGroup M] [Module A M] : Function.Injective ⇑(inlHom δ M)

theorem TauCeti.DerivationExtension.sndHom_surjective {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : Type v) [AddCommGroup M] [Module A M] : Function.Surjective ⇑(sndHom δ M)

@[simp]

theorem TauCeti.DerivationExtension.sndHom_comp_inlHom {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : Type v) [AddCommGroup M] [Module A M] : sndHom δ M ∘ₗ inlHom δ M = 0

theorem TauCeti.DerivationExtension.exact_inlHom_sndHom {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : Type v) [AddCommGroup M] [Module A M] : Function.Exact ⇑(inlHom δ M) ⇑(sndHom δ M)

E_δ(M) is an extension of M by M: the kernel of the projection is the image of the inclusion.

def TauCeti.DerivationExtension.map {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) : DerivationExtension δ M →ₗ[A] DerivationExtension δ N

The functoriality of E_δ(-): a linear map f acts coordinatewise.

@[simp]

theorem TauCeti.DerivationExtension.fst_map {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) (x : DerivationExtension δ M) : ((map f) x).fst = f x.fst

@[simp]

theorem TauCeti.DerivationExtension.snd_map {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) (x : DerivationExtension δ M) : ((map f) x).snd = f x.snd

@[simp]

theorem TauCeti.DerivationExtension.map_id {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} {M : Type v} [AddCommGroup M] [Module A M] : map LinearMap.id = LinearMap.id

theorem TauCeti.DerivationExtension.map_comp {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] {P : Type u_2} [AddCommGroup P] [Module A P] (f : M →ₗ[A] N) (g : N →ₗ[A] P) : map (g ∘ₗ f) = map g ∘ₗ map f

theorem TauCeti.DerivationExtension.map_comp_inlHom {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) : map f ∘ₗ inlHom δ M = inlHom δ N ∘ₗ f

theorem TauCeti.DerivationExtension.sndHom_comp_map {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) : sndHom δ N ∘ₗ map f = f ∘ₗ sndHom δ M

def TauCeti.DerivationExtension.innerEquiv {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ δ' : ↥(derivationLieAlgebra R A)} {b : A} (M : Type v) [AddCommGroup M] [Module A M] (h : δ' = δ + (innerDerivation R) b) : DerivationExtension δ M ≃ₗ[A] DerivationExtension δ' M

Changing a derivation by an inner derivation does not change its self-extension: when δ' = δ + ad b, the map (u, v) ↦ (u + b • v, v) is an isomorphism E_δ(M) ≃ E_δ'(M).

@[simp]

theorem TauCeti.DerivationExtension.fst_innerEquiv {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ δ' : ↥(derivationLieAlgebra R A)} {b : A} (M : Type v) [AddCommGroup M] [Module A M] (h : δ' = δ + (innerDerivation R) b) (x : DerivationExtension δ M) : ((innerEquiv M h) x).fst = x.fst + b • x.snd

@[simp]

theorem TauCeti.DerivationExtension.snd_innerEquiv {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ δ' : ↥(derivationLieAlgebra R A)} {b : A} (M : Type v) [AddCommGroup M] [Module A M] (h : δ' = δ + (innerDerivation R) b) (x : DerivationExtension δ M) : ((innerEquiv M h) x).snd = x.snd

@[simp]

theorem TauCeti.DerivationExtension.fst_innerEquiv_symm {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ δ' : ↥(derivationLieAlgebra R A)} {b : A} (M : Type v) [AddCommGroup M] [Module A M] (h : δ' = δ + (innerDerivation R) b) (x : DerivationExtension δ' M) : ((innerEquiv M h).symm x).fst = x.fst - b • x.snd

@[simp]

theorem TauCeti.DerivationExtension.snd_innerEquiv_symm {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ δ' : ↥(derivationLieAlgebra R A)} {b : A} (M : Type v) [AddCommGroup M] [Module A M] (h : δ' = δ + (innerDerivation R) b) (x : DerivationExtension δ' M) : ((innerEquiv M h).symm x).snd = x.snd

@[simp]

theorem TauCeti.DerivationExtension.innerEquiv_comp_inlHom {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ δ' : ↥(derivationLieAlgebra R A)} {b : A} (M : Type v) [AddCommGroup M] [Module A M] (h : δ' = δ + (innerDerivation R) b) : ↑(innerEquiv M h) ∘ₗ inlHom δ M = inlHom δ' M

The comparison innerEquiv restricts to the identity on the submodule M.

@[simp]

theorem TauCeti.DerivationExtension.sndHom_comp_innerEquiv {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ δ' : ↥(derivationLieAlgebra R A)} {b : A} (M : Type v) [AddCommGroup M] [Module A M] (h : δ' = δ + (innerDerivation R) b) : sndHom δ' M ∘ₗ ↑(innerEquiv M h) = sndHom δ M

The comparison innerEquiv induces the identity on the quotient M.

theorem TauCeti.DerivationExtension.map_comp_innerEquiv {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ δ' : ↥(derivationLieAlgebra R A)} {b : A} (M : Type v) [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (h : δ' = δ + (innerDerivation R) b) (f : M →ₗ[A] N) : map f ∘ₗ ↑(innerEquiv M h) = ↑(innerEquiv N h) ∘ₗ map f

The comparison innerEquiv is natural in M.

@[simp]

theorem TauCeti.DerivationExtension.innerEquiv_zero {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} (M : Type v) [AddCommGroup M] [Module A M] (h : δ = δ + (innerDerivation R) 0) : innerEquiv M h = LinearEquiv.refl A (DerivationExtension δ M)

The comparison for the zero inner derivation is the identity.

theorem TauCeti.DerivationExtension.innerEquiv_trans {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ δ' δ'' : ↥(derivationLieAlgebra R A)} {b b' : A} (M : Type v) [AddCommGroup M] [Module A M] (h : δ' = δ + (innerDerivation R) b) (h' : δ'' = δ' + (innerDerivation R) b') : innerEquiv M h ≪≫ₗ innerEquiv M h' = innerEquiv M ⋯

The comparisons for b and b' compose to the comparison for b + b'.

theorem TauCeti.DerivationExtension.innerEquiv_symm {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ δ' : ↥(derivationLieAlgebra R A)} {b : A} (M : Type v) [AddCommGroup M] [Module A M] (h : δ' = δ + (innerDerivation R) b) : (innerEquiv M h).symm = innerEquiv M ⋯

The inverse of the comparison for b is the comparison for -b.

def TauCeti.DerivationExtension.shortComplex {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : ModuleCat A) : CategoryTheory.ShortComplex (ModuleCat A)

The self-extension 0 → M → E_δ(M) → M → 0, as a short complex in ModuleCat A.

@[simp]

theorem TauCeti.DerivationExtension.shortComplex_X₃ {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : ModuleCat A) : (shortComplex δ M).X₃ = M

@[simp]

theorem TauCeti.DerivationExtension.shortComplex_g {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : ModuleCat A) : (shortComplex δ M).g = ModuleCat.ofHom (sndHom δ ↑M)

@[simp]

theorem TauCeti.DerivationExtension.shortComplex_X₂_carrier {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : ModuleCat A) : ↑(shortComplex δ M).X₂ = DerivationExtension δ ↑M

@[simp]

theorem TauCeti.DerivationExtension.shortComplex_f {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : ModuleCat A) : (shortComplex δ M).f = ModuleCat.ofHom (inlHom δ ↑M)

@[simp]

theorem TauCeti.DerivationExtension.shortComplex_X₁ {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : ModuleCat A) : (shortComplex δ M).X₁ = M

theorem TauCeti.DerivationExtension.shortExact_shortComplex {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : ModuleCat A) : (shortComplex δ M).ShortExact

The self-extension of M attached to a derivation is a short exact sequence.

def TauCeti.DerivationExtension.functor {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) : CategoryTheory.Functor (ModuleCat A) (CategoryTheory.ShortComplex (ModuleCat A))

The self-extension 0 → M → E_δ(M) → M → 0, as a functor of M.

@[simp]

theorem TauCeti.DerivationExtension.functor_map_τ₂ {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) {X✝ Y✝ : ModuleCat A} (f : X✝ ⟶ Y✝) : ((functor δ).map f).τ₂ = ModuleCat.ofHom (map (ModuleCat.Hom.hom f))

@[simp]

theorem TauCeti.DerivationExtension.functor_map_τ₁ {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) {X✝ Y✝ : ModuleCat A} (f : X✝ ⟶ Y✝) : ((functor δ).map f).τ₁ = f

@[simp]

theorem TauCeti.DerivationExtension.functor_obj {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) (M : ModuleCat A) : (functor δ).obj M = shortComplex δ M

@[simp]

theorem TauCeti.DerivationExtension.functor_map_τ₃ {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] (δ : ↥(derivationLieAlgebra R A)) {X✝ Y✝ : ModuleCat A} (f : X✝ ⟶ Y✝) : ((functor δ).map f).τ₃ = f

def TauCeti.DerivationExtension.functorInnerIso {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ δ' : ↥(derivationLieAlgebra R A)} {b : A} (h : δ' = δ + (innerDerivation R) b) : functor δ ≅ functor δ'

When δ' = δ + ad b, the self-extensions attached to δ and δ' are isomorphic as extensions, naturally in M: the isomorphism is innerEquiv in the middle and the identity on both ends.

@[simp]

theorem TauCeti.DerivationExtension.functorInnerIso_hom_app_τ₂ {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} (M : ModuleCat A) {δ' : ↥(derivationLieAlgebra R A)} {b : A} (h : δ' = δ + (innerDerivation R) b) : ((functorInnerIso h).hom.app M).τ₂ = ModuleCat.ofHom ↑(innerEquiv (↑M) h)

@[simp]

theorem TauCeti.DerivationExtension.functorInnerIso_hom_app_τ₁ {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} (M : ModuleCat A) {δ' : ↥(derivationLieAlgebra R A)} {b : A} (h : δ' = δ + (innerDerivation R) b) : ((functorInnerIso h).hom.app M).τ₁ = CategoryTheory.CategoryStruct.id M

@[simp]

theorem TauCeti.DerivationExtension.functorInnerIso_hom_app_τ₃ {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} (M : ModuleCat A) {δ' : ↥(derivationLieAlgebra R A)} {b : A} (h : δ' = δ + (innerDerivation R) b) : ((functorInnerIso h).hom.app M).τ₃ = CategoryTheory.CategoryStruct.id M

@[simp]

theorem TauCeti.DerivationExtension.functorInnerIso_inv_app_τ₂ {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} (M : ModuleCat A) {δ' : ↥(derivationLieAlgebra R A)} {b : A} (h : δ' = δ + (innerDerivation R) b) : ((functorInnerIso h).inv.app M).τ₂ = ModuleCat.ofHom ↑(innerEquiv (↑M) h).symm

@[simp]

theorem TauCeti.DerivationExtension.functorInnerIso_inv_app_τ₁ {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} (M : ModuleCat A) {δ' : ↥(derivationLieAlgebra R A)} {b : A} (h : δ' = δ + (innerDerivation R) b) : ((functorInnerIso h).inv.app M).τ₁ = CategoryTheory.CategoryStruct.id M

@[simp]

theorem TauCeti.DerivationExtension.functorInnerIso_inv_app_τ₃ {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] {δ : ↥(derivationLieAlgebra R A)} (M : ModuleCat A) {δ' : ↥(derivationLieAlgebra R A)} {b : A} (h : δ' = δ + (innerDerivation R) b) : ((functorInnerIso h).inv.app M).τ₃ = CategoryTheory.CategoryStruct.id M

theorem TauCeti.discreteModules_derivationExtension {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] [TopologicalSpace A] {δ : ↥(derivationLieAlgebra R A)} (hδ : Continuous ⇑↑δ) {M : ModuleCat A} (hM : discreteModules A M) : discreteModules A ↧(DerivationExtension δ ↑M)

The self-extension of a discrete module along a continuous derivation is discrete.

def TauCeti.DerivationExtension.discreteShortComplex {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] [TopologicalSpace A] {δ : ↥(derivationLieAlgebra R A)} (hδ : Continuous ⇑↑δ) (M : (discreteModules A).FullSubcategory) : CategoryTheory.ShortComplex (discreteModules A).FullSubcategory

For a continuous derivation δ and a discrete module M, the self-extension 0 → M → E_δ(M) → M → 0, as a short complex in the category of discrete modules.

@[simp]

theorem TauCeti.DerivationExtension.discreteShortComplex_X₃ {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] [TopologicalSpace A] {δ : ↥(derivationLieAlgebra R A)} (hδ : Continuous ⇑↑δ) (M : (discreteModules A).FullSubcategory) : (discreteShortComplex hδ M).X₃ = M

@[simp]

theorem TauCeti.DerivationExtension.discreteShortComplex_f {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] [TopologicalSpace A] {δ : ↥(derivationLieAlgebra R A)} (hδ : Continuous ⇑↑δ) (M : (discreteModules A).FullSubcategory) : (discreteShortComplex hδ M).f = CategoryTheory.ObjectProperty.homMk (shortComplex δ M.obj).f

@[simp]

theorem TauCeti.DerivationExtension.discreteShortComplex_X₁ {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] [TopologicalSpace A] {δ : ↥(derivationLieAlgebra R A)} (hδ : Continuous ⇑↑δ) (M : (discreteModules A).FullSubcategory) : (discreteShortComplex hδ M).X₁ = M

@[simp]

theorem TauCeti.DerivationExtension.discreteShortComplex_g {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] [TopologicalSpace A] {δ : ↥(derivationLieAlgebra R A)} (hδ : Continuous ⇑↑δ) (M : (discreteModules A).FullSubcategory) : (discreteShortComplex hδ M).g = CategoryTheory.ObjectProperty.homMk (shortComplex δ M.obj).g

@[simp]

theorem TauCeti.DerivationExtension.discreteShortComplex_X₂_obj_carrier {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] [TopologicalSpace A] {δ : ↥(derivationLieAlgebra R A)} (hδ : Continuous ⇑↑δ) (M : (discreteModules A).FullSubcategory) : ↑(discreteShortComplex hδ M).X₂.obj = DerivationExtension δ ↑M.obj

@[simp]

theorem TauCeti.DerivationExtension.discreteShortComplex_map_ι {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] [TopologicalSpace A] {δ : ↥(derivationLieAlgebra R A)} (hδ : Continuous ⇑↑δ) (M : (discreteModules A).FullSubcategory) : (discreteShortComplex hδ M).map (discreteModules A).ι = shortComplex δ M.obj

The inclusion of discrete modules sends discreteShortComplex to shortComplex.

theorem TauCeti.DerivationExtension.shortExact_discreteShortComplex {R : Type u_1} [CommRing R] {A : Type u} [Ring A] [Algebra R A] [TopologicalSpace A] {δ : ↥(derivationLieAlgebra R A)} (hδ : Continuous ⇑↑δ) (M : (discreteModules A).FullSubcategory) : (discreteShortComplex hδ M).ShortExact

The self-extension of a discrete module along a continuous derivation is short exact in the category of discrete modules.