LeanPool.Monlib4.LinearAlgebra.Coalgebra.Lemmas #

Imported Lean Pool material for LeanPool.Monlib4.LinearAlgebra.Coalgebra.Lemmas.

theorem TensorProduct.map_left_up {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (f : A →ₗ[R] B) (g : C →ₗ[R] D) :

map f g = map f LinearMap.id ∘ₗ map LinearMap.id g

source

theorem TensorProduct.map_right_down {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (f : A →ₗ[R] B) (g : C →ₗ[R] D) :

map f g = map f LinearMap.id ∘ₗ map LinearMap.id g

Alias of TensorProduct.map_left_up.

source

theorem TensorProduct.map_right_up {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (f : A →ₗ[R] B) (g : C →ₗ[R] D) :

map f g = map LinearMap.id g ∘ₗ map f LinearMap.id

source

theorem TensorProduct.map_left_down {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (f : A →ₗ[R] B) (g : C →ₗ[R] D) :

map f g = map LinearMap.id g ∘ₗ map f LinearMap.id

Alias of TensorProduct.map_right_up.

source

theorem Algebra.linearMap_mul'_assoc {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :

LinearMap.mul' R A ∘ₗ _root_.TensorProduct.map (LinearMap.mul' R A) LinearMap.id = LinearMap.mul' R A ∘ₗ _root_.TensorProduct.map LinearMap.id (LinearMap.mul' R A) ∘ₗ ↑(_root_.TensorProduct.assoc R A A A)

source

theorem Algebra.assoc {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :

Alias of Algebra.linearMap_mul'_assoc.

source

theorem Algebra.assoc' {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :

LinearMap.mul' R A ∘ₗ LinearMap.rTensor A (LinearMap.mul' R A) = LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (LinearMap.mul' R A) ∘ₗ ↑(_root_.TensorProduct.assoc R A A A)

source

theorem Algebra.mul_comp_rTensor_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :

LinearMap.mul' R A ∘ₗ LinearMap.rTensor A (LinearMap.mul' R A) = LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (LinearMap.mul' R A) ∘ₗ ↑(_root_.TensorProduct.assoc R A A A)

Alias of Algebra.assoc'.

source

theorem Algebra.mul_comp_rTensor_unit {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :

LinearMap.mul' R A ∘ₗ LinearMap.rTensor A (Algebra.linearMap R A) = ↑(_root_.TensorProduct.lid R A)

source

theorem Algebra.mul_comp_rTensor_unit_comp_lid_symm {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :

LinearMap.mul' R A ∘ₗ LinearMap.rTensor A (Algebra.linearMap R A) ∘ₗ ↑(_root_.TensorProduct.lid R A).symm = LinearMap.id

source

theorem Algebra.mul_comp_lTensor_unit {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :

LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (Algebra.linearMap R A) = ↑(_root_.TensorProduct.rid R A)

source

theorem Algebra.mul_comp_lTensor_unit_comp_rid_symm {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :

LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (Algebra.linearMap R A) ∘ₗ ↑(_root_.TensorProduct.rid R A).symm = LinearMap.id

source

theorem counit_comp_mul_comp_rTensor_unit {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [Coalgebra R A] :

CoalgebraStruct.counit ∘ₗ LinearMap.mul' R A ∘ₗ LinearMap.rTensor A (Algebra.linearMap R A) ∘ₗ ↑(TensorProduct.lid R A).symm = CoalgebraStruct.counit

source

theorem counit_comp_mul_lTensor_unit {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [Coalgebra R A] :

CoalgebraStruct.counit ∘ₗ LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (Algebra.linearMap R A) ∘ₗ ↑(TensorProduct.rid R A).symm = CoalgebraStruct.counit

source

theorem lTensor_counit_comp_comul_unit {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [Coalgebra R A] :

LinearMap.lTensor A CoalgebraStruct.counit ∘ₗ CoalgebraStruct.comul ∘ₗ Algebra.linearMap R A = ↑(TensorProduct.rid R A).symm ∘ₗ Algebra.linearMap R A

source

theorem Coalgebra.rTensor_counit_comp_comul' {R : Type u_1} [CommSemiring R] {A : Type u_2} [AddCommMonoid A] [Module R A] [Coalgebra R A] :

LinearMap.rTensor A counit ∘ₗ comul = ↑(TensorProduct.lid R A).symm

source

theorem TensorProduct.assoc_symm_comp_rTensor {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (x : A →ₗ[R] D) :

↑(TensorProduct.assoc R D B C).symm ∘ₗ LinearMap.rTensor (TensorProduct R B C) x = LinearMap.rTensor C (LinearMap.rTensor B x) ∘ₗ ↑(TensorProduct.assoc R A B C).symm

source

theorem TensorProduct.assoc_symm_comp_lTensor_lTensor {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (x : A →ₗ[R] D) :

↑(TensorProduct.assoc R B C D).symm ∘ₗ LinearMap.lTensor B (LinearMap.lTensor C x) = LinearMap.lTensor (TensorProduct R B C) x ∘ₗ ↑(TensorProduct.assoc R B C A).symm

source

theorem TensorProduct.rTensor_lTensor_comp_assoc_symm {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (x : A →ₗ[R] D) :

LinearMap.rTensor C (LinearMap.lTensor B x) ∘ₗ ↑(TensorProduct.assoc R B A C).symm = ↑(TensorProduct.assoc R B D C).symm ∘ₗ LinearMap.lTensor B (LinearMap.rTensor C x)

source

theorem TensorProduct.assoc_comp_rTensor_rTensor {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (x : A →ₗ[R] D) :

↑(TensorProduct.assoc R D B C) ∘ₗ LinearMap.rTensor C (LinearMap.rTensor B x) = LinearMap.rTensor (TensorProduct R B C) x ∘ₗ ↑(TensorProduct.assoc R A B C)

source

theorem TensorProduct.ext_fourfold_right {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} {E : Type u_6} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [AddCommMonoid E] [Module R A] [Module R B] [Module R C] [Module R D] [Module R E] {f g : TensorProduct R A (TensorProduct R B (TensorProduct R C D)) →ₗ[R] E} :

(∀ (x : A) (y : B) (z : C) (w : D), f (x ⊗ₜ[R] (y ⊗ₜ[R] (z ⊗ₜ[R] w))) = g (x ⊗ₜ[R] (y ⊗ₜ[R] (z ⊗ₜ[R] w)))) → f = g

source

theorem TensorProduct.assoc_comp_rTensor_assoc_symm_comp_assoc_symm_comp_lTensor_assoc_symm {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] :

↑(TensorProduct.assoc R (TensorProduct R A B) C D) ∘ₗ LinearMap.rTensor D ↑(TensorProduct.assoc R A B C).symm ∘ₗ ↑(TensorProduct.assoc R A (TensorProduct R B C) D).symm ∘ₗ LinearMap.lTensor A ↑(TensorProduct.assoc R B C D).symm = ↑(TensorProduct.assoc R A B (TensorProduct R C D)).symm

source

theorem TensorProduct.rTensor_comp_rTensor {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (x : B →ₗ[R] C) (y : A →ₗ[R] B) :

LinearMap.rTensor D x ∘ₗ LinearMap.rTensor D y = LinearMap.rTensor D (x ∘ₗ y)

source

theorem TensorProduct.lTensor_comp_lTensor {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (x : B →ₗ[R] C) (y : A →ₗ[R] B) :

LinearMap.lTensor D x ∘ₗ LinearMap.lTensor D y = LinearMap.lTensor D (x ∘ₗ y)

source

theorem lid_tensor_toLinearMap {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] :

↑(TensorProduct.lid R (TensorProduct R A B)) = LinearMap.rTensor B ↑(TensorProduct.lid R A) ∘ₗ ↑(TensorProduct.assoc R R A B).symm

source

theorem lid_tensor {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] :

↑(TensorProduct.lid R (TensorProduct R A B)) = LinearMap.rTensor B ↑(TensorProduct.lid R A) ∘ₗ ↑(TensorProduct.assoc R R A B).symm

source

theorem rTensor_comp_lTensor' {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (x : A →ₗ[R] B) (y : C →ₗ[R] D) :

LinearMap.rTensor D x ∘ₗ LinearMap.lTensor A y = LinearMap.lTensor B y ∘ₗ LinearMap.rTensor C x

source

theorem lTensor_mul_comp_rTensor_comul_of {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] [Coalgebra R A] (h : LinearMap.lTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A CoalgebraStruct.comul = LinearMap.rTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm ∘ₗ LinearMap.lTensor A CoalgebraStruct.comul) :

LinearMap.lTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ LinearMap.mul' R A

if (id ⊗ mul) (comul ⊗ id) = (mul ⊗ id) (id ⊗ comul), then (id ⊗ mul) (comul ⊗ id) = comul ∘ mul.

This is sometimes referred to as the Frobenius equations.

source

theorem counit_comp_mul_comp_rTensor_unit_eq_counit {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] [Coalgebra R A] :

CoalgebraStruct.counit ∘ₗ LinearMap.mul' R A ∘ₗ LinearMap.rTensor A (Algebra.linearMap R A) = CoalgebraStruct.counit ∘ₗ ↑(TensorProduct.lid R A)

source

theorem counit_comp_mul_comp_lTensor_unit_eq_counit {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] [Coalgebra R A] :

CoalgebraStruct.counit ∘ₗ LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (Algebra.linearMap R A) = CoalgebraStruct.counit ∘ₗ ↑(TensorProduct.rid R A)

source

theorem rTensor_counit_comp_comul_comp_unit_eq_unit {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] [Coalgebra R A] :

LinearMap.rTensor A CoalgebraStruct.counit ∘ₗ CoalgebraStruct.comul ∘ₗ Algebra.linearMap R A = ↑(TensorProduct.lid R A).symm ∘ₗ Algebra.linearMap R A

source

theorem lTensor_counit_comp_comul_comp_unit_eq_unit {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] [Coalgebra R A] :

LinearMap.lTensor A CoalgebraStruct.counit ∘ₗ CoalgebraStruct.comul ∘ₗ Algebra.linearMap R A = ↑(TensorProduct.rid R A).symm ∘ₗ Algebra.linearMap R A

source

class FrobeniusAlgebra (R : Type u_3) (A : Type u_4) [CommSemiring R] [Semiring A] extends Algebra R A, Coalgebra R A :

Type (max u_3 u_4)

An algebra and coalgebra with the Frobenius tensor compatibility law.

smul : R → A → A
algebraMap : R →+* A
commutes' (r : R) (x : A) : (algebraMap R A) r * x = x * (algebraMap R A) r
smul_def' (r : R) (x : A) : r • x = (algebraMap R A) r * x
comul : A →ₗ[R] TensorProduct R A A
counit : A →ₗ[R] R
coassoc : ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A comul ∘ₗ comul = LinearMap.lTensor A comul ∘ₗ comul
rTensor_counit_comp_comul : LinearMap.rTensor A counit ∘ₗ comul = (TensorProduct.mk R R A) 1
lTensor_counit_comp_comul : LinearMap.lTensor A counit ∘ₗ comul = (TensorProduct.mk R A R).flip 1
lTensor_mul_comp_rTensor_comul_commute : LinearMap.lTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A CoalgebraStruct.comul = LinearMap.rTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm ∘ₗ LinearMap.lTensor A CoalgebraStruct.comul

Instances

source

theorem FrobeniusAlgebra.lTensor_mul_comp_rTensor_comul_eq_comul_comp_mul {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [FrobeniusAlgebra R A] :

LinearMap.lTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ LinearMap.mul' R A

source

theorem FrobeniusAlgebra.rTensor_mul_comp_lTensor_comul_eq_comul_comp_mul {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [FrobeniusAlgebra R A] :

LinearMap.rTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm ∘ₗ LinearMap.lTensor A CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ LinearMap.mul' R A

source

theorem FrobeniusAlgebra.rTensor_mul_comp_lTensor_comul_unit_eq_comul {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [FrobeniusAlgebra R A] :

LinearMap.rTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm ∘ₗ LinearMap.lTensor A (CoalgebraStruct.comul ∘ₗ Algebra.linearMap R A) = CoalgebraStruct.comul ∘ₗ ↑(TensorProduct.rid R A)

source

theorem FrobeniusAlgebra.lTensor_mul_comp_rTensor_comul_unit {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [FrobeniusAlgebra R A] :

LinearMap.lTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A (CoalgebraStruct.comul ∘ₗ Algebra.linearMap R A) = CoalgebraStruct.comul ∘ₗ ↑(TensorProduct.lid R A)

source

theorem FrobeniusAlgebra.rTensor_counit_mul_comp_lTensor_comul {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [FrobeniusAlgebra R A] :

LinearMap.rTensor A (CoalgebraStruct.counit ∘ₗ LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm ∘ₗ LinearMap.lTensor A CoalgebraStruct.comul = ↑(TensorProduct.lid R A).symm ∘ₗ LinearMap.mul' R A

source

theorem FrobeniusAlgebra.lTensor_counit_mul_comp_rTensor_comul {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [FrobeniusAlgebra R A] :

LinearMap.lTensor A (CoalgebraStruct.counit ∘ₗ LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A CoalgebraStruct.comul = ↑(TensorProduct.rid R A).symm ∘ₗ LinearMap.mul' R A

source

theorem FrobeniusAlgebra.rTensor_counit_mul_comp_lTensor_comul_unit {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [FrobeniusAlgebra R A] :

LinearMap.rTensor A (CoalgebraStruct.counit ∘ₗ LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm ∘ₗ LinearMap.lTensor A (CoalgebraStruct.comul ∘ₗ Algebra.linearMap R A) = ↑(TensorProduct.comm R A R)

"snake equations" v1

source

theorem FrobeniusAlgebra.lTensor_counit_mul_comp_rTensor_comul_unit {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [FrobeniusAlgebra R A] :

LinearMap.lTensor A (CoalgebraStruct.counit ∘ₗ LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A (CoalgebraStruct.comul ∘ₗ Algebra.linearMap R A) = ↑(TensorProduct.comm R R A)

"snake equations" v2