LeanPool.Monlib4.LinearAlgebra.Coalgebra.FiniteDimensional

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

theorem algebraMapCLM_eq_ket_one {R : Type u_3} {A : Type u_4} [RCLike R] [NormedAddCommGroupOfRing A] [InnerProductSpace R A] [SMulCommClass R A A] [IsScalarTower R A A] : algebraMapCLM R A = (ket R) 1

theorem algebraMapCLM_adjoint_eq_bra_one {R : Type u_3} {A : Type u_4} [RCLike R] [NormedAddCommGroupOfRing A] [InnerProductSpace R A] [SMulCommClass R A A] [IsScalarTower R A A] [CompleteSpace A] : ContinuousLinearMap.adjoint (algebraMapCLM R A) = (bra R) 1

theorem LinearMap.rTensor_adjoint {𝕜 : Type u_3} {A : Type u_4} {B : Type u_5} {C : Type u_6} [RCLike 𝕜] [NormedAddCommGroup A] [NormedAddCommGroup B] [NormedAddCommGroup C] [InnerProductSpace 𝕜 A] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] [FiniteDimensional 𝕜 A] [FiniteDimensional 𝕜 B] [FiniteDimensional 𝕜 C] (f : A →ₗ[𝕜] B) : adjoint (rTensor C f) = rTensor C (adjoint f)

theorem LinearMap.lTensor_adjoint {𝕜 : Type u_3} {A : Type u_4} {B : Type u_5} {C : Type u_6} [RCLike 𝕜] [NormedAddCommGroup A] [NormedAddCommGroup B] [NormedAddCommGroup C] [InnerProductSpace 𝕜 A] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] [FiniteDimensional 𝕜 A] [FiniteDimensional 𝕜 B] [FiniteDimensional 𝕜 C] (f : A →ₗ[𝕜] B) : adjoint (lTensor C f) = lTensor C (adjoint f)

theorem TensorProduct.rid_adjoint {𝕜 : Type u_3} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : LinearMap.adjoint ↑(TensorProduct.rid 𝕜 E) = ↑(TensorProduct.rid 𝕜 E).symm

@[reducible]

noncomputable instance Coalgebra.ofFiniteDimensionalHilbertAlgebra {R : Type u_1} {A : Type u_2} [RCLike R] [NormedAddCommGroupOfRing A] [InnerProductSpace R A] [SMulCommClass R A A] [IsScalarTower R A A] [FiniteDimensional R A] : Coalgebra R A

Equations

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

theorem Coalgebra.comul_eq_mul_adjoint {R : Type u_1} {A : Type u_2} [RCLike R] [NormedAddCommGroupOfRing A] [InnerProductSpace R A] [SMulCommClass R A A] [IsScalarTower R A A] [FiniteDimensional R A] : comul = LinearMap.adjoint (LinearMap.mul' R A)

theorem Coalgebra.counit_eq_unit_adjoint {R : Type u_1} {A : Type u_2} [RCLike R] [NormedAddCommGroupOfRing A] [InnerProductSpace R A] [SMulCommClass R A A] [IsScalarTower R A A] [FiniteDimensional R A] : counit = LinearMap.adjoint (Algebra.linearMap R A)

theorem Coalgebra.inner_eq_counit' {R : Type u_1} {A : Type u_2} [RCLike R] [NormedAddCommGroupOfRing A] [InnerProductSpace R A] [SMulCommClass R A A] [IsScalarTower R A A] [FiniteDimensional R A] : (fun (x : A) => inner R 1 x) = ⇑counit

theorem Coalgebra.counit_eq_bra_one {R : Type u_1} {A : Type u_2} [RCLike R] [NormedAddCommGroupOfRing A] [InnerProductSpace R A] [SMulCommClass R A A] [IsScalarTower R A A] [FiniteDimensional R A] : counit = ↑((bra R) 1)

theorem Coalgebra.rTensor_mul_comp_lTensor_comul {R : Type u_1} {A : Type u_2} [RCLike R] [NormedAddCommGroupOfRing A] [InnerProductSpace R A] [SMulCommClass R A A] [IsScalarTower R A A] [FiniteDimensional R A] (h : ∃ (σ : A → A), ∀ (x y z : A), inner R (x * y) z = inner R y (σ x * z)) : LinearMap.rTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm ∘ₗ LinearMap.lTensor A comul = comul ∘ₗ LinearMap.mul' R A

theorem Coalgebra.rTensor_mul_comp_lTensor_mul_adjoint {R : Type u_1} {A : Type u_2} [RCLike R] [NormedAddCommGroupOfRing A] [InnerProductSpace R A] [SMulCommClass R A A] [IsScalarTower R A A] [FiniteDimensional R A] (h : ∃ (σ : A → A), ∀ (x y z : A), inner R (x * y) z = inner R y (σ x * z)) : LinearMap.rTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm ∘ₗ LinearMap.lTensor A (LinearMap.adjoint (LinearMap.mul' R A)) = LinearMap.adjoint (LinearMap.mul' R A) ∘ₗ LinearMap.mul' R A

theorem Coalgebra.lTensor_mul_comp_rTensor_comul_of {R : Type u_1} {A : Type u_2} [RCLike R] [NormedAddCommGroupOfRing A] [InnerProductSpace R A] [SMulCommClass R A A] [IsScalarTower R A A] [FiniteDimensional R A] (h : ∃ (σ : A → A), ∀ (x y z : A), inner R (x * y) z = inner R y (σ x * z)) : LinearMap.lTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A comul = comul ∘ₗ LinearMap.mul' R A

theorem Coalgebra.lTensor_mul_comp_rTensor_mul_adjoint_of {R : Type u_1} {A : Type u_2} [RCLike R] [NormedAddCommGroupOfRing A] [InnerProductSpace R A] [SMulCommClass R A A] [IsScalarTower R A A] [FiniteDimensional R A] (h : ∃ (σ : A → A), ∀ (x y z : A), inner R (x * y) z = inner R y (σ x * z)) : LinearMap.lTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A (LinearMap.adjoint (LinearMap.mul' R A)) = LinearMap.adjoint (LinearMap.mul' R A) ∘ₗ LinearMap.mul' R A

@[reducible]

noncomputable def FiniteDimensionalCoAlgebraIsFrobeniusAlgebraOf {R : Type u_1} {A : Type u_2} [RCLike R] [NormedAddCommGroupOfRing A] [InnerProductSpace R A] [SMulCommClass R A A] [IsScalarTower R A A] [FiniteDimensional R A] (h : ∃ (σ : A → A), ∀ (x y z : A), inner R (x * y) z = inner R y (σ x * z)) : FrobeniusAlgebra R A

Construct the Frobenius algebra structure from finite-dimensional Hilbert-algebra data.

Equations

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

structure LinearMap.IsCoalgHom {R : Type u_3} {A : Type u_4} {B : Type u_5} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (x : A →ₗ[R] B) : Prop

Predicate for linear maps that preserve the counit and comultiplication.

• counit_comp : CoalgebraStruct.counit ∘ₗ x = CoalgebraStruct.counit
• map_comp_comul : TensorProduct.map x x ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ x

theorem LinearMap.isCoalgHom_iff {R : Type u_3} {A : Type u_4} {B : Type u_5} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (x : A →ₗ[R] B) : x.IsCoalgHom ↔ CoalgebraStruct.counit ∘ₗ x = CoalgebraStruct.counit ∧ TensorProduct.map x x ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ x

structure LinearMap.IsAlgHom {R : Type u_3} {A : Type u_4} {B : Type u_5} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (x : A →ₗ[R] B) : Prop

Predicate for linear maps that preserve the unit and multiplication.

• comp_unit : x ∘ₗ Algebra.linearMap R A = Algebra.linearMap R B
• mul'_comp_map : mul' R B ∘ₗ TensorProduct.map x x = x ∘ₗ mul' R A

theorem LinearMap.isAlgHom_iff {R : Type u_3} {A : Type u_4} {B : Type u_5} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (x : A →ₗ[R] B) : x.IsAlgHom ↔ x ∘ₗ Algebra.linearMap R A = Algebra.linearMap R B ∧ mul' R B ∘ₗ TensorProduct.map x x = x ∘ₗ mul' R A

theorem AlgHom.isAlgHom {R : Type u_3} {A : Type u_4} {B : Type u_5} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (x : A →ₐ[R] B) : x.toLinearMap.IsAlgHom

theorem AlgEquiv.isAlgHom {R : Type u_3} {A : Type u_4} {B : Type u_5} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (x : A ≃ₐ[R] B) : x.toLinearMap.IsAlgHom

theorem LinearMap.isAlgHom_iff_adjoint_isCoalgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [RCLike R] [NormedAddCommGroupOfRing A] [NormedAddCommGroupOfRing B] [InnerProductSpace R A] [InnerProductSpace R B] [SMulCommClass R A A] [SMulCommClass R B B] [IsScalarTower R A A] [IsScalarTower R B B] [FiniteDimensional R A] [FiniteDimensional R B] (x : A →ₗ[R] B) : x.IsAlgHom ↔ (adjoint x).IsCoalgHom

theorem LinearMap.isCoalgHom_iff_adjoint_isAlgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [RCLike R] [NormedAddCommGroupOfRing A] [NormedAddCommGroupOfRing B] [InnerProductSpace R A] [InnerProductSpace R B] [SMulCommClass R A A] [SMulCommClass R B B] [IsScalarTower R A A] [IsScalarTower R B B] [FiniteDimensional R A] [FiniteDimensional R B] (x : A →ₗ[R] B) : x.IsCoalgHom ↔ (adjoint x).IsAlgHom