1. Physlib
  2. Particles
  3. SuperSymmetry
  4. N1
  5. Basic
Imports
/- Copyright (c) 2026 Andrea Pari. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Andrea Pari -/ module public import Mathlib.Data.Complex.Basic public import Physlib.Relativity.Tensors.Conjugation.Basic

SUSY N=1 chiral sector: index, configuration, and conjugation data

i. Overview

This file fixes the data that indexes the scalars of the N=1 chiral sector, makes their contractions type-safe, and equips them with conjugation.

A single finite type ι indexes the chiral scalars (written ChiralIndexingType in signatures) — the only index type. Variance (upper versus lower) and holomorphy (a scalar versus its complex conjugate) are not separate index types but the two axes of a four-element type ChiralColor, the product of chiral/anti with up/down. Each axis is realized as a genuine carrier distinction, not a label: variance as a module versus its dual (ι → ℂ versus Module.Dual ℂ (ι → ℂ)), holomorphy as a module versus its complex conjugate (ConjModule, where i acts as −i).

The dual-colour involution τ flips variance and preserves holomorphy. Two indices may contract exactly when their colours are τ-related, so a holomorphic index pairs only with a holomorphic index of the opposite variance, and a conjugate ("barred") index only with a conjugate index of the opposite variance. This is the discipline that makes the F-term contraction g^{IJ̄} D_I W D̄_J̄ W̄ type-check.

The physical field content is the configuration ChiralScalarConfiguration ι = ι → ℂ, carrying 2 · Fintype.card ι real degrees of freedom. The anti-chiral scalars are the complex conjugates of this data, never an independent configuration.

The index data is packaged as a ConjTensorSpecies over ChiralColor, each colour carrying its distinct carrier from above. Complex conjugation is the conjugate-linear identity conjEquiv : M ≃ₛₗ[starRingEnd ℂ] ConjModule M on each carrier (anti basis Basis.conj); the species' holomorphy flip (conjEquiv, hence conjT) is built from it. Every colour carries the trivial representation over the trivial group Unit, so the chiral scalars hold no charge. Contracting a colour against its τ-dual is the dot product of the two coordinate vectors, the Kronecker δ_{IJ} on basis labels: contr is that pairing V c ⊗ V (τ c) → ℂ, unit its cap in V (τ c) ⊗ V c, and metric the cap ∑_I b_I ⊗ b_I in V c ⊗ V c. This instance equips the chiral sector with the framework's generic tensor API (.Tensor, .contrT, …).

