The split extensions component of the Connes rigidity formalization.

noncomputable def Connes.PaperSplitExtensions.lambdaExtension (action : Construction.H →* MulAut (Multiplicative Construction.PaperKernel.D)) : SplitAbelianExtension Construction.PaperKernel.D (PaperPropertyT.lambdaOf action) SpecialLinear.sl3Group

The SL₃ semidirect product as a split abelian extension. Paper: §4.

Equations

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

theorem Connes.PaperSplitExtensions.lambdaExtension_inclusion (action : Construction.H →* MulAut (Multiplicative Construction.PaperKernel.D)) (a : Multiplicative Construction.PaperKernel.D) : (lambdaExtension action).inclusion a = SemidirectProduct.inl a

The kernel inclusion of the action-indexed extension is the semidirect product inclusion. Paper: §4.

theorem Connes.PaperSplitExtensions.lambdaExtension_quotient (action : Construction.H →* MulAut (Multiplicative Construction.PaperKernel.D)) (x : (PaperPropertyT.lambdaOf action).Carrier) : (lambdaExtension action).quotient x = x.right

The quotient of the action-indexed extension is the semidirect-product projection. Paper: §4.

theorem Connes.PaperSplitExtensions.lambdaExtension_splitting (action : Construction.H →* MulAut (Multiplicative Construction.PaperKernel.D)) (g : SpecialLinear.SL3) : (lambdaExtension action).splitting g = SemidirectProduct.inr g

The splitting of the action-indexed extension is the semidirect-product section. Paper: §4.

@[simp]

theorem Connes.PaperSplitExtensions.lambdaExtension_action (action : Construction.H →* MulAut (Multiplicative Construction.PaperKernel.D)) (g : SpecialLinear.SL3) : (lambdaExtension action).action g = ((MulAutMultiplicative Construction.PaperKernel.D).toMonoidHom.comp action) (PaperPropertyT.sl3ToActingGroup g)

The extension action is the restriction of the given action along the standard inclusion SL₃ → SL₃ × Sp₄(𝔽₂). Paper: §4.