The quadratic cocycle component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.OpenAIPort.ModTwoSymplecticGroup : Submonoid (Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) (ZMod 2))

The ModTwoSymplecticGroup construction used in the Connes rigidity formalization.

Equations

• Connes.OpenAIPort.ModTwoSymplecticGroup = Matrix.symplecticGroup (Fin 2) (ZMod 2)

@[instance_reducible]

instance Connes.OpenAIPort.modTwoSymplecticGroupDecidableMem : DecidablePred fun (A : Matrix SymplecticIndex SymplecticIndex (ZMod 2)) => A ∈ Matrix.symplecticGroup (Fin 2) (ZMod 2)

Equations

• Connes.OpenAIPort.modTwoSymplecticGroupDecidableMem A = decidable_of_iff (A * Matrix.J (Fin 2) (ZMod 2) * A.transpose = Matrix.J (Fin 2) (ZMod 2)) ⋯

@[instance_reducible]

instance Connes.OpenAIPort.instFintypeSubtypeMatrixSumFinOfNatNatZModMemSubmonoidModTwoSymplecticGroup : Fintype ↥ModTwoSymplecticGroup

Equations

• Connes.OpenAIPort.instFintypeSubtypeMatrixSumFinOfNatNatZModMemSubmonoidModTwoSymplecticGroup = Subtype.fintype (Membership.mem Connes.OpenAIPort.ModTwoSymplecticGroup)

def Connes.OpenAIPort.reducedSymplecticHom : ↥IntegralSymplecticGroup →* ↥ModTwoSymplecticGroup

The reducedSymplecticHom construction used in the Connes rigidity formalization.

Equations

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

@[simp]

theorem Connes.OpenAIPort.reducedSymplecticHom_coe (g : ↥IntegralSymplecticGroup) : ↑(reducedSymplecticHom g) = reducedMatrixHom g

Evaluation of matrix reduction. Paper: §2.

@[instance_reducible]

instance Connes.OpenAIPort.instDistribMulActionSubtypeMatrixSumFinOfNatNatZModMemSubmonoidModTwoSymplecticGroupModTwoSpace : DistribMulAction (↥ModTwoSymplecticGroup) ModTwoSpace

Equations

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

def Connes.OpenAIPort.modTwoBasis (i : SymplecticIndex) : ModTwoSpace

The modTwoBasis construction used in the Connes rigidity formalization.

Equations

• Connes.OpenAIPort.modTwoBasis i = Pi.single i 1

def Connes.OpenAIPort.finiteQuadraticCocycle (g : ↥ModTwoSymplecticGroup) : ModTwoSpace

The source-shaped quadratic cocycle. Paper: §2.

Equations

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

theorem Connes.OpenAIPort.modTwoSymplecticForm_eq_dotProduct (x y : ModTwoSpace) : modTwoSymplecticForm x y = x ⬝ᵥ (Matrix.J (Fin 2) (ZMod 2)).mulVec y

Dot-product form of the alternating pairing. Paper: §2.

theorem Connes.OpenAIPort.modTwoSymplecticForm_smul (g : ↥ModTwoSymplecticGroup) (x y : ModTwoSpace) : modTwoSymplecticForm (g • x) (g • y) = modTwoSymplecticForm x y

theorem Connes.OpenAIPort.modTwoSymplecticForm_add_right (x y z : ModTwoSpace) : modTwoSymplecticForm x (y + z) = modTwoSymplecticForm x y + modTwoSymplecticForm x z

def Connes.OpenAIPort.quadraticDefectLinear (g : ↥ModTwoSymplecticGroup) : ModTwoSpace →ₗ[ZMod 2] ZMod 2

The quadraticDefectLinear construction used in the Connes rigidity formalization.

Equations

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

def Connes.OpenAIPort.symplecticFunctional (d : ModTwoSpace) : ModTwoSpace →ₗ[ZMod 2] ZMod 2

The pairing functional associated to a finite vector. Paper: §2.

Equations

• Connes.OpenAIPort.symplecticFunctional d = { toFun := fun (w : Connes.OpenAIPort.ModTwoSpace) => Connes.OpenAIPort.modTwoSymplecticForm d w, map_add' := ⋯, map_smul' := ⋯ }

theorem Connes.OpenAIPort.finiteQuadraticCocycle_defining_identity (g : ↥ModTwoSymplecticGroup) (w : ModTwoSpace) : standardQuadraticForm (g⁻¹ • w) + standardQuadraticForm w = modTwoSymplecticForm (finiteQuadraticCocycle g) w

The quadratic defect is represented by its source cocycle. Paper: §2.

theorem Connes.OpenAIPort.modTwoSymplecticForm_nondegenerate {x y : ModTwoSpace} (h : ∀ (w : ModTwoSpace), modTwoSymplecticForm x w = modTwoSymplecticForm y w) : x = y

theorem Connes.OpenAIPort.modTwoSymplecticForm_add_left (x y z : ModTwoSpace) : modTwoSymplecticForm (x + y) z = modTwoSymplecticForm x z + modTwoSymplecticForm y z

theorem Connes.OpenAIPort.modTwoSymplecticForm_smul_left (g : ↥ModTwoSymplecticGroup) (x y : ModTwoSpace) : modTwoSymplecticForm (g • x) y = modTwoSymplecticForm x (g⁻¹ • y)

theorem Connes.OpenAIPort.finiteQuadraticCocycle_isCocycle : groupCohomology.IsCocycle₁ finiteQuadraticCocycle

def Connes.OpenAIPort.integralQuadraticCocycle (g : ↥IntegralSymplecticGroup) : ModTwoSpace

The integralQuadraticCocycle construction used in the Connes rigidity formalization.

Equations

• Connes.OpenAIPort.integralQuadraticCocycle g = Connes.OpenAIPort.finiteQuadraticCocycle (Connes.OpenAIPort.reducedSymplecticHom g)

theorem Connes.OpenAIPort.reducedSymplecticHom_smul (g : ↥IntegralSymplecticGroup) (w : ModTwoSpace) : reducedSymplecticHom g • w = g • w

theorem Connes.OpenAIPort.integralQuadraticCocycle_defining_identity (g : ↥IntegralSymplecticGroup) (w : ModTwoSpace) : standardQuadraticForm (g⁻¹ • w) + standardQuadraticForm w = modTwoSymplecticForm (integralQuadraticCocycle g) w

theorem Connes.OpenAIPort.integralQuadraticCocycle_isCocycle : groupCohomology.IsCocycle₁ integralQuadraticCocycle