Conjugation is intrinsic species data: a ConjTensorSpecies is a TensorSpecies extended with the conjugate-colour involution ChiralColor.bar and its coherence. The framework then supplies the map conjT (conjugate the components and flip each index's holomorphy by bar) and its laws. bar is the holomorphy dual, distinct from and commuting with the variance dual τ; it is not used in contraction.

Conjugation enters wherever reality does. It is what lets one state that the Kähler metric is Hermitian (conjT g equals g with its two indices swapped), that the anti-chiral sector is the complex conjugate of the chiral one (D̄_J̄ W̄ = conjT (D_I W)), and hence that the F-term g^{IJ̄} D_I W D̄_J̄ W̄ is real. The species can express none of these alone.

ii. Key results

    SUSY.N1.ChiralScalarConfiguration : the scalar configuration space ι → ℂ, where ι is the finite type indexing the chiral scalars. This is the only field data in the sector.

    SUSY.N1.ChiralColor : the four colours chiral/anti × up/down, with the dual-colour involution ChiralColor.tau.

    SUSY.N1.chiralTensor : the ConjTensorSpecies assembled from the above, whose τ-discipline makes the F-term contraction type-safe and whose bar carries the chiral-antichiral conjugation in which reality and Hermiticity conditions are phrased.

iii. Table of contents

    A. The chiral scalar configuration

    B. The chiral colours and the dual involution

    C. Carrier, representation, and basis

    D. The δ structure on based finite modules

    E. The chiral-index tensor species

    F. Conjugation

iv. References

@[expose] public section

A. The chiral scalar configuration

The chiral scalar configuration: a complex value for each chiral label. This is the sector's only field data. Declared as an abbrev so that unification sees through it to ChiralIndexingType → ℂ and applies Mathlib's function-space calculus lemmas directly.

abbrev ChiralScalarConfiguration (ChiralIndexingType : Type*) := ChiralIndexingType → ℂ

B. The chiral colours and the dual involution

The four colours carried by a chiral-sector index: holomorphy (chiral versus anti, a scalar versus its complex conjugate) crossed with variance (up versus down, contravariant versus covariant). Carrying both axes here lets the single index type ι label the scalars.

inductive ChiralColor | chiralUp | chiralDown | antiUp | antiDown deriving DecidableEq

The dual colour: flips variance and preserves holomorphy. Two indices may contract exactly when their colours are τ-related, so V^I pairs only with V_I (same holomorphy, opposite variance) and never with a conjugate index.

def tau : ChiralColor → ChiralColor | chiralUp => chiralDown | chiralDown => chiralUp | antiUp => antiDown | antiDown => antiUp

The conjugate colour: flips holomorphy (chiral↔anti) and preserves variance. Complex conjugation sends an index to its conjugate carrier, so bar swaps chiral* with anti*. Distinct from the variance dual tau; the two commute (bar_tau).

def bar : ChiralColor → ChiralColor | chiralUp => antiUp | antiUp => chiralUp | chiralDown => antiDown | antiDown => chiralDown
@[simp] lemma bar_bar (c : ChiralColor) : bar (bar c) = c := c:ChiralColor⊢ c.bar.bar = c ⊢ chiralUp.bar.bar = chiralUp⊢ chiralDown.bar.bar = chiralDown⊢ antiUp.bar.bar = antiUp⊢ antiDown.bar.bar = antiDown ⊢ chiralUp.bar.bar = chiralUp⊢ chiralDown.bar.bar = chiralDown⊢ antiUp.bar.bar = antiUp⊢ antiDown.bar.bar = antiDown All goals completed! 🐙@[simp] lemma bar_tau (c : ChiralColor) : bar (tau c) = tau (bar c) := c:ChiralColor⊢ c.tau.bar = c.bar.tau ⊢ chiralUp.tau.bar = chiralUp.bar.tau⊢ chiralDown.tau.bar = chiralDown.bar.tau⊢ antiUp.tau.bar = antiUp.bar.tau⊢ antiDown.tau.bar = antiDown.bar.tau ⊢ chiralUp.tau.bar = chiralUp.bar.tau⊢ chiralDown.tau.bar = chiralDown.bar.tau⊢ antiUp.tau.bar = antiUp.bar.tau⊢ antiDown.tau.bar = antiDown.bar.tau All goals completed! 🐙

C. Carrier, representation, and basis

A TensorSpecies takes, for each colour c, a carrier module, a group representation on it, and a basis. The carrier depends on both axes: variance gives the vector/dual distinction (ι → ℂ versus Module.Dual ℂ (ι → ℂ)) and holomorphy the conjugate-module distinction (ConjModule …, where i acts as −i), so all four colours have distinct carriers. The representation is trivial over the trivial group Unit (no charge) for every colour; each basis is indexed by ι — piBasis, its dual piBasis.dualBasis, and the Basis.conj of each. Variance (τ) sends a carrier to its dual; conjugation (bar) sends it to its conjugate module.

The carrier module of each colour, distinct for all four: the holomorphic vectors ι → ℂ and their dual Module.Dual ℂ (ι → ℂ) on the chiral side, and the conjugate module ConjModule … of each (where i acts as −i) on the anti side. Variance is the vector/dual axis, holomorphy the conjugate-module axis; both are genuine carrier data, not labels tracked separately.

abbrev chiralModule : ChiralColor → Type | .chiralUp => ι → ℂ | .chiralDown => Module.Dual ℂ (ι → ℂ) | .antiUp => ConjModule (ι → ℂ) | .antiDown => ConjModule (Module.Dual ℂ (ι → ℂ))
instance instAddCommGroupChiralModule : ∀ c, AddCommGroup (chiralModule (ι := ι) c) | .chiralUp | .chiralDown | .antiUp | .antiDown => inferInstance

The representation on each colour, taken trivial over the trivial group Unit: the chiral scalars carry no charge in this sector.

def chiralRep : (c : ChiralColor) → Representation ℂ Unit (chiralModule (ι := ι) c) := fun _ => Representation.trivial ℂ Unit _

The standard basis of the vector carrier ι → ℂ (the indicator functions); the basis of chiralUp and the reference basis for the δ pairing.

def piBasis : Basis ι ℂ (ι → ℂ) := Pi.basisFun ℂ ι

D. The δ structure on based finite modules

The contraction, unit, and metric are one δ structure in basis coordinates. Here metric is the TensorSpecies field of that name — the δ index-raising tensor δ^{IJ} — and is not the physical Kähler metric g_{IJ̄}, which is built downstream on top of this sector. A contraction pairs a colour with its variance dual τ c, whose carriers are distinct (a module and its dual, or their conjugates) but share the index ι, so the pairing is the dot product across two based modules (M, b) and (N, b'), (x, y) ↦ ∑_I (b x)_I (b' y)_I, with cap ∑_I b_I ⊗ b'_I ∈ M ⊗ N. The single-colour cap deltaCap (b = b') is what metric c uses, since its two slots are the same colour; the two-module pairing deltaContr₂/deltaCap₂ is what contr and unit use. The δ data stays within one holomorphy and needs no conjugation; conjugation is carried instead by the tensor conjT (§F).

The δ cap ∑_I b_I ⊗ b_I: the rank-2 tensor in M ⊗ M with two upper indices, whose components in the basis b are δⁱʲ. It is an element of M ⊗ M (the inverse-metric "cap"), not a linear map, and serves as the metric field of the species (whose two slots share a colour).

def deltaCap (b : Basis ι ℂ M) : M ⊗[ℂ] M := ∑ I, b I ⊗ₜ[ℂ] b I

