Monlib.LinearAlgebra.Coalgebra.FiniteDimensional

source

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

source

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

source

theorem LinearMap.adjoint_id {𝕜 : Type u_3} {A : Type u_4} [RCLike 𝕜] [NormedAddCommGroup A] [InnerProductSpace 𝕜 A] [FiniteDimensional 𝕜 A] :

LinearMap.adjoint LinearMap.id = LinearMap.id

source

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

LinearMap.adjoint (LinearMap.rTensor C f) = LinearMap.rTensor C (LinearMap.adjoint f)

source

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

LinearMap.adjoint (LinearMap.lTensor C f) = LinearMap.lTensor C (LinearMap.adjoint f)

source

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

source

@[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

Coalgebra.ofFiniteDimensionalHilbertAlgebra = Coalgebra.mk ⋯ ⋯ ⋯

source

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

Coalgebra.comul = LinearMap.adjoint (LinearMap.mul' R A)

source

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

Coalgebra.counit = LinearMap.adjoint (Algebra.linearMap R A)

source

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) = ⇑Coalgebra.counit

source

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

Coalgebra.counit = ↑((bra R) 1)

source

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 Coalgebra.comul = Coalgebra.comul ∘ₗ LinearMap.mul' R A

source

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

source

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 Coalgebra.comul = Coalgebra.comul ∘ₗ LinearMap.mul' R A

source

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

source

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

source

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

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

Instances For

source

theorem LinearMap.IsCoalgHom.counit_comp {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} (self : x.IsCoalgHom) :

Coalgebra.counit ∘ₗ x = Coalgebra.counit

source

theorem LinearMap.IsCoalgHom.map_comp_comul {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} (self : x.IsCoalgHom) :

TensorProduct.map x x ∘ₗ Coalgebra.comul = Coalgebra.comul ∘ₗ x

source

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 ↔ Coalgebra.counit ∘ₗ x = Coalgebra.counit ∧ TensorProduct.map x x ∘ₗ Coalgebra.comul = Coalgebra.comul ∘ₗ x

source

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

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

Instances For

source

theorem LinearMap.IsAlgHom.comp_unit {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} (self : x.IsAlgHom) :

x ∘ₗ Algebra.linearMap R A = Algebra.linearMap R B

source

theorem LinearMap.IsAlgHom.mul'_comp_map {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} (self : x.IsAlgHom) :

LinearMap.mul' R B ∘ₗ TensorProduct.map x x = x ∘ₗ LinearMap.mul' R A

source

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 ∧ LinearMap.mul' R B ∘ₗ TensorProduct.map x x = x ∘ₗ LinearMap.mul' R A

source

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

source

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

source

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 ↔ (LinearMap.adjoint x).IsCoalgHom

source

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 ↔ (LinearMap.adjoint x).IsAlgHom