The paper actions component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.Construction.PaperKernel.Q : Submonoid (Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) (ZMod 2))

The Q construction used in the Connes rigidity formalization.

Equations

• Connes.Construction.PaperKernel.Q = Connes.OpenAIPort.ModTwoSymplecticGroup

@[reducible, inline]

abbrev Connes.Construction.PaperKernel.SymplecticIndex : Type

The SymplecticIndex construction used in the Connes rigidity formalization.

Equations

• Connes.Construction.PaperKernel.SymplecticIndex = Connes.OpenAIPort.SymplecticIndex

noncomputable def Connes.Construction.PaperKernel.sl3AAction : SpecialLinear.SL3 →* A ≃ₗ[k] A

The SL₃ action on the polynomial module. Paper: §2.

Equations

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

noncomputable def Connes.Construction.PaperKernel.sl3TensorAction (l : SpecialLinear.SL3) : TensorAA →ₗ[k] TensorAA

The diagonal SL₃ action on the tensor square. Paper: §2.

Equations

• Connes.Construction.PaperKernel.sl3TensorAction l = TensorProduct.map ↑(Connes.Construction.PaperKernel.sl3AAction l) ↑(Connes.Construction.PaperKernel.sl3AAction l)

noncomputable def Connes.Construction.PaperKernel.sl3CAction (l : SpecialLinear.SL3) : ↥C →ₗ[k] ↥C

The diagonal SL₃ action restricted to the fixed tensor module. Paper: §2.

Equations

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

def Connes.Construction.PaperKernel.qVAction (q : ↥Q) : PaperV ≃ₗ[k] PaperV

The natural linear action of Q on the finite module. Paper: §2.

Equations

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

def Connes.Construction.PaperKernel.qVActionHom : ↥Q →* PaperV ≃ₗ[k] PaperV

The Q action homomorphism on the finite module. Paper: §2.

Equations

• Connes.Construction.PaperKernel.qVActionHom = { toFun := Connes.Construction.PaperKernel.qVAction, map_one' := Connes.Construction.PaperKernel.qVActionHom._proof_2, map_mul' := ⋯ }

def Connes.Construction.PaperKernel.qVStarActionHom : ↥Q →* VStar ≃ₗ[k] VStar

The contragredient Q action on the finite dual. Paper: §2.

Equations

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

@[simp]

theorem Connes.Construction.PaperKernel.sl3CAction_diagonal (l : SpecialLinear.SL3) (a : A) : (sl3CAction l) (diagonal a) = diagonal ((sl3AAction l) a)

noncomputable def Connes.Construction.PaperKernel.squareSpan : Submodule k TensorAA

Span of square tensors in the tensor square. Paper: §2.

Equations

• Connes.Construction.PaperKernel.squareSpan = Submodule.span Connes.Construction.k (Set.range fun (a : Connes.Construction.A) => a ⊗ₜ[Connes.Construction.k] a)

structure Connes.Construction.PaperKernel.SquareSpanData : Prop

The paper's missing spanning statement for the fixed tensor module. Paper: §2.

• squares_span (c : ↥C) : ↑c ∈ squareSpan

theorem Connes.Construction.PaperKernel.delta_surjective : Function.Surjective ⇑delta

The coefficientwise candidate is surjective. Paper: §2.

theorem Connes.Construction.PaperKernel.deltaTensor_equivariant_on_squareSpan (l : SpecialLinear.SL3) {x : TensorAA} (hx : x ∈ squareSpan) : deltaTensor ((sl3TensorAction l) x) = (sl3AAction l) (deltaTensor x)

The coefficientwise candidate intertwines the tensor action on squares. Paper: §2.

theorem Connes.Construction.PaperKernel.delta_equivariant_of_squareSpanData (l : SpecialLinear.SL3) (data : SquareSpanData) (c : ↥C) : delta ((sl3CAction l) c) = (sl3AAction l) (delta c)

The candidate is equivariant once the paper's spanning lemma is supplied. Paper: §2.