Tactic to reassociate comultiplication in a coalgebra

coassoc_simps is a simp set useful to prove tautologies on coalgebras.

The general algorithm it follows is to push the associators TensorProduct.assoc and commutators TensorProduct.comm inwards (to the right) until they cancel against co-multiplications.

The simp set makes the following choice of normal form

• It regards TensorProduct.map, TensorProduct.assoc, TensorProduct.comm as the primitive constructions and rewrites everything else such as lTensor, leftComm using them.
• It rewrites both sides into a right associated composition of linear maps. In particular LinearMap.comp_assoc and LinearEquiv.coe_trans are tagged.
• It rewrites (f₂ ⊗ g₂) ∘ (f₁ ⊗ g₁) into (f₂ ∘ f₁) ⊗ (g₂ ∘ g₁).

Notes

• It is not confluent with (ε ⊗ₘ id) ∘ₗ δ = λ⁻¹. It is often useful to trans (or calc) with a term containing (ε ⊗ₘ _) ∘ₗ δ or (_ ⊗ₘ ε) ∘ₗ δ, and use one of map_counit_comp_comul_left map_counit_comp_comul_right map_counit_comp_comul_left_assoc map_counit_comp_comul_right_assoc to continue.

• Some lemmas (e.g. lid_comp_map : λ ∘ₗ (f ⊗ₘ g) = g ∘ₗ λ ∘ₗ (f ⊗ₘ id)) loops when tagged as simp, so we wrap it inside a rudimentary simproc that only fires when g ≠ id.

theorem CoassocSimps.TensorProduct.map_comp_assoc {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} {N' : Type u_7} {P' : Type u_8} {M₁ : Type u_11} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [AddCommMonoid M'] [Module R M'] [AddCommMonoid N'] [Module R N'] [AddCommMonoid P'] [Module R P'] [AddCommMonoid M₁] [Module R M₁] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (f' : M' →ₗ[R] N') (g' : N' →ₗ[R] P') (φ : M₁ →ₗ[R] TensorProduct R M M') : TensorProduct.map g g' ∘ₗ TensorProduct.map f f' ∘ₗ φ = TensorProduct.map (g ∘ₗ f) (g' ∘ₗ f') ∘ₗ φ

theorem CoassocSimps.TensorProduct.map_map_comp_assoc_eq_assoc {R : Type u_1} {M : Type u_3} {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15} {N₃ : Type u_16} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃] [Module R M₁] [Module R M₂] [Module R M₃] [Module R N₁] [Module R N₂] [Module R N₃] (f₁ : M₁ →ₗ[R] N₁) (f₂ : M₂ →ₗ[R] N₂) (f₃ : M₃ →ₗ[R] N₃) (f : M →ₗ[R] TensorProduct R (TensorProduct R M₁ M₂) M₃) : TensorProduct.map f₁ (TensorProduct.map f₂ f₃) ∘ₗ ↑(TensorProduct.assoc R M₁ M₂ M₃) ∘ₗ f = ↑(TensorProduct.assoc R N₁ N₂ N₃) ∘ₗ TensorProduct.map (TensorProduct.map f₁ f₂) f₃ ∘ₗ f

theorem CoassocSimps.TensorProduct.map_map_comp_assoc_symm_eq_assoc {R : Type u_1} {M : Type u_3} {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15} {N₃ : Type u_16} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃] [Module R M₁] [Module R M₂] [Module R M₃] [Module R N₁] [Module R N₂] [Module R N₃] (f₁ : M₁ →ₗ[R] N₁) (f₂ : M₂ →ₗ[R] N₂) (f₃ : M₃ →ₗ[R] N₃) (f : M →ₗ[R] TensorProduct R M₁ (TensorProduct R M₂ M₃)) : TensorProduct.map (TensorProduct.map f₁ f₂) f₃ ∘ₗ ↑(TensorProduct.assoc R M₁ M₂ M₃).symm ∘ₗ f = ↑(TensorProduct.assoc R N₁ N₂ N₃).symm ∘ₗ TensorProduct.map f₁ (TensorProduct.map f₂ f₃) ∘ₗ f

