Theorems · Theorem · ring theory

Coalgebra.sum_map_tmul_tmul_eq

∀ {R : Type u} {A : Type v} {ι : Type u_1} {κ : ι → Type u_2} {Λ : ι → Type u_3} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid A] [inst_2 : Module R A] [inst_3 : Coalgebra R A] {B : Type u_4} [inst_4 : AddCommMonoid B]
  [inst_5 : Module R B] {F : Type u_5} [inst_6 : FunLike F A B] [LinearMapClass F R A B] (f g h : F) (a : A)
  {repr : Coalgebra.Repr R a ι} {a₁ : (i : ι) → Coalgebra.Repr R (repr.left i) (κ i)}
  {a₂ : (i : ι) → Coalgebra.Repr R (repr.right i) (Λ i)},
  ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, f (repr.left i) ⊗ₜ[R] (g ((a₂ i).left j) ⊗ₜ[R] h ((a₂ i).right j)) =
    ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, f ((a₁ i).left j) ⊗ₜ[R] (g ((a₁ i).right j) ⊗ₜ[R] h (repr.right i))

Defined in

Mathlib.RingTheory.Coalgebra.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleCoalgebraAddCommMonoidModuleFunLikeLinearMapClass