Commit 2023-12-07 11:12 10038705

View on Github →

feat(RingTheory/Coalgebra): product of coalgebras (#8822) This also splits out a CoalgebraStruct typeclass, to allow defining the operators and their definitional properties before committing to proving coassociativity. These proofs are extremely painful, as you're fighting associativity all the time (and LinearMap.comp is very verbose in the goal view)

Estimated changes

Modified Mathlib/LinearAlgebra/Prod.lean

added theorem LinearMap.fst_comp_inl

added theorem LinearMap.fst_comp_inr

added theorem LinearMap.snd_comp_inl

added theorem LinearMap.snd_comp_inr

Modified Mathlib/LinearAlgebra/TensorProduct.lean

added theorem LinearMap.lTensor_comp_mk

added theorem LinearMap.rTensor_comp_flip_mk

added theorem TensorProduct.map_comm

added theorem TensorProduct.map_map_assoc

added theorem TensorProduct.map_map_assoc_symm

added theorem TensorProduct.map_map_comp_assoc_eq

added theorem TensorProduct.map_map_comp_assoc_symm_eq

added theorem TensorProduct.map_zero_left

added theorem TensorProduct.map_zero_right

Modified Mathlib/RingTheory/Coalgebra.lean

added theorem Prod.comul_apply

added theorem Prod.comul_comp_fst

added theorem Prod.comul_comp_inl

added theorem Prod.comul_comp_inr

added theorem Prod.comul_comp_snd

added theorem Prod.counit_apply

added theorem Prod.counit_comp_inl

added theorem Prod.counit_comp_inr