theorem CoassocSimps.assoc_comp_map_map_comp {R : Type u_1} {M : Type u_3} {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15} {N₃ : Type u_16} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃] [Module R M₁] [Module R M₂] [Module R M₃] [Module R N₁] [Module R N₂] [Module R N₃] (f₁ : M₁ →ₗ[R] N₁) (f₂ : M₂ →ₗ[R] N₂) (f₃ : M₃ →ₗ[R] N₃) (f₁₂ : M →ₗ[R] TensorProduct R M₁ M₂) : ↑(TensorProduct.assoc R N₁ N₂ N₃) ∘ₗ TensorProduct.map (TensorProduct.map f₁ f₂ ∘ₗ f₁₂) f₃ = TensorProduct.map f₁ (TensorProduct.map f₂ f₃) ∘ₗ ↑(TensorProduct.assoc R M₁ M₂ M₃) ∘ₗ TensorProduct.map f₁₂ LinearMap.id

theorem CoassocSimps.assoc_comp_map_map_comp_assoc {R : Type u_1} {M : Type u_3} {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15} {N₃ : Type u_16} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃] [Module R M₁] [Module R M₂] [Module R M₃] [Module R N₁] [Module R N₂] [Module R N₃] (f₁ : M₁ →ₗ[R] N₁) (f₂ : M₂ →ₗ[R] N₂) (f₃ : M₃ →ₗ[R] N₃) (f₁₂ : M →ₗ[R] TensorProduct R M₁ M₂) (f : M →ₗ[R] TensorProduct R M M₃) : ↑(TensorProduct.assoc R N₁ N₂ N₃) ∘ₗ TensorProduct.map (TensorProduct.map f₁ f₂ ∘ₗ f₁₂) f₃ ∘ₗ f = TensorProduct.map f₁ (TensorProduct.map f₂ f₃) ∘ₗ ↑(TensorProduct.assoc R M₁ M₂ M₃) ∘ₗ TensorProduct.map f₁₂ LinearMap.id ∘ₗ f

theorem CoassocSimps.assoc_comp_map {R : Type u_1} {M : Type u_3} {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₃ : Type u_16} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid N₃] [Module R M₁] [Module R M₂] [Module R M₃] [Module R N₃] (f₃ : M₃ →ₗ[R] N₃) (f₁₂ : M →ₗ[R] TensorProduct R M₁ M₂) : ↑(TensorProduct.assoc R M₁ M₂ N₃) ∘ₗ TensorProduct.map f₁₂ f₃ = TensorProduct.map LinearMap.id (TensorProduct.map LinearMap.id f₃) ∘ₗ ↑(TensorProduct.assoc R M₁ M₂ M₃) ∘ₗ TensorProduct.map f₁₂ LinearMap.id

def CoassocSimps.assoc_comp_map_simproc : Lean.Meta.Simp.Simproc

Simproc version of assoc_comp_map that only fires when f₃ ≠ id.

Equations

• One or more equations did not get rendered due to their size.

theorem CoassocSimps.assoc_comp_map_assoc {R : Type u_1} {M : Type u_3} {P : Type u_5} {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₃ : Type u_16} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid N₃] [Module R M₁] [Module R M₂] [Module R M₃] [Module R N₃] (f₃ : M₃ →ₗ[R] N₃) (f₁₂ : M →ₗ[R] TensorProduct R M₁ M₂) (f : P →ₗ[R] TensorProduct R M M₃) : ↑(TensorProduct.assoc R M₁ M₂ N₃) ∘ₗ TensorProduct.map f₁₂ f₃ ∘ₗ f = TensorProduct.map LinearMap.id (TensorProduct.map LinearMap.id f₃) ∘ₗ ↑(TensorProduct.assoc R M₁ M₂ M₃) ∘ₗ TensorProduct.map f₁₂ LinearMap.id ∘ₗ f

def CoassocSimps.assoc_comp_map_assoc_simproc : Lean.Meta.Simp.Simproc

Simproc version of assoc_comp_map_assoc that only fires when f₃ ≠ id.

Equations

• One or more equations did not get rendered due to their size.

