The finite extensions component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.PaperFiniteExtensions.N : Type

The N construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFiniteExtensions.N = Multiplicative Connes.Construction.PaperKernel.D

@[reducible, inline]

abbrev Connes.PaperFiniteExtensions.S : Type

The S construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFiniteExtensions.S = Connes.SpecialLinear.SL3

@[reducible, inline]

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

The Q construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFiniteExtensions.Q = Connes.Construction.PaperKernel.Q

noncomputable def Connes.PaperFiniteExtensions.quotientQ (action : Construction.H →* MulAut N) : Construction.PaperKernel.paperGammaCarrier action →* ↥Q

The finite quotient map records the Sp₄(F₂) coordinate. Paper: §4.

Equations

• Connes.PaperFiniteExtensions.quotientQ action = (MonoidHom.snd Connes.PaperFiniteExtensions.S ↥Connes.PaperFiniteExtensions.Q).comp SemidirectProduct.rightHom

theorem Connes.PaperFiniteExtensions.quotientQ_surjective (action : Construction.H →* MulAut N) : Function.Surjective ⇑(quotientQ action)

noncomputable def Connes.PaperFiniteExtensions.liftLambda (action : Construction.H →* MulAut N) : PaperPropertyT.lambdaCarrier action →* Construction.PaperKernel.paperGammaCarrier action

The intermediate semidirect product embeds as the kernel of the finite quotient. Paper: §4.

Equations

• Connes.PaperFiniteExtensions.liftLambda action = SemidirectProduct.map (MonoidHom.id Connes.PaperFiniteExtensions.N) Connes.PaperPropertyT.sl3ToActingGroup ⋯

noncomputable def Connes.PaperFiniteExtensions.lambdaToSubgroup (action : Construction.H →* MulAut N) : PaperPropertyT.lambdaCarrier action ≃* ↥(quotientQ action).ker

The intermediate group is identified with the finite-index kernel. Paper: §4.

Equations

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

noncomputable def Connes.PaperFiniteExtensions.finiteExtension (action : Construction.H →* MulAut N) : PropertyTTransfer.FiniteExtensionData (PaperPropertyT.lambdaOf action) (Construction.PaperKernel.paperGammaOf action) PaperPropertyT.finiteSymplecticGroup

The finite extension associated to a kernel action. Paper: §4.

Equations

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