Theorems · Theorem · ring theory

Coalgebra.rTensor_counit_comp_comul

∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : AddCommMonoid A} {inst_2 : Module R A}
  [self : Coalgebra R A],
  LinearMap.rTensor A CoalgebraStruct.counit ∘ₗ CoalgebraStruct.comul = (TensorProduct.mk R R A) 1

The counit satisfies the left counitality law

Defined in

Mathlib.RingTheory.Coalgebra.Basic

Cited by

4 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Quot.sound

Assumes

Coalgebra