theorem CoassocSimps.assoc_symm_comp_map {R : Type u_1} {M : Type u_3} {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₁ : Type u_14} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid N₁] [Module R M₁] [Module R M₂] [Module R M₃] [Module R N₁] (f₁ : M₁ →ₗ[R] N₁) (f₂₃ : M →ₗ[R] TensorProduct R M₂ M₃) : ↑(TensorProduct.assoc R N₁ M₂ M₃).symm ∘ₗ TensorProduct.map f₁ f₂₃ = TensorProduct.map (TensorProduct.map f₁ LinearMap.id) LinearMap.id ∘ₗ ↑(TensorProduct.assoc R M₁ M₂ M₃).symm ∘ₗ TensorProduct.map LinearMap.id f₂₃

def CoassocSimps.assoc_symm_comp_map_simproc : Lean.Meta.Simp.Simproc

Simproc version of assoc_symm_comp_map that only fires when f₁ ≠ id.

Equations

• One or more equations did not get rendered due to their size.

theorem CoassocSimps.assoc_symm_comp_map_assoc {R : Type u_1} {M : Type u_3} {P : Type u_5} {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₁ : Type u_14} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid N₁] [Module R M₁] [Module R M₂] [Module R M₃] [Module R N₁] (f₁ : M₁ →ₗ[R] N₁) (f₂₃ : M →ₗ[R] TensorProduct R M₂ M₃) (f : P →ₗ[R] TensorProduct R M₁ M) : ↑(TensorProduct.assoc R N₁ M₂ M₃).symm ∘ₗ TensorProduct.map f₁ f₂₃ ∘ₗ f = TensorProduct.map (TensorProduct.map f₁ LinearMap.id) LinearMap.id ∘ₗ ↑(TensorProduct.assoc R M₁ M₂ M₃).symm ∘ₗ TensorProduct.map LinearMap.id f₂₃ ∘ₗ f

def CoassocSimps.assoc_symm_comp_map_assoc_simproc : Lean.Meta.Simp.Simproc

Simproc version of assoc_symm_comp_map_assoc that only fires when f₁ ≠ id.

Equations

• One or more equations did not get rendered due to their size.

theorem CoassocSimps.assoc_symm_comp_map_map_comp {R : Type u_1} {M : Type u_3} {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15} {N₃ : Type u_16} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃] [Module R M₁] [Module R M₂] [Module R M₃] [Module R N₁] [Module R N₂] [Module R N₃] (f₁ : M₁ →ₗ[R] N₁) (f₂ : M₂ →ₗ[R] N₂) (f₃ : M₃ →ₗ[R] N₃) (f₂₃ : M →ₗ[R] TensorProduct R M₂ M₃) : ↑(TensorProduct.assoc R N₁ N₂ N₃).symm ∘ₗ TensorProduct.map f₁ (TensorProduct.map f₂ f₃ ∘ₗ f₂₃) = TensorProduct.map (TensorProduct.map f₁ f₂) f₃ ∘ₗ ↑(TensorProduct.assoc R M₁ M₂ M₃).symm ∘ₗ TensorProduct.map LinearMap.id f₂₃

theorem CoassocSimps.assoc_symm_comp_map_map_comp_assoc {R : Type u_1} {M : Type u_3} {N : Type u_4} {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15} {N₃ : Type u_16} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃] [Module R M₁] [Module R M₂] [Module R M₃] [Module R N₁] [Module R N₂] [Module R N₃] (f₁ : M₁ →ₗ[R] N₁) (f₂ : M₂ →ₗ[R] N₂) (f₃ : M₃ →ₗ[R] N₃) (f₂₃ : M →ₗ[R] TensorProduct R M₂ M₃) (f : N →ₗ[R] TensorProduct R M₁ M) : ↑(TensorProduct.assoc R N₁ N₂ N₃).symm ∘ₗ TensorProduct.map f₁ (TensorProduct.map f₂ f₃ ∘ₗ f₂₃) ∘ₗ f = TensorProduct.map (TensorProduct.map f₁ f₂) f₃ ∘ₗ ↑(TensorProduct.assoc R M₁ M₂ M₃).symm ∘ₗ TensorProduct.map LinearMap.id f₂₃ ∘ₗ f

