Contraction of vectors

This file is down stream of TensorTree. There are other files in TensorSpecies.Contractions which are up-stream of TensorTree.

def TensorSpecies.contractSelfHom (S : TensorSpecies) (c : S.C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c }) (S.FD.obj { as := c }) ⟶ 𝟙_ (Rep S.k S.G)

The equivariant map from S.FD.obj (Discrete.mk c) ⊗ S.FD.obj (Discrete.mk c) to the underlying field obtained by contracting.

Equations

• S.contractSelfHom c = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (S.FD.obj { as := c }) (S.dualRepIsoDiscrete c).hom) (S.contr.app { as := c })

def TensorSpecies.contractSelfField {S : TensorSpecies} {c : S.C} : TensorProduct S.k ↑(S.FD.obj { as := c }).V ↑(S.FD.obj { as := c }).V →ₗ[S.k] S.k

The contraction of two vectors in a tensor species of the same color, as a linear map to the underlying field.

Equations

• TensorSpecies.contractSelfField = ModuleCat.Hom.hom (S.contractSelfHom c).hom

def TensorSpecies.«term⟪_,_⟫ₜₛ» : Lean.ParserDescr

Notation for coCoContract acting on a tmul.

Equations

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

@[simp]

theorem TensorSpecies.contractSelfField_equivariant {S : TensorSpecies} {c : S.C} {g : S.G} (ψ φ : ↑(S.FD.obj { as := c }).V) : contractSelfField (((S.FD.obj { as := c }).ρ g) ψ ⊗ₜ[S.k] ((S.FD.obj { as := c }).ρ g) φ) = contractSelfField (ψ ⊗ₜ[S.k] φ)

The map contractSelfField is equivariant with respect to the group action.

def TensorSpecies.contractSelfField_non_degenerate : InformalLemma

The contraction of two vectors of the same color is non-degenerate, i.e., ⟪ψ, φ⟫ₜₛ = 0 for all φ implies ψ = 0.

Proof: the basic idea is that being degenerate contradicts the assumption of having a unit in the tensor species.

Equations

• TensorSpecies.contractSelfField_non_degenerate = { deps := [`TensorSpecies.contractSelfField] }

def TensorSpecies.contractSelfField_tensorTree : InformalLemma

The contraction ⟪ψ, φ⟫ₜₛ is related to the tensor tree {ψ | μ ⊗ (S.dualRepIsoDiscrete c).hom φ | μ}ᵀ.

Equations

• TensorSpecies.contractSelfField_tensorTree = { deps := [`TensorSpecies.contractSelfField, `TensorTree] }

IsNormOne

def TensorSpecies.IsNormOne (S : TensorSpecies) {c : S.C} (ψ : ↑(S.FD.obj { as := c }).V) : Prop

A vector satisfies IsNormOne if it has norm equal to one, i.e. if ⟪ψ, ψ⟫ₜₛ = 1.

Equations

• S.IsNormOne ψ = (TensorSpecies.contractSelfField (ψ ⊗ₜ[S.k] ψ) = 1)

@[simp]

theorem TensorSpecies.action_isNormOne_of_isNormOne (S : TensorSpecies) {c : S.C} {ψ : ↑(S.FD.obj { as := c }).V} (g : S.G) : S.IsNormOne (((S.FD.obj { as := c }).ρ g) ψ) ↔ S.IsNormOne ψ

If a vector is norm-one, then any vector in the orbit of that vector is also norm-one.

IsNormZero

def TensorSpecies.IsNormZero (S : TensorSpecies) {c : S.C} (ψ : ↑(S.FD.obj { as := c }).V) : Prop

A vector satisfies IsNormZero if it has norm equal to zero, i.e. if ⟪ψ, ψ⟫ₜₛ = 0.

Equations

• S.IsNormZero ψ = (TensorSpecies.contractSelfField (ψ ⊗ₜ[S.k] ψ) = 0)

@[simp]

theorem TensorSpecies.zero_isNormZero (S : TensorSpecies) {c : S.C} : S.IsNormZero 0

The zero vector has norm equal to zero.

theorem TensorSpecies.smul_isNormZero_of_isNormZero (S : TensorSpecies) {c : S.C} {ψ : ↑(S.FD.obj { as := c }).V} (h : S.IsNormZero ψ) (a : S.k) : S.IsNormZero (a • ψ)

If a vector is norm-zero, then any scalar multiple of that vector is also norm-zero.

@[simp]

theorem TensorSpecies.action_isNormZero_iff_isNormZero (S : TensorSpecies) {c : S.C} {ψ : ↑(S.FD.obj { as := c }).V} (g : S.G) : S.IsNormZero (((S.FD.obj { as := c }).ρ g) ψ) ↔ S.IsNormZero ψ

If a vector is norm-zero, then any vector in the orbit of that vector is also norm-zero.