Theorems · Inductive type · ring theory

Coalgebra.IsCocomm

(R : Type u) →
  (A : Type v) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → [Coalgebra R A] → Prop

A coalgebra A is cocommutative if its comultiplication δ : A → A ⊗ A commutes with the swapping β : A ⊗ A ≃ A ⊗ A of the factors in the tensor product.

Defined in

Mathlib.RingTheory.Coalgebra.Basic

Cited by

11 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CommSemiringAddCommMonoidModuleCoalgebra