The δ pairing between two based modules sharing the index ι: the dot product of coordinate vectors (x, y) ↦ ∑_I (b x)_I (b' y)_I. Built from Mathlib's Basis.toDual b (the canonical δ map M → Module.Dual M, sending b to its dual basis) precomposed on the second slot with the basis transport b' ≃ b.

def deltaBil₂ (b : Basis ι ℂ M) (b' : Basis ι ℂ N) : M →ₗ[ℂ] N →ₗ[ℂ] ℂ := b.toDual.compl₂ (b'.equiv b (Equiv.refl ι)).toLinearMap

deltaBil₂ b b' x y = ∑_I (b x)_I (b' y)_I.

ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nb:Basis ι ℂ Mb':Basis ι ℂ Nx:My:N⊢ (b.toDual x) ((b'.equiv b (Equiv.refl ι)) y) = ∑ I, b.equivFun x I * b'.equivFun y I conv_lhs => ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nb:Basis ι ℂ Mb':Basis ι ℂ Nx:My:N| (b.toDual x) ((b'.equiv b (Equiv.refl ι)) (∑ i, b'.equivFun y i • b' i)) simp_rw ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nb:Basis ι ℂ Mb':Basis ι ℂ Nx:My:N⊢ (b.toDual x) ((b'.equiv b (Equiv.refl ι)) (∑ i, b'.equivFun y i • b' i)) = ∑ I, b.equivFun x I * b'.equivFun y Iι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nb:Basis ι ℂ Mb':Basis ι ℂ Nx:My:N⊢ ∑ x_1, (b.toDual x) ((b'.equiv b (Equiv.refl ι)) (b'.equivFun y x_1 • b' x_1)) = ∑ I, b.equivFun x I * b'.equivFun y I ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nb:Basis ι ℂ Mb':Basis ι ℂ Nx:My:N⊢ ∑ x_1, b'.equivFun y x_1 • (b.toDual x) ((b'.equiv b (Equiv.refl ι)) (b' x_1)) = ∑ I, b.equivFun x I * b'.equivFun y I ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nb:Basis ι ℂ Mb':Basis ι ℂ Nx:My:N⊢ ∑ x_1, b'.equivFun y x_1 • (b.toDual x) (b ((Equiv.refl ι) x_1)) = ∑ I, b.equivFun x I * b'.equivFun y I ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nb:Basis ι ℂ Mb':Basis ι ℂ Nx:My:N⊢ ∑ x_1, b'.equivFun y x_1 • (b.toDual x) (b x_1) = ∑ I, b.equivFun x I * b'.equivFun y I ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nb:Basis ι ℂ Mb':Basis ι ℂ Nx:My:N⊢ ∑ x_1, b'.equivFun y x_1 • b.equivFun x x_1 = ∑ I, b.equivFun x I * b'.equivFun y I ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nb:Basis ι ℂ Mb':Basis ι ℂ Nx:My:N⊢ ∑ x_1, b'.equivFun y x_1 * b.equivFun x x_1 = ∑ I, b.equivFun x I * b'.equivFun y I] All goals completed! 🐙

The two-module δ contraction M ⊗ N → ℂ.

def deltaContr₂ (b : Basis ι ℂ M) (b' : Basis ι ℂ N) : M ⊗[ℂ] N →ₗ[ℂ] ℂ := TensorProduct.lift (deltaBil₂ b b')

deltaContr₂ b b' (x ⊗ₜ y) = ∑_I (b x)_I (b' y)_I.

All goals completed! 🐙

deltaContr₂ b b' (x ⊗ₜ b' J) = x_J: pairing with the second basis reads off a coordinate.

