class GradedCoalgebra (R : Type u) [CommRing R] {ι : Type v} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (M : ι → Type w) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] extends Coalgebra R (DirectSum ι fun (i : ι) => M i) : Type (max (max u v) w)

Definition 26.1 (Graded coalgebra). A ι-graded coalgebra over a commutative ring R is a coalgebra structure on the direct sum ⨁_i M i whose coproduct Δ : M → M ⊗ M respects the grading: for any homogeneous element x ∈ M_n, the component of Δ x in degree (p, q) vanishes whenever p + q ≠ n. In other words, Δ(M_n) ⊆ ⨁_{p+q=n} M_p ⊗ M_q. This is the coalgebraic analogue of a graded algebra and is the structure carried by the cohomology of a (Hopf) space.

• comul : (DirectSum ι fun (i : ι) => M i) →ₗ[R] TensorProduct R (DirectSum ι fun (i : ι) => M i) (DirectSum ι fun (i : ι) => M i)
• counit : (DirectSum ι fun (i : ι) => M i) →ₗ[R] R
• coassoc : ↑(TensorProduct.assoc R (DirectSum ι fun (i : ι) => M i) (DirectSum ι fun (i : ι) => M i) (DirectSum ι fun (i : ι) => M i)) ∘ₗ LinearMap.rTensor (DirectSum ι fun (i : ι) => M i) comul ∘ₗ comul = LinearMap.lTensor (DirectSum ι fun (i : ι) => M i) comul ∘ₗ comul
• rTensor_counit_comp_comul : LinearMap.rTensor (DirectSum ι fun (i : ι) => M i) counit ∘ₗ comul = (TensorProduct.mk R R (DirectSum ι fun (i : ι) => M i)) 1
• lTensor_counit_comp_comul : LinearMap.lTensor (DirectSum ι fun (i : ι) => M i) counit ∘ₗ comul = (TensorProduct.mk R (DirectSum ι fun (i : ι) => M i) R).flip 1
• comul_respects_grading (n : ι) (x : M n) (p q : ι) : p + q ≠ n → (DirectSum.component R (ι × ι) (fun (pq : ι × ι) => TensorProduct R (M pq.1) (M pq.2)) (p, q)) ((TensorProduct.directSum R R M M) (CoalgebraStruct.comul ((DirectSum.lof R ι M n) x))) = 0

class CommGradedCoalgebra (R : Type u) [CommRing R] {ι : Type v} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (M : ι → Type w) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] extends GradedCoalgebra R M : Type (max (max u v) w)

Definition 26.1 / Corollary 26.2 (Cocommutative graded coalgebra). A graded coalgebra is graded-cocommutative when its coproduct is invariant under the Koszul-signed twist on the tensor product: τ ∘ Δ = Δ, where τ : M ⊗ M → M ⊗ M sends a ⊗ b ↦ (-1)^{|a||b|} b ⊗ a on homogeneous elements. The diagonal map on a topological space induces such a cocommutative graded-coalgebra structure on its singular cohomology (Cor 26.2).

• comul : (DirectSum ι fun (i : ι) => M i) →ₗ[R] TensorProduct R (DirectSum ι fun (i : ι) => M i) (DirectSum ι fun (i : ι) => M i)
• counit : (DirectSum ι fun (i : ι) => M i) →ₗ[R] R
• coassoc : ↑(TensorProduct.assoc R (DirectSum ι fun (i : ι) => M i) (DirectSum ι fun (i : ι) => M i) (DirectSum ι fun (i : ι) => M i)) ∘ₗ LinearMap.rTensor (DirectSum ι fun (i : ι) => M i) comul ∘ₗ comul = LinearMap.lTensor (DirectSum ι fun (i : ι) => M i) comul ∘ₗ comul
• rTensor_counit_comp_comul : LinearMap.rTensor (DirectSum ι fun (i : ι) => M i) counit ∘ₗ comul = (TensorProduct.mk R R (DirectSum ι fun (i : ι) => M i)) 1
• lTensor_counit_comp_comul : LinearMap.lTensor (DirectSum ι fun (i : ι) => M i) counit ∘ₗ comul = (TensorProduct.mk R (DirectSum ι fun (i : ι) => M i) R).flip 1
• comul_respects_grading (n : ι) (x : M n) (p q : ι) : p + q ≠ n → (DirectSum.component R (ι × ι) (fun (pq : ι × ι) => TensorProduct R (M pq.1) (M pq.2)) (p, q)) ((TensorProduct.directSum R R M M) (CoalgebraStruct.comul ((DirectSum.lof R ι M n) x))) = 0
• comul_comm : ↑(TensorProduct.gradedComm R M M) ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul