Documentation

Monlib.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.adjoint_id {𝕜 : Type u_3} {A : Type u_4} [RCLike 𝕜] [NormedAddCommGroup A] [InnerProductSpace 𝕜 A] [FiniteDimensional 𝕜 A] :

adjoint id = id

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] :

Equations

Coalgebra.ofFiniteDimensionalHilbertAlgebra = Coalgebra.mk ⋯ ⋯ ⋯

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 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] [Star A] [InnerProductSpace R A] [SMulCommClass R A A] [IsScalarTower R A A] [FiniteDimensional R A] (h : ∃ (σ : A → A), ∀ (x y z : A), inner (x * y) z = inner y (σ (star 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] [Star A] [InnerProductSpace R A] [SMulCommClass R A A] [IsScalarTower R A A] [FiniteDimensional R A] (h : ∃ (σ : A → A), ∀ (x y z : A), inner (x * y) z = inner y (σ (star 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] [Star A] [InnerProductSpace R A] [SMulCommClass R A A] [IsScalarTower R A A] [FiniteDimensional R A] (h : ∃ (σ : A → A), ∀ (x y z : A), inner (x * y) z = inner y (σ (star 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] [Star A] [InnerProductSpace R A] [SMulCommClass R A A] [IsScalarTower R A A] [FiniteDimensional R A] (h : ∃ (σ : A → A), ∀ (x y z : A), inner (x * y) z = inner y (σ (star 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

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

FrobeniusAlgebra R A

Equations

FiniteDimensionalCoAlgebra_isFrobeniusAlgebra_of h = FrobeniusAlgebra.mk ⋯

Instances For

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) :

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

Instances For

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) :

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

Instances For

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