theorem CoassocSimps.assoc_symm_comp_lid_symm {R : Type u_1} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : ↑(TensorProduct.assoc R R M N).symm ∘ₗ ↑(TensorProduct.lid R (TensorProduct R M N)).symm = TensorProduct.map (↑(TensorProduct.lid R M).symm) LinearMap.id

theorem CoassocSimps.assoc_symm_comp_lid_symm_assoc {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (f : P →ₗ[R] TensorProduct R M N) : ↑(TensorProduct.assoc R R M N).symm ∘ₗ ↑(TensorProduct.lid R (TensorProduct R M N)).symm ∘ₗ f = TensorProduct.map (↑(TensorProduct.lid R M).symm) LinearMap.id ∘ₗ f

theorem CoassocSimps.assoc_symm_comp_map_lid_symm {R : Type u_1} {M : Type u_3} {N : Type u_4} {M' : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') : ↑(TensorProduct.assoc R M' R N).symm ∘ₗ TensorProduct.map f ↑(TensorProduct.lid R N).symm = TensorProduct.map (TensorProduct.map f LinearMap.id ∘ₗ ↑(TensorProduct.rid R M).symm) LinearMap.id

theorem CoassocSimps.assoc_symm_comp_map_lid_symm_assoc {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (g : P →ₗ[R] TensorProduct R M N) : ↑(TensorProduct.assoc R M' R N).symm ∘ₗ TensorProduct.map f ↑(TensorProduct.lid R N).symm ∘ₗ g = TensorProduct.map (TensorProduct.map f LinearMap.id ∘ₗ ↑(TensorProduct.rid R M).symm) LinearMap.id ∘ₗ g

theorem CoassocSimps.assoc_symm_comp_map_rid_symm {R : Type u_1} {M : Type u_3} {N : Type u_4} {M' : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') : ↑(TensorProduct.assoc R M' N R).symm ∘ₗ TensorProduct.map f ↑(TensorProduct.rid R N).symm = TensorProduct.map (TensorProduct.map f LinearMap.id) LinearMap.id ∘ₗ ↑(TensorProduct.rid R (TensorProduct R M N)).symm

theorem CoassocSimps.assoc_symm_comp_map_rid_symm_assoc {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (g : P →ₗ[R] TensorProduct R M N) : ↑(TensorProduct.assoc R M' N R).symm ∘ₗ TensorProduct.map f ↑(TensorProduct.rid R N).symm ∘ₗ g = TensorProduct.map (TensorProduct.map f LinearMap.id) LinearMap.id ∘ₗ ↑(TensorProduct.rid R (TensorProduct R M N)).symm ∘ₗ g

theorem CoassocSimps.assoc_comp_rid_symm {R : Type u_1} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : ↑(TensorProduct.assoc R M N R) ∘ₗ ↑(TensorProduct.rid R (TensorProduct R M N)).symm = TensorProduct.map LinearMap.id ↑(TensorProduct.rid R N).symm

theorem CoassocSimps.assoc_comp_rid_symm_assoc {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (f : P →ₗ[R] TensorProduct R M N) : ↑(TensorProduct.assoc R M N R) ∘ₗ ↑(TensorProduct.rid R (TensorProduct R M N)).symm ∘ₗ f = TensorProduct.map LinearMap.id ↑(TensorProduct.rid R N).symm ∘ₗ f

theorem CoassocSimps.assoc_comp_map_lid_symm {R : Type u_1} {M : Type u_3} {N : Type u_4} {N' : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid N'] [Module R N'] (f : N →ₗ[R] N') : ↑(TensorProduct.assoc R R M N') ∘ₗ TensorProduct.map (↑(TensorProduct.lid R M).symm) f = TensorProduct.map LinearMap.id (TensorProduct.map LinearMap.id f) ∘ₗ ↑(TensorProduct.lid R (TensorProduct R M N)).symm

theorem CoassocSimps.assoc_comp_map_lid_symm_assoc {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} {N' : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [AddCommMonoid N'] [Module R N'] (f : N →ₗ[R] N') (g : P →ₗ[R] TensorProduct R M N) : ↑(TensorProduct.assoc R R M N') ∘ₗ TensorProduct.map (↑(TensorProduct.lid R M).symm) f ∘ₗ g = TensorProduct.map LinearMap.id (TensorProduct.map LinearMap.id f) ∘ₗ ↑(TensorProduct.lid R (TensorProduct R M N)).symm ∘ₗ g

theorem CoassocSimps.assoc_comp_map_rid_symm {R : Type u_1} {M : Type u_3} {N : Type u_4} {N' : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid N'] [Module R N'] (f : N →ₗ[R] N') : ↑(TensorProduct.assoc R M R N') ∘ₗ TensorProduct.map (↑(TensorProduct.rid R M).symm) f = TensorProduct.map LinearMap.id (TensorProduct.map LinearMap.id f ∘ₗ ↑(TensorProduct.lid R N).symm)

theorem CoassocSimps.assoc_comp_map_rid_symm_assoc {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} {N' : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [AddCommMonoid N'] [Module R N'] (f : N →ₗ[R] N') (g : P →ₗ[R] TensorProduct R M N) : ↑(TensorProduct.assoc R M R N') ∘ₗ TensorProduct.map (↑(TensorProduct.rid R M).symm) f ∘ₗ g = TensorProduct.map LinearMap.id (TensorProduct.map LinearMap.id f ∘ₗ ↑(TensorProduct.lid R N).symm) ∘ₗ g

theorem CoassocSimps.lid_comp_map {R : Type u_1} {M : Type u_3} {N : Type u_4} {M' : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] R) (g : N →ₗ[R] M') : ↑(TensorProduct.lid R M') ∘ₗ TensorProduct.map f g = g ∘ₗ ↑(TensorProduct.lid R N) ∘ₗ TensorProduct.map f LinearMap.id

def CoassocSimps.lid_comp_map_simproc : Lean.Meta.Simp.Simproc

Simproc version of lid_comp_map that only fires when g ≠ id.

Equations

• One or more equations did not get rendered due to their size.

theorem CoassocSimps.lid_comp_map_assoc {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] R) (g : N →ₗ[R] M') (h : P →ₗ[R] TensorProduct R M N) : ↑(TensorProduct.lid R M') ∘ₗ TensorProduct.map f g ∘ₗ h = g ∘ₗ ↑(TensorProduct.lid R N) ∘ₗ TensorProduct.map f LinearMap.id ∘ₗ h

def CoassocSimps.lid_comp_map_assoc_simproc : Lean.Meta.Simp.Simproc

Simproc version of lid_comp_map_assoc that only fires when g ≠ id.

Equations

• One or more equations did not get rendered due to their size.

theorem CoassocSimps.rid_comp_map {R : Type u_1} {M : Type u_3} {N : Type u_4} {M' : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (g : N →ₗ[R] R) : ↑(TensorProduct.rid R M') ∘ₗ TensorProduct.map f g = f ∘ₗ ↑(TensorProduct.rid R M) ∘ₗ TensorProduct.map LinearMap.id g

def CoassocSimps.rid_comp_map_simproc : Lean.Meta.Simp.Simproc

Simproc version of rid_comp_map that only fires when g ≠ id.

Equations

• One or more equations did not get rendered due to their size.

theorem CoassocSimps.rid_comp_map_assoc {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (g : N →ₗ[R] R) (h : P →ₗ[R] TensorProduct R M N) : ↑(TensorProduct.rid R M') ∘ₗ TensorProduct.map f g ∘ₗ h = f ∘ₗ ↑(TensorProduct.rid R M) ∘ₗ TensorProduct.map LinearMap.id g ∘ₗ h

def CoassocSimps.rid_comp_map_assoc_simproc : Lean.Meta.Simp.Simproc

Simproc version of rid_comp_map_assoc that only fires when f ≠ id.

Equations

• One or more equations did not get rendered due to their size.

theorem CoassocSimps.lid_symm_comp {R : Type u_1} {M : Type u_3} {M' : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') : ↑(TensorProduct.lid R M').symm ∘ₗ f = TensorProduct.map LinearMap.id f ∘ₗ ↑(TensorProduct.lid R M).symm

theorem CoassocSimps.rid_symm_comp {R : Type u_1} {M : Type u_3} {M' : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') : ↑(TensorProduct.rid R M').symm ∘ₗ f = TensorProduct.map f LinearMap.id ∘ₗ ↑(TensorProduct.rid R M).symm

theorem CoassocSimps.symm_comp_lid_symm {R : Type u_1} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] : ↑(TensorProduct.comm R R M) ∘ₗ ↑(TensorProduct.lid R M).symm = ↑(TensorProduct.rid R M).symm

theorem CoassocSimps.symm_comp_lid_symm_assoc {R : Type u_1} {M : Type u_3} {M' : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') : ↑(TensorProduct.comm R R M') ∘ₗ ↑(TensorProduct.lid R M').symm ∘ₗ f = ↑(TensorProduct.rid R M').symm ∘ₗ f

theorem CoassocSimps.symm_comp_rid_symm {R : Type u_1} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] : ↑(TensorProduct.comm R M R) ∘ₗ ↑(TensorProduct.rid R M).symm = ↑(TensorProduct.lid R M).symm

theorem CoassocSimps.symm_comp_rid_symm_assoc {R : Type u_1} {M : Type u_3} {M' : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') : ↑(TensorProduct.comm R M' R) ∘ₗ ↑(TensorProduct.rid R M').symm ∘ₗ f = ↑(TensorProduct.lid R M').symm ∘ₗ f

theorem CoassocSimps.symm_comp_map {R : Type u_1} {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid M'] [Module R M'] [AddCommMonoid N'] [Module R N'] (f : M →ₗ[R] M') (g : N →ₗ[R] N') : ↑(TensorProduct.comm R M' N') ∘ₗ TensorProduct.map f g = TensorProduct.map g f ∘ₗ ↑(TensorProduct.comm R M N)

theorem CoassocSimps.symm_comp_map_assoc {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} {N' : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [AddCommMonoid M'] [Module R M'] [AddCommMonoid N'] [Module R N'] (f : M →ₗ[R] M') (g : N →ₗ[R] N') (h : P →ₗ[R] TensorProduct R M N) : ↑(TensorProduct.comm R M' N') ∘ₗ TensorProduct.map f g ∘ₗ h = TensorProduct.map g f ∘ₗ ↑(TensorProduct.comm R M N) ∘ₗ h

theorem CoassocSimps.coassoc_left {R : Type u_1} {M : Type u_3} {M' : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] [Coalgebra R M] (f : M →ₗ[R] M') : ↑(TensorProduct.assoc R M M M') ∘ₗ TensorProduct.map CoalgebraStruct.comul f ∘ₗ CoalgebraStruct.comul = TensorProduct.map LinearMap.id (TensorProduct.map LinearMap.id f) ∘ₗ TensorProduct.map LinearMap.id CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul

theorem CoassocSimps.coassoc_left_assoc {R : Type u_1} {M : Type u_3} {N : Type u_4} {M' : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid M'] [Module R M'] [Coalgebra R M] (f : M →ₗ[R] M') (g : N →ₗ[R] M) : ↑(TensorProduct.assoc R M M M') ∘ₗ TensorProduct.map CoalgebraStruct.comul f ∘ₗ CoalgebraStruct.comul ∘ₗ g = TensorProduct.map LinearMap.id (TensorProduct.map LinearMap.id f) ∘ₗ TensorProduct.map LinearMap.id CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul ∘ₗ g

theorem CoassocSimps.coassoc_right {R : Type u_1} {M : Type u_3} {M' : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] [Coalgebra R M] (f : M →ₗ[R] M') : ↑(TensorProduct.assoc R M' M M).symm ∘ₗ TensorProduct.map f CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul = TensorProduct.map (TensorProduct.map f LinearMap.id) LinearMap.id ∘ₗ TensorProduct.map CoalgebraStruct.comul LinearMap.id ∘ₗ CoalgebraStruct.comul

theorem CoassocSimps.coassoc_right_assoc {R : Type u_1} {M : Type u_3} {N : Type u_4} {M' : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid M'] [Module R M'] [Coalgebra R M] (f : M →ₗ[R] M') (g : N →ₗ[R] M) : ↑(TensorProduct.assoc R M' M M).symm ∘ₗ TensorProduct.map f CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul ∘ₗ g = TensorProduct.map (TensorProduct.map f LinearMap.id) LinearMap.id ∘ₗ TensorProduct.map CoalgebraStruct.comul LinearMap.id ∘ₗ CoalgebraStruct.comul ∘ₗ g

theorem CoassocSimps.map_counit_comp_comul_left {R : Type u_1} {M : Type u_3} {M' : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] [Coalgebra R M] (f : M →ₗ[R] M') : TensorProduct.map CoalgebraStruct.counit f ∘ₗ CoalgebraStruct.comul = TensorProduct.map LinearMap.id f ∘ₗ ↑(TensorProduct.lid R M).symm

theorem CoassocSimps.map_counit_comp_comul_left_assoc {R : Type u_1} {M : Type u_3} {P : Type u_5} {M' : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] [AddCommMonoid M'] [Module R M'] [Coalgebra R M] (f : M →ₗ[R] M') (g : P →ₗ[R] M) : TensorProduct.map CoalgebraStruct.counit f ∘ₗ CoalgebraStruct.comul ∘ₗ g = TensorProduct.map LinearMap.id f ∘ₗ ↑(TensorProduct.lid R M).symm ∘ₗ g

theorem CoassocSimps.map_counit_comp_comul_right {R : Type u_1} {M : Type u_3} {M' : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] [Coalgebra R M] (f : M →ₗ[R] M') : TensorProduct.map f CoalgebraStruct.counit ∘ₗ CoalgebraStruct.comul = TensorProduct.map f LinearMap.id ∘ₗ ↑(TensorProduct.rid R M).symm

theorem CoassocSimps.map_counit_comp_comul_right_assoc {R : Type u_1} {M : Type u_3} {P : Type u_5} {M' : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] [AddCommMonoid M'] [Module R M'] [Coalgebra R M] (f : M →ₗ[R] M') (g : P →ₗ[R] M) : TensorProduct.map f CoalgebraStruct.counit ∘ₗ CoalgebraStruct.comul ∘ₗ g = TensorProduct.map f LinearMap.id ∘ₗ ↑(TensorProduct.rid R M).symm ∘ₗ g

theorem CoassocSimps.assoc_comp_map_comm_comp_comul_comp_comul {R : Type u_1} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Coalgebra R M] (f : M →ₗ[R] N) : ↑(TensorProduct.assoc R M M N) ∘ₗ TensorProduct.map (↑(TensorProduct.comm R M M) ∘ₗ CoalgebraStruct.comul) f ∘ₗ CoalgebraStruct.comul = TensorProduct.map LinearMap.id (TensorProduct.map LinearMap.id f ∘ₗ ↑(TensorProduct.comm R M M)) ∘ₗ ↑(TensorProduct.assoc R M M M) ∘ₗ TensorProduct.map CoalgebraStruct.comul LinearMap.id ∘ₗ ↑(TensorProduct.comm R M M) ∘ₗ CoalgebraStruct.comul

theorem CoassocSimps.assoc_comp_map_comm_comp_comul_comp_comul_assoc {R : Type u_1} {M : Type u_3} {N : Type u_4} {Q : Type u_9} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid Q] [Module R Q] [Coalgebra R M] (f : M →ₗ[R] N) (h : Q →ₗ[R] M) : ↑(TensorProduct.assoc R M M N) ∘ₗ TensorProduct.map (↑(TensorProduct.comm R M M) ∘ₗ CoalgebraStruct.comul) f ∘ₗ CoalgebraStruct.comul ∘ₗ h = TensorProduct.map LinearMap.id (TensorProduct.map LinearMap.id f ∘ₗ ↑(TensorProduct.comm R M M)) ∘ₗ ↑(TensorProduct.assoc R M M M) ∘ₗ TensorProduct.map CoalgebraStruct.comul LinearMap.id ∘ₗ ↑(TensorProduct.comm R M M) ∘ₗ CoalgebraStruct.comul ∘ₗ h