Theorems · Definition · nonassociative algebras

Derivation.couple

(R : Type u_1) →
  [inst : CommRing R] →
    (A : Type u_2) →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] →
          (A' : Type u_3) →
            [inst_3 : CommRing A'] →
              [inst_4 : Algebra R A'] →
                [inst_5 : Algebra A A'] →
                  [IsScalarTower R A A'] → LieSubalgebra R (Derivation R A' A' × Derivation R A A)

Let σ : A → A' be a an homomorphism. A derivation d : A → A and a derivation d' : A' → A' are called compatible if d' ∘ σ = σ ∘ d. Couples of derivations with this property form a Lie subalgebra of all couples of derivations.

Defined in

Mathlib.RingTheory.Derivation.Lie

Cited by

4 results in Mathlib

Foundations

Depth 53 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraCommRingAlgebraAlgebraIsScalarTower