Derivations into bimodules

This file defines derivations from a possibly noncommutative algebra into a bimodule. The right action is expressed, as usual in Mathlib, as a left action of the opposite algebra. These derivations are the maps represented by noncommutative universal one-forms.

Unlike Derivation, which currently treats commutative algebras and symmetric modules, BimoduleDerivation uses the associative Leibniz rule D (a * b) = a • D b + op b • D a.

A derivation of a possibly nonunital algebra A into a bimodule over its forced unitization extends by zero on the scalar summand to a derivation of Unitization k A; see BimoduleDerivation.ofUnitization.

structure TauCeti.BimoduleDerivation (k : Type u) (A : Type v) (M : Type w) [CommSemiring k] [Semiring A] [AddCommMonoid M] [Algebra k A] [Module k M] [Module A M] [Module Aᵐᵒᵖ M] [SMulCommClass A Aᵐᵒᵖ M] [IsScalarTower k A M] [IsScalarTower k Aᵐᵒᵖ M] extends A →ₗ[k] M : Type (max v w)

A derivation from an associative unital algebra into a bimodule.

The left action is the A-action and the right action is the Aᵐᵒᵖ-action; the two actions commute and are compatible with the ground-semiring action, so M is a k-linear bimodule. We include D 1 = 0 in the data so that the definition works over semirings and non-cancellative additive targets as well as over rings.

• toFun : A → M
• map_add' (x y : A) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : k) (x : A) : self.toFun (m • x) = (RingHom.id k) m • self.toFun x
• map_one_eq_zero' : self.toLinearMap 1 = 0
• leibniz' (a b : A) : self.toLinearMap (a * b) = a • self.toLinearMap b + MulOpposite.op b • self.toLinearMap a

@[instance_reducible]

instance TauCeti.BimoduleDerivation.instFunLike {k : Type u} {A : Type v} {M : Type w} [CommSemiring k] [Semiring A] [AddCommMonoid M] [Algebra k A] [Module k M] [Module A M] [Module Aᵐᵒᵖ M] [SMulCommClass A Aᵐᵒᵖ M] [IsScalarTower k A M] [IsScalarTower k Aᵐᵒᵖ M] : FunLike (BimoduleDerivation k A M) A M

instance TauCeti.BimoduleDerivation.instAddMonoidHomClass {k : Type u} {A : Type v} {M : Type w} [CommSemiring k] [Semiring A] [AddCommMonoid M] [Algebra k A] [Module k M] [Module A M] [Module Aᵐᵒᵖ M] [SMulCommClass A Aᵐᵒᵖ M] [IsScalarTower k A M] [IsScalarTower k Aᵐᵒᵖ M] : AddMonoidHomClass (BimoduleDerivation k A M) A M

@[instance_reducible]

instance TauCeti.BimoduleDerivation.instCoeLinearMapId {k : Type u} {A : Type v} {M : Type w} [CommSemiring k] [Semiring A] [AddCommMonoid M] [Algebra k A] [Module k M] [Module A M] [Module Aᵐᵒᵖ M] [SMulCommClass A Aᵐᵒᵖ M] [IsScalarTower k A M] [IsScalarTower k Aᵐᵒᵖ M] : Coe (BimoduleDerivation k A M) (A →ₗ[k] M)

@[simp]

theorem TauCeti.BimoduleDerivation.coe_toLinearMap {k : Type u} {A : Type v} {M : Type w} [CommSemiring k] [Semiring A] [AddCommMonoid M] [Algebra k A] [Module k M] [Module A M] [Module Aᵐᵒᵖ M] [SMulCommClass A Aᵐᵒᵖ M] [IsScalarTower k A M] [IsScalarTower k Aᵐᵒᵖ M] (D : BimoduleDerivation k A M) : ⇑D.toLinearMap = ⇑D

Coercion to the underlying linear map preserves the underlying function.

theorem TauCeti.BimoduleDerivation.ext {k : Type u} {A : Type v} {M : Type w} [CommSemiring k] [Semiring A] [AddCommMonoid M] [Algebra k A] [Module k M] [Module A M] [Module Aᵐᵒᵖ M] [SMulCommClass A Aᵐᵒᵖ M] [IsScalarTower k A M] [IsScalarTower k Aᵐᵒᵖ M] {D E : BimoduleDerivation k A M} (h : ∀ (a : A), D a = E a) : D = E

Two bimodule derivations are equal when they agree on every input.