lemma deltaContr₂_tmul_basis (b : Basis ι ℂ M) (b' : Basis ι ℂ N) (x : M) (J : ι) : deltaContr₂ b b' (x ⊗ₜ[ℂ] b' J) = b.equivFun x J := ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nb:Basis ι ℂ Mb':Basis ι ℂ Nx:MJ:ι⊢ (deltaContr₂ b b') (x ⊗ₜ[ℂ] b' J) = b.equivFun x J All goals completed! 🐙

deltaContr₂ b b' (b I ⊗ₜ b' J) = δ_{IJ}: the two bases are δ-dual.

All goals completed! 🐙

deltaContr₂ b b' (x ⊗ₜ y) = deltaContr₂ b' b (y ⊗ₜ x): swapping slots swaps the two bases.

ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nb:Basis ι ℂ Mb':Basis ι ℂ Nx:My:N⊢ ∑ I, b.equivFun x I * b'.equivFun y I = ∑ I, b'.equivFun y I * b.equivFun x I All goals completed! 🐙

The two-module δ cap ∑_I b_I ⊗ b'_I ∈ M ⊗ N.

def deltaCap₂ (b : Basis ι ℂ M) (b' : Basis ι ℂ N) : M ⊗[ℂ] N := ∑ I, b I ⊗ₜ[ℂ] b' I

comm (deltaCap₂ b b') = deltaCap₂ b' b: swapping the two factors swaps the two bases.

omit [DecidableEq ι] inAll goals completed! 🐙

The unit_symm law (two-module, toSpanSingleton form): deltaCap₂ b' b is the swap of deltaCap₂ b b'.

omit [DecidableEq ι] inι:Typeinst✝⁴:Fintype ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nb:Basis ι ℂ Mb':Basis ι ℂ N⊢ deltaCap₂ b' b = (LinearMap.lTensor N ↑(LinearEquiv.refl ℂ M)) (deltaCap₂ b' b) All goals completed! 🐙

The snake identity (two-module, contr_unit law): contracting x ∈ M into the M-leg of deltaCap₂ b' b ∈ N ⊗ M returns x.

All goals completed! 🐙

The contr_metric law (two-module): contracting the inner M/N legs of deltaCap b ⊗ deltaCap b' yields deltaCap₂ b' b.

ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nb:Basis ι ℂ Mb':Basis ι ℂ N⊢ (TensorProduct.comm ℂ M N) ((LinearEquiv.lTensor M (TensorProduct.lid ℂ N)) ((LinearMap.lTensor M (LinearMap.rTensor N (deltaContr₂ b b'))) ((LinearMap.lTensor M ↑(TensorProduct.assoc ℂ M N N).symm) ((TensorProduct.assoc ℂ M M (N ⊗[ℂ] N)) (deltaCap b ⊗ₜ[ℂ] deltaCap b'))))) = deltaCap₂ b' b conv_lhs => ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nb:Basis ι ℂ Mb':Basis ι ℂ N| (TensorProduct.comm ℂ M N) ((LinearEquiv.lTensor M (TensorProduct.lid ℂ N)) ((LinearMap.lTensor M (LinearMap.rTensor N (deltaContr₂ b b'))) ((LinearMap.lTensor M ↑(TensorProduct.assoc ℂ M N N).symm) ((TensorProduct.assoc ℂ M M (N ⊗[ℂ] N)) (∑ a, b a ⊗ₜ[ℂ] b a ⊗ₜ[ℂ] ∑ I, b' I ⊗ₜ[ℂ] b' I))))) conv_rhs => ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nb:Basis ι ℂ Mb':Basis ι ℂ N| ∑ I, b' I ⊗ₜ[ℂ] b I ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nb:Basis ι ℂ Mb':Basis ι ℂ N⊢ ∑ x, ∑ x_1, (TensorProduct.comm ℂ M N) ((LinearEquiv.lTensor M (TensorProduct.lid ℂ N)) ((LinearMap.lTensor M (LinearMap.rTensor N (deltaContr₂ b b'))) ((LinearMap.lTensor M ↑(TensorProduct.assoc ℂ M N N).symm) ((TensorProduct.assoc ℂ M M (N ⊗[ℂ] N)) (b x ⊗ₜ[ℂ] b x ⊗ₜ[ℂ] (b' x_1 ⊗ₜ[ℂ] b' x_1)))))) = ∑ I, b' I ⊗ₜ[ℂ] b I ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nb:Basis ι ℂ Mb':Basis ι ℂ N⊢ ∑ x, ∑ x_1, (if x = x_1 then b' x_1 else 0) ⊗ₜ[ℂ] b x = ∑ I, b' I ⊗ₜ[ℂ] b I All goals completed! 🐙

E. The chiral-index tensor species

The chiral-index tensor species, bundled with its conjugation. Its four colours chiral/anti × up/down carry the four distinct carriers of §C. contr c is the two-module δ pairing of a colour against its variance dual τ c (V c ⊗ V (τ c) → ℂ); unit c is the δ cap across those two carriers; metric c is the single-colour δ cap ∑_I b_I ⊗ b_I. Each TensorSpecies coherence law reduces, by case analysis on the colour, to the corresponding abstract two-module δ lemma of §D. The conjugation flips holomorphy (ChiralColor.bar) while preserving variance; every basis is indexed by ι, so barIdx_eq is rfl, and conj_contrComm is star δ = δ. Instantiating ConjTensorSpecies this way gives the chiral sector both the framework's generic tensor API and its conjugation API (conjT and its laws) on one object.

ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nd:ChiralColorx₁:ιx₂:ιkey:∀ {M₁ M₁' M₂ M₂' : Type} [inst : AddCommGroup M₁] [inst_1 : Module ℂ M₁] [inst_2 : AddCommGroup M₁'] [inst_3 : Module ℂ M₁'] [inst_4 : AddCommGroup M₂] [inst_5 : Module ℂ M₂] [inst_6 : AddCommGroup M₂'] [inst_7 : Module ℂ M₂'] (B₁ : Basis ι ℂ M₁) (B₁' : Basis ι ℂ M₁') (B₂ : Basis ι ℂ M₂) (B₂' : Basis ι ℂ M₂'), star ((deltaContr₂ B₁ B₁') (B₁ x₁ ⊗ₜ[ℂ] B₁' x₂)) = (deltaContr₂ B₂ B₂') (B₂ x₁ ⊗ₜ[ℂ] B₂' x₂)⊢ star ((let __src := deltaContr₂ (chiralBasis d) (chiralBasis d.tau); { toLinearMap := __src, isIntertwining' := ⋯ }) ((chiralBasis d) x₁ ⊗ₜ[ℂ] (chiralBasis d.tau) x₂)) = (let __src := deltaContr₂ (chiralBasis d.bar) (chiralBasis d.bar.tau); { toLinearMap := __src, isIntertwining' := ⋯ }) ((chiralBasis d.bar) ((Equiv.cast ⋯).symm x₁) ⊗ₜ[ℂ] (chiralBasis d.bar.tau) ((TensorSpecies.basisIdxCongr ⋯) ((Equiv.cast ⋯).symm x₂))) ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nx₁:ιx₂:ιkey:∀ {M₁ M₁' M₂ M₂' : Type} [inst : AddCommGroup M₁] [inst_1 : Module ℂ M₁] [inst_2 : AddCommGroup M₁'] [inst_3 : Module ℂ M₁'] [inst_4 : AddCommGroup M₂] [inst_5 : Module ℂ M₂] [inst_6 : AddCommGroup M₂'] [inst_7 : Module ℂ M₂'] (B₁ : Basis ι ℂ M₁) (B₁' : Basis ι ℂ M₁') (B₂ : Basis ι ℂ M₂) (B₂' : Basis ι ℂ M₂'), star ((deltaContr₂ B₁ B₁') (B₁ x₁ ⊗ₜ[ℂ] B₁' x₂)) = (deltaContr₂ B₂ B₂') (B₂ x₁ ⊗ₜ[ℂ] B₂' x₂)⊢ star ((let __src := deltaContr₂ (chiralBasis ChiralColor.chiralUp) (chiralBasis ChiralColor.chiralUp.tau); { toLinearMap := __src, isIntertwining' := ⋯ }) ((chiralBasis ChiralColor.chiralUp) x₁ ⊗ₜ[ℂ] (chiralBasis ChiralColor.chiralUp.tau) x₂)) = (let __src := deltaContr₂ (chiralBasis ChiralColor.chiralUp.bar) (chiralBasis ChiralColor.chiralUp.bar.tau); { toLinearMap := __src, isIntertwining' := ⋯ }) ((chiralBasis ChiralColor.chiralUp.bar) ((Equiv.cast ⋯).symm x₁) ⊗ₜ[ℂ] (chiralBasis ChiralColor.chiralUp.bar.tau) ((TensorSpecies.basisIdxCongr ⋯) ((Equiv.cast ⋯).symm x₂)))ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nx₁:ιx₂:ιkey:∀ {M₁ M₁' M₂ M₂' : Type} [inst : AddCommGroup M₁] [inst_1 : Module ℂ M₁] [inst_2 : AddCommGroup M₁'] [inst_3 : Module ℂ M₁'] [inst_4 : AddCommGroup M₂] [inst_5 : Module ℂ M₂] [inst_6 : AddCommGroup M₂'] [inst_7 : Module ℂ M₂'] (B₁ : Basis ι ℂ M₁) (B₁' : Basis ι ℂ M₁') (B₂ : Basis ι ℂ M₂) (B₂' : Basis ι ℂ M₂'), star ((deltaContr₂ B₁ B₁') (B₁ x₁ ⊗ₜ[ℂ] B₁' x₂)) = (deltaContr₂ B₂ B₂') (B₂ x₁ ⊗ₜ[ℂ] B₂' x₂)⊢ star ((let __src := deltaContr₂ (chiralBasis ChiralColor.chiralDown) (chiralBasis ChiralColor.chiralDown.tau); { toLinearMap := __src, isIntertwining' := ⋯ }) ((chiralBasis ChiralColor.chiralDown) x₁ ⊗ₜ[ℂ] (chiralBasis ChiralColor.chiralDown.tau) x₂)) = (let __src := deltaContr₂ (chiralBasis ChiralColor.chiralDown.bar) (chiralBasis ChiralColor.chiralDown.bar.tau); { toLinearMap := __src, isIntertwining' := ⋯ }) ((chiralBasis ChiralColor.chiralDown.bar) ((Equiv.cast ⋯).symm x₁) ⊗ₜ[ℂ] (chiralBasis ChiralColor.chiralDown.bar.tau) ((TensorSpecies.basisIdxCongr ⋯) ((Equiv.cast ⋯).symm x₂)))ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nx₁:ιx₂:ιkey:∀ {M₁ M₁' M₂ M₂' : Type} [inst : AddCommGroup M₁] [inst_1 : Module ℂ M₁] [inst_2 : AddCommGroup M₁'] [inst_3 : Module ℂ M₁'] [inst_4 : AddCommGroup M₂] [inst_5 : Module ℂ M₂] [inst_6 : AddCommGroup M₂'] [inst_7 : Module ℂ M₂'] (B₁ : Basis ι ℂ M₁) (B₁' : Basis ι ℂ M₁') (B₂ : Basis ι ℂ M₂) (B₂' : Basis ι ℂ M₂'), star ((deltaContr₂ B₁ B₁') (B₁ x₁ ⊗ₜ[ℂ] B₁' x₂)) = (deltaContr₂ B₂ B₂') (B₂ x₁ ⊗ₜ[ℂ] B₂' x₂)⊢ star ((let __src := deltaContr₂ (chiralBasis ChiralColor.antiUp) (chiralBasis ChiralColor.antiUp.tau); { toLinearMap := __src, isIntertwining' := ⋯ }) ((chiralBasis ChiralColor.antiUp) x₁ ⊗ₜ[ℂ] (chiralBasis ChiralColor.antiUp.tau) x₂)) = (let __src := deltaContr₂ (chiralBasis ChiralColor.antiUp.bar) (chiralBasis ChiralColor.antiUp.bar.tau); { toLinearMap := __src, isIntertwining' := ⋯ }) ((chiralBasis ChiralColor.antiUp.bar) ((Equiv.cast ⋯).symm x₁) ⊗ₜ[ℂ] (chiralBasis ChiralColor.antiUp.bar.tau) ((TensorSpecies.basisIdxCongr ⋯) ((Equiv.cast ⋯).symm x₂)))ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nx₁:ιx₂:ιkey:∀ {M₁ M₁' M₂ M₂' : Type} [inst : AddCommGroup M₁] [inst_1 : Module ℂ M₁] [inst_2 : AddCommGroup M₁'] [inst_3 : Module ℂ M₁'] [inst_4 : AddCommGroup M₂] [inst_5 : Module ℂ M₂] [inst_6 : AddCommGroup M₂'] [inst_7 : Module ℂ M₂'] (B₁ : Basis ι ℂ M₁) (B₁' : Basis ι ℂ M₁') (B₂ : Basis ι ℂ M₂) (B₂' : Basis ι ℂ M₂'), star ((deltaContr₂ B₁ B₁') (B₁ x₁ ⊗ₜ[ℂ] B₁' x₂)) = (deltaContr₂ B₂ B₂') (B₂ x₁ ⊗ₜ[ℂ] B₂' x₂)⊢ star ((let __src := deltaContr₂ (chiralBasis ChiralColor.antiDown) (chiralBasis ChiralColor.antiDown.tau); { toLinearMap := __src, isIntertwining' := ⋯ }) ((chiralBasis ChiralColor.antiDown) x₁ ⊗ₜ[ℂ] (chiralBasis ChiralColor.antiDown.tau) x₂)) = (let __src := deltaContr₂ (chiralBasis ChiralColor.antiDown.bar) (chiralBasis ChiralColor.antiDown.bar.tau); { toLinearMap := __src, isIntertwining' := ⋯ }) ((chiralBasis ChiralColor.antiDown.bar) ((Equiv.cast ⋯).symm x₁) ⊗ₜ[ℂ] (chiralBasis ChiralColor.antiDown.bar.tau) ((TensorSpecies.basisIdxCongr ⋯) ((Equiv.cast ⋯).symm x₂))) ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nx₁:ιx₂:ιkey:∀ {M₁ M₁' M₂ M₂' : Type} [inst : AddCommGroup M₁] [inst_1 : Module ℂ M₁] [inst_2 : AddCommGroup M₁'] [inst_3 : Module ℂ M₁'] [inst_4 : AddCommGroup M₂] [inst_5 : Module ℂ M₂] [inst_6 : AddCommGroup M₂'] [inst_7 : Module ℂ M₂'] (B₁ : Basis ι ℂ M₁) (B₁' : Basis ι ℂ M₁') (B₂ : Basis ι ℂ M₂) (B₂' : Basis ι ℂ M₂'), star ((deltaContr₂ B₁ B₁') (B₁ x₁ ⊗ₜ[ℂ] B₁' x₂)) = (deltaContr₂ B₂ B₂') (B₂ x₁ ⊗ₜ[ℂ] B₂' x₂)⊢ star ((let __src := deltaContr₂ (chiralBasis ChiralColor.chiralUp) (chiralBasis ChiralColor.chiralUp.tau); { toLinearMap := __src, isIntertwining' := ⋯ }) ((chiralBasis ChiralColor.chiralUp) x₁ ⊗ₜ[ℂ] (chiralBasis ChiralColor.chiralUp.tau) x₂)) = (let __src := deltaContr₂ (chiralBasis ChiralColor.chiralUp.bar) (chiralBasis ChiralColor.chiralUp.bar.tau); { toLinearMap := __src, isIntertwining' := ⋯ }) ((chiralBasis ChiralColor.chiralUp.bar) ((Equiv.cast ⋯).symm x₁) ⊗ₜ[ℂ] (chiralBasis ChiralColor.chiralUp.bar.tau) ((TensorSpecies.basisIdxCongr ⋯) ((Equiv.cast ⋯).symm x₂)))ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nx₁:ιx₂:ιkey:∀ {M₁ M₁' M₂ M₂' : Type} [inst : AddCommGroup M₁] [inst_1 : Module ℂ M₁] [inst_2 : AddCommGroup M₁'] [inst_3 : Module ℂ M₁'] [inst_4 : AddCommGroup M₂] [inst_5 : Module ℂ M₂] [inst_6 : AddCommGroup M₂'] [inst_7 : Module ℂ M₂'] (B₁ : Basis ι ℂ M₁) (B₁' : Basis ι ℂ M₁') (B₂ : Basis ι ℂ M₂) (B₂' : Basis ι ℂ M₂'), star ((deltaContr₂ B₁ B₁') (B₁ x₁ ⊗ₜ[ℂ] B₁' x₂)) = (deltaContr₂ B₂ B₂') (B₂ x₁ ⊗ₜ[ℂ] B₂' x₂)⊢ star ((let __src := deltaContr₂ (chiralBasis ChiralColor.chiralDown) (chiralBasis ChiralColor.chiralDown.tau); { toLinearMap := __src, isIntertwining' := ⋯ }) ((chiralBasis ChiralColor.chiralDown) x₁ ⊗ₜ[ℂ] (chiralBasis ChiralColor.chiralDown.tau) x₂)) = (let __src := deltaContr₂ (chiralBasis ChiralColor.chiralDown.bar) (chiralBasis ChiralColor.chiralDown.bar.tau); { toLinearMap := __src, isIntertwining' := ⋯ }) ((chiralBasis ChiralColor.chiralDown.bar) ((Equiv.cast ⋯).symm x₁) ⊗ₜ[ℂ] (chiralBasis ChiralColor.chiralDown.bar.tau) ((TensorSpecies.basisIdxCongr ⋯) ((Equiv.cast ⋯).symm x₂)))ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nx₁:ιx₂:ιkey:∀ {M₁ M₁' M₂ M₂' : Type} [inst : AddCommGroup M₁] [inst_1 : Module ℂ M₁] [inst_2 : AddCommGroup M₁'] [inst_3 : Module ℂ M₁'] [inst_4 : AddCommGroup M₂] [inst_5 : Module ℂ M₂] [inst_6 : AddCommGroup M₂'] [inst_7 : Module ℂ M₂'] (B₁ : Basis ι ℂ M₁) (B₁' : Basis ι ℂ M₁') (B₂ : Basis ι ℂ M₂) (B₂' : Basis ι ℂ M₂'), star ((deltaContr₂ B₁ B₁') (B₁ x₁ ⊗ₜ[ℂ] B₁' x₂)) = (deltaContr₂ B₂ B₂') (B₂ x₁ ⊗ₜ[ℂ] B₂' x₂)⊢ star ((let __src := deltaContr₂ (chiralBasis ChiralColor.antiUp) (chiralBasis ChiralColor.antiUp.tau); { toLinearMap := __src, isIntertwining' := ⋯ }) ((chiralBasis ChiralColor.antiUp) x₁ ⊗ₜ[ℂ] (chiralBasis ChiralColor.antiUp.tau) x₂)) = (let __src := deltaContr₂ (chiralBasis ChiralColor.antiUp.bar) (chiralBasis ChiralColor.antiUp.bar.tau); { toLinearMap := __src, isIntertwining' := ⋯ }) ((chiralBasis ChiralColor.antiUp.bar) ((Equiv.cast ⋯).symm x₁) ⊗ₜ[ℂ] (chiralBasis ChiralColor.antiUp.bar.tau) ((TensorSpecies.basisIdxCongr ⋯) ((Equiv.cast ⋯).symm x₂)))ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nx₁:ιx₂:ιkey:∀ {M₁ M₁' M₂ M₂' : Type} [inst : AddCommGroup M₁] [inst_1 : Module ℂ M₁] [inst_2 : AddCommGroup M₁'] [inst_3 : Module ℂ M₁'] [inst_4 : AddCommGroup M₂] [inst_5 : Module ℂ M₂] [inst_6 : AddCommGroup M₂'] [inst_7 : Module ℂ M₂'] (B₁ : Basis ι ℂ M₁) (B₁' : Basis ι ℂ M₁') (B₂ : Basis ι ℂ M₂) (B₂' : Basis ι ℂ M₂'), star ((deltaContr₂ B₁ B₁') (B₁ x₁ ⊗ₜ[ℂ] B₁' x₂)) = (deltaContr₂ B₂ B₂') (B₂ x₁ ⊗ₜ[ℂ] B₂' x₂)⊢ star ((let __src := deltaContr₂ (chiralBasis ChiralColor.antiDown) (chiralBasis ChiralColor.antiDown.tau); { toLinearMap := __src, isIntertwining' := ⋯ }) ((chiralBasis ChiralColor.antiDown) x₁ ⊗ₜ[ℂ] (chiralBasis ChiralColor.antiDown.tau) x₂)) = (let __src := deltaContr₂ (chiralBasis ChiralColor.antiDown.bar) (chiralBasis ChiralColor.antiDown.bar.tau); { toLinearMap := __src, isIntertwining' := ⋯ }) ((chiralBasis ChiralColor.antiDown.bar) ((Equiv.cast ⋯).symm x₁) ⊗ₜ[ℂ] (chiralBasis ChiralColor.antiDown.bar.tau) ((TensorSpecies.basisIdxCongr ⋯) ((Equiv.cast ⋯).symm x₂))) All goals completed! 🐙

F. Conjugation

Reality is a physical input the bare species cannot express: that the anti-chiral fields are the complex conjugates of the chiral ones, that the Kähler metric is Hermitian, that the F-term potential is real. Each is a statement that some quantity equals its own conjugate, so it can only be phrased once conjugation is available. This section exposes that operation for the two shapes the sector actually conjugates — the scalar W and the holomorphic covector D_I W — and certifies on components that it is honest complex conjugation.

Conjugation is bundled into chiralTensor itself (§E): as a ConjTensorSpecies it carries bar beside τ, and the framework supplies the conjugation map conjT and its laws (conjT_smul, conjT_conjT, conjT_contrT, conjT_eq_permT_iff) once, abstractly, against any ConjTensorSpecies. The chiral sector's conjugation flips holomorphy (ChiralColor.bar) while preserving variance, and through chiralTensor.conjT the reality and Hermiticity conditions are phrased. The basis index type ι is the same for every colour, so the identification barIdx_eq is rfl and the component reindexing is the identity.

The following normalize the output of (chiralTensor (ι := ι)).conjT back to the canonical colour lists for scalar and anti-holomorphic covector tensors respectively.

Conjugation of a scalar tensor, normalized back to the scalar colour list ![].

def conjScalar (t : (chiralTensor (ι := ι)).Tensor ![]) : (chiralTensor (ι := ι)).Tensor ![] := permT id ⟨Function.bijective_id, fun i => ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nt:chiralTensor.Tensor ![]i:Fin 0⊢ chiralTensor.bar (![] (id i)) = ![] i All goals completed! 🐙⟩ ((chiralTensor (ι := ι)).conjT t)

Conjugation of a holomorphic covector, normalized to the anti-holomorphic covector colour list ![antiDown].

def conjChiralCovector (t : (chiralTensor (ι := ι)).Tensor ![chiralDown]) : (chiralTensor (ι := ι)).Tensor ![antiDown] := permT ![0] ⟨ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nt:chiralTensor.Tensor ![chiralDown]⊢ Function.Bijective ![0] All goals completed! 🐙, fun i => ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nt:chiralTensor.Tensor ![chiralDown]i:Fin (Nat.succ 0)⊢ chiralTensor.bar (![chiralDown] (![0] i)) = ![antiDown] i ι:Typeinst✝⁵:Fintype ιinst✝⁴:DecidableEq ιM:Type u_1inst✝³:AddCommGroup Minst✝²:Module ℂ MN:Type u_2inst✝¹:AddCommGroup Ninst✝:Module ℂ Nt:chiralTensor.Tensor ![chiralDown]⊢ chiralTensor.bar (![chiralDown] (![0] ((fun i => i) ⟨0, ⋯⟩))) = ![antiDown] ((fun i => i) ⟨0, ⋯⟩); All goals completed! 🐙⟩ ((chiralTensor (ι := ι)).conjT t)

For scalar tensors, toField of the normalized tensor conjugate is the complex conjugate of toField.

ι:Typeinst✝¹:Fintype ιinst✝:DecidableEq ιt:chiralTensor.Tensor ![]⊢ (((basis fun i => chiralTensor.bar (![] i)).repr (chiralTensor.conjT t)) fun j => j.elim0) = star (((basis ![]).repr t) fun j => j.elim0) ι:Typeinst✝¹:Fintype ιinst✝:DecidableEq ιt:chiralTensor.Tensor ![]⊢ ((componentMap (chiralTensor.bar ∘ ![])) (chiralTensor.conjT t) fun j => j.elim0) = star (((basis ![]).repr t) fun j => j.elim0) erw [ι:Typeinst✝¹:Fintype ιinst✝:DecidableEq ιt:chiralTensor.Tensor ![]⊢ star ((componentMap ![]) t ((chiralTensor.componentReindex ![]) fun j => j.elim0)) = star (((basis ![]).repr t) fun j => j.elim0)ι:Typeinst✝¹:Fintype ιinst✝:DecidableEq ιt:chiralTensor.Tensor ![]⊢ star ((componentMap ![]) t ((chiralTensor.componentReindex ![]) fun j => j.elim0)) = star (((basis ![]).repr t) fun j => j.elim0) All goals completed! 🐙

Component formula for the holomorphic covector conjugate: the ![I] basis component of conjChiralCovector t is the complex conjugate of the ![I] component of t.

ι:Typeinst✝¹:Fintype ιinst✝:DecidableEq ιt:chiralTensor.Tensor ![chiralDown]I:ι⊢ (((basis fun i => chiralTensor.bar (![chiralDown] i)).repr (chiralTensor.conjT t)) fun i => (basisIdxCongr ⋯) (![I] (IsReindexing.inv ![0] ⋯ i))) = star (((basis ![chiralDown]).repr t) ![I]) ι:Typeinst✝¹:Fintype ιinst✝:DecidableEq ιt:chiralTensor.Tensor ![chiralDown]I:ι⊢ ((componentMap (chiralTensor.bar ∘ ![chiralDown])) (chiralTensor.conjT t) fun i => (basisIdxCongr ⋯) (![I] (IsReindexing.inv ![0] ⋯ i))) = star (((basis ![chiralDown]).repr t) ![I]) erw [ι:Typeinst✝¹:Fintype ιinst✝:DecidableEq ιt:chiralTensor.Tensor ![chiralDown]I:ι⊢ star ((componentMap ![chiralDown]) t ((chiralTensor.componentReindex ![chiralDown]) fun i => (basisIdxCongr ⋯) (![I] (IsReindexing.inv ![0] ⋯ i)))) = star (((basis ![chiralDown]).repr t) ![I])ι:Typeinst✝¹:Fintype ιinst✝:DecidableEq ιt:chiralTensor.Tensor ![chiralDown]I:ι⊢ star ((componentMap ![chiralDown]) t ((chiralTensor.componentReindex ![chiralDown]) fun i => (basisIdxCongr ⋯) (![I] (IsReindexing.inv ![0] ⋯ i)))) = star (((basis ![chiralDown]).repr t) ![I]) ι:Typeinst✝¹:Fintype ιinst✝:DecidableEq ιt:chiralTensor.Tensor ![chiralDown]I:ι⊢ (componentMap ![chiralDown]) t ((chiralTensor.componentReindex ![chiralDown]) fun i => (basisIdxCongr ⋯) (![I] (IsReindexing.inv ![0] ⋯ i))) = ((basis ![chiralDown]).repr t) ![I] ι:Typeinst✝¹:Fintype ιinst✝:DecidableEq ιt:chiralTensor.Tensor ![chiralDown]I:ι⊢ ((chiralTensor.componentReindex ![chiralDown]) fun i => (basisIdxCongr ⋯) (![I] (IsReindexing.inv ![0] ⋯ i))) = ![I] ι:Typeinst✝¹:Fintype ιinst✝:DecidableEq ιt:chiralTensor.Tensor ![chiralDown]I:ιi:Fin (Nat.succ 0)⊢ (chiralTensor.componentReindex ![chiralDown]) (fun i => (basisIdxCongr ⋯) (![I] (IsReindexing.inv ![0] ⋯ i))) i = ![I] i ι:Typeinst✝¹:Fintype ιinst✝:DecidableEq ιt:chiralTensor.Tensor ![chiralDown]I:ι⊢ (chiralTensor.componentReindex ![chiralDown]) (fun i => (basisIdxCongr ⋯) (![I] (IsReindexing.inv ![0] ⋯ i))) ((fun i => i) ⟨0, ⋯⟩) = ![I] ((fun i => i) ⟨0, ⋯⟩) All goals completed! 🐙

Conjugation of a holomorphic covector is additive.

@[simp] lemma conjChiralCovector_add (t₁ t₂ : (chiralTensor (ι := ι)).Tensor ![chiralDown]) : conjChiralCovector (t₁ + t₂) = conjChiralCovector t₁ + conjChiralCovector t₂ := ι:Typeinst✝¹:Fintype ιinst✝:DecidableEq ιt₁:chiralTensor.Tensor ![chiralDown]t₂:chiralTensor.Tensor ![chiralDown]⊢ conjChiralCovector (t₁ + t₂) = conjChiralCovector t₁ + conjChiralCovector t₂ All goals completed! 🐙

Conjugation of a holomorphic covector is conjugate-linear: a scalar r pulls out as star r.

@[simp] lemma conjChiralCovector_smul (r : ℂ) (t : (chiralTensor (ι := ι)).Tensor ![chiralDown]) : conjChiralCovector (r • t) = star r • conjChiralCovector t := ι:Typeinst✝¹:Fintype ιinst✝:DecidableEq ιr:ℂt:chiralTensor.Tensor ![chiralDown]⊢ conjChiralCovector (r • t) = star r • conjChiralCovector t All goals completed! 🐙