Tactic to reassociate comultiplication in a coalgebra #
theorem
Coalgebra.comp_assoc_symm
{R : Type u_1}
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
{Q : Type u_9}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
[AddCommMonoid P]
[Module R P]
[AddCommMonoid Q]
[Module R Q]
(f₁ : M →ₗ[R] N)
(f₂ : N →ₗ[R] P)
(f₃ : P →ₗ[R] Q)
:
theorem
Coalgebra.map_comp_left
{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] N)
(f₂ : N →ₗ[R] P)
(g : M' →ₗ[R] N')
:
theorem
Coalgebra.map_comp_right
{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] N)
(f₂ : N →ₗ[R] P)
(g : M' →ₗ[R] N')
:
theorem
Coalgebra.map_comul_right_comp_comul
{R : Type u_1}
{A : Type u_2}
{M : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[Coalgebra R A]
[AddCommMonoid M]
[Module R M]
(f : A →ₗ[R] M)
:
TensorProduct.map f comul ∘ₗ comul = ↑(TensorProduct.assoc R M A A) ∘ₗ LinearMap.rTensor A (LinearMap.rTensor A f) ∘ₗ LinearMap.rTensor A comul ∘ₗ comul
theorem
Coalgebra.map_comul_right_comp_comul_assoc
{R : Type u_1}
{A : Type u_2}
{M : Type u_3}
{P : Type u_5}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[Coalgebra R A]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid P]
[Module R P]
(f : A →ₗ[R] M)
(h : TensorProduct R M (TensorProduct R A A) →ₗ[R] P)
:
(h ∘ₗ TensorProduct.map f comul) ∘ₗ comul = h ∘ₗ ↑(TensorProduct.assoc R M A A) ∘ₗ LinearMap.rTensor A (LinearMap.rTensor A f) ∘ₗ LinearMap.rTensor A comul ∘ₗ comul
theorem
Coalgebra.map_comp_comul_right_comp_comul
{R : Type u_1}
{A : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[Coalgebra R A]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
(f : A →ₗ[R] M)
(g : TensorProduct R A A →ₗ[R] N)
:
TensorProduct.map f (g ∘ₗ comul) ∘ₗ comul = LinearMap.lTensor M g ∘ₗ ↑(TensorProduct.assoc R M A A) ∘ₗ LinearMap.rTensor A (LinearMap.rTensor A f) ∘ₗ LinearMap.rTensor A comul ∘ₗ comul
theorem
Coalgebra.map_comp_comul_right_comp_comul_assoc
{R : Type u_1}
{A : Type u_2}
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[Coalgebra R A]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
[AddCommMonoid P]
[Module R P]
(f : A →ₗ[R] M)
(g : TensorProduct R A A →ₗ[R] N)
(h : TensorProduct R M N →ₗ[R] P)
:
(h ∘ₗ TensorProduct.map f (g ∘ₗ comul)) ∘ₗ comul = h ∘ₗ LinearMap.lTensor M g ∘ₗ ↑(TensorProduct.assoc R M A A) ∘ₗ LinearMap.rTensor A (LinearMap.rTensor A f) ∘ₗ LinearMap.rTensor A comul ∘ₗ comul
theorem
Coalgebra.map_map
{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}
[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']
(f₁ : M →ₗ[R] N)
(f₂ : N →ₗ[R] P)
(g₁ : M' →ₗ[R] N')
(g₂ : N' →ₗ[R] P')
:
theorem
Coalgebra.map_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}
{P' : Type u_8}
{Q : Type u_9}
[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 Q]
[Module R Q]
(f₁ : M →ₗ[R] N)
(f₂ : N →ₗ[R] P)
(g₁ : M' →ₗ[R] N')
(g₂ : N' →ₗ[R] P')
(h : TensorProduct R P P' →ₗ[R] Q)
:
(h ∘ₗ TensorProduct.map f₂ g₂) ∘ₗ TensorProduct.map f₁ g₁ = h ∘ₗ TensorProduct.map (f₂ ∘ₗ f₁) (g₂ ∘ₗ g₁)
theorem
Coalgebra.map_id_id
{R : Type u_1}
{M : Type u_3}
{N : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
:
theorem
Coalgebra.map_map_comp_assoc_eq_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}
{Q : Type u_9}
[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 Q]
[Module R Q]
(f : M →ₗ[R] M')
(g : N →ₗ[R] N')
(h : P →ₗ[R] P')
(i : TensorProduct R M' (TensorProduct R N' P') →ₗ[R] Q)
:
(i ∘ₗ TensorProduct.map f (TensorProduct.map g h)) ∘ₗ ↑(TensorProduct.assoc R M N P) = i ∘ₗ ↑(TensorProduct.assoc R M' N' P') ∘ₗ TensorProduct.map (TensorProduct.map f g) h
theorem
Coalgebra.map_map_comp_assoc_eq_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}
{Q : Type u_9}
{Q' : Type u_10}
[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 Q]
[Module R Q]
[AddCommMonoid Q']
[Module R Q']
(f : M →ₗ[R] M')
(g : N →ₗ[R] N')
(h : P →ₗ[R] P')
(i₁ : TensorProduct R M' Q' →ₗ[R] Q)
(i₂ : TensorProduct R N' P' →ₗ[R] Q')
:
(i₁ ∘ₗ TensorProduct.map f (i₂ ∘ₗ TensorProduct.map g h)) ∘ₗ ↑(TensorProduct.assoc R M N P) = i₁ ∘ₗ LinearMap.lTensor M' i₂ ∘ₗ ↑(TensorProduct.assoc R M' N' P') ∘ₗ TensorProduct.map (TensorProduct.map f g) h
theorem
Coalgebra.map_map_comp_assoc_eq_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}
{Q' : Type u_10}
[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 Q']
[Module R Q']
(f : M →ₗ[R] M')
(g : N →ₗ[R] N')
(h : P →ₗ[R] P')
(i₂ : TensorProduct R N' P' →ₗ[R] Q')
:
TensorProduct.map f (i₂ ∘ₗ TensorProduct.map g h) ∘ₗ ↑(TensorProduct.assoc R M N P) = LinearMap.lTensor M' i₂ ∘ₗ ↑(TensorProduct.assoc R M' N' P') ∘ₗ TensorProduct.map (TensorProduct.map f g) h
theorem
Coalgebra.map_map_comp_assoc_symm_eq_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}
{Q : Type u_9}
[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 Q]
[Module R Q]
(f : M →ₗ[R] M')
(g : N →ₗ[R] N')
(h : P →ₗ[R] P')
(i : TensorProduct R (TensorProduct R M' N') P' →ₗ[R] Q)
:
(i ∘ₗ TensorProduct.map (TensorProduct.map f g) h) ∘ₗ ↑(TensorProduct.assoc R M N P).symm = i ∘ₗ ↑(TensorProduct.assoc R M' N' P').symm ∘ₗ TensorProduct.map f (TensorProduct.map g h)
theorem
Coalgebra.map_map_comp_assoc_symm_eq_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}
{Q : Type u_9}
{Q' : Type u_10}
[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 Q]
[Module R Q]
[AddCommMonoid Q']
[Module R Q']
(f : M →ₗ[R] M')
(g : N →ₗ[R] N')
(h : P →ₗ[R] P')
(i₁ : TensorProduct R Q' P' →ₗ[R] Q)
(i₂ : TensorProduct R M' N' →ₗ[R] Q')
:
(i₁ ∘ₗ TensorProduct.map (i₂ ∘ₗ TensorProduct.map f g) h) ∘ₗ ↑(TensorProduct.assoc R M N P).symm = i₁ ∘ₗ LinearMap.rTensor P' i₂ ∘ₗ ↑(TensorProduct.assoc R M' N' P').symm ∘ₗ TensorProduct.map f (TensorProduct.map g h)
theorem
Coalgebra.map_map_comp_assoc_symm_eq_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}
{Q' : Type u_10}
[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 Q']
[Module R Q']
(f : M →ₗ[R] M')
(g : N →ₗ[R] N')
(h : P →ₗ[R] P')
(i₂ : TensorProduct R M' N' →ₗ[R] Q')
:
TensorProduct.map (i₂ ∘ₗ TensorProduct.map f g) h ∘ₗ ↑(TensorProduct.assoc R M N P).symm = LinearMap.rTensor P' i₂ ∘ₗ ↑(TensorProduct.assoc R M' N' P').symm ∘ₗ TensorProduct.map f (TensorProduct.map g h)
coassoc_simps reassociates attempts to replace x by
x₁ ⊗ₜ x₂ via linearity. This is an implementation detail that is used to set up tensor products
of coalgebras, bialgebras, and hopf algebras, and shouldn't be relied on downstream.
Equations
- Coalgebra.tacticCoassoc_simps = Lean.ParserDescr.node `Coalgebra.tacticCoassoc_simps 1024 (Lean.ParserDescr.nonReservedSymbol "coassoc_simps" false)