theorem TauCeti.BimoduleDerivation.ext_iff {k : Type u} {A : Type v} {M : Type w} [CommSemiring k] [Semiring A] [AddCommMonoid M] [Algebra k A] [Module k M] [Module A M] [Module Aᵐᵒᵖ M] [SMulCommClass A Aᵐᵒᵖ M] [IsScalarTower k A M] [IsScalarTower k Aᵐᵒᵖ M] {D E : BimoduleDerivation k A M} : D = E ↔ ∀ (a : A), D a = E a

@[simp]

theorem TauCeti.BimoduleDerivation.map_one_eq_zero {k : Type u} {A : Type v} {M : Type w} [CommSemiring k] [Semiring A] [AddCommMonoid M] [Algebra k A] [Module k M] [Module A M] [Module Aᵐᵒᵖ M] [SMulCommClass A Aᵐᵒᵖ M] [IsScalarTower k A M] [IsScalarTower k Aᵐᵒᵖ M] (D : BimoduleDerivation k A M) : D 1 = 0

A bimodule derivation sends the unit to zero.

@[simp]

theorem TauCeti.BimoduleDerivation.leibniz {k : Type u} {A : Type v} {M : Type w} [CommSemiring k] [Semiring A] [AddCommMonoid M] [Algebra k A] [Module k M] [Module A M] [Module Aᵐᵒᵖ M] [SMulCommClass A Aᵐᵒᵖ M] [IsScalarTower k A M] [IsScalarTower k Aᵐᵒᵖ M] (D : BimoduleDerivation k A M) (a b : A) : D (a * b) = a • D b + MulOpposite.op b • D a

The associative Leibniz rule for a bimodule derivation.

@[simp]

theorem TauCeti.BimoduleDerivation.map_smul {k : Type u} {A : Type v} {M : Type w} [CommSemiring k] [Semiring A] [AddCommMonoid M] [Algebra k A] [Module k M] [Module A M] [Module Aᵐᵒᵖ M] [SMulCommClass A Aᵐᵒᵖ M] [IsScalarTower k A M] [IsScalarTower k Aᵐᵒᵖ M] (D : BimoduleDerivation k A M) (r : k) (a : A) : D (r • a) = r • D a

A bimodule derivation is linear over the ground semiring.

@[simp]

theorem TauCeti.BimoduleDerivation.map_algebraMap {k : Type u} {A : Type v} {M : Type w} [CommSemiring k] [Semiring A] [AddCommMonoid M] [Algebra k A] [Module k M] [Module A M] [Module Aᵐᵒᵖ M] [SMulCommClass A Aᵐᵒᵖ M] [IsScalarTower k A M] [IsScalarTower k Aᵐᵒᵖ M] (D : BimoduleDerivation k A M) (r : k) : D ((algebraMap k A) r) = 0

A bimodule derivation vanishes on scalars.

def TauCeti.BimoduleDerivation.ofUnitization {k : Type u} {A : Type v} {M : Type w} [CommSemiring k] [NonUnitalSemiring A] [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] [AddCommMonoid M] [Module k M] [Module (Unitization k A) M] [Module (Unitization k A)ᵐᵒᵖ M] [IsScalarTower k (Unitization k A) M] [IsScalarTower k (Unitization k A)ᵐᵒᵖ M] [SMulCommClass (Unitization k A) (Unitization k A)ᵐᵒᵖ M] (D : A →ₗ[k] M) (hD : ∀ (a b : A), D (a * b) = ↑a • D b + MulOpposite.op ↑b • D a) : BimoduleDerivation k (Unitization k A) M

Extend a derivation on a nonunital algebra by zero on the scalar summand of its forced unitization.

@[simp]

theorem TauCeti.BimoduleDerivation.ofUnitization_inr {k : Type u} {A : Type v} {M : Type w} [CommSemiring k] [NonUnitalSemiring A] [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] [AddCommMonoid M] [Module k M] [Module (Unitization k A) M] [Module (Unitization k A)ᵐᵒᵖ M] [IsScalarTower k (Unitization k A) M] [IsScalarTower k (Unitization k A)ᵐᵒᵖ M] [SMulCommClass (Unitization k A) (Unitization k A)ᵐᵒᵖ M] (D : A →ₗ[k] M) (hD : ∀ (a b : A), D (a * b) = ↑a • D b + MulOpposite.op ↑b • D a) (a : A) : (ofUnitization D hD) ↑a = D a

Extending by zero and then evaluating on the original algebra recovers the derivation.