This file proves the concrete characteristic-kernel transport needed by the Zhou-shaped nonisomorphism argument. It is independently written from the cited public mathematical source.

@[reducible, inline]

abbrev Connes.PaperCharacteristicTransport.N : Type

The N construction used in the Connes rigidity formalization.

Equations

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

@[reducible, inline]

abbrev Connes.PaperCharacteristicTransport.S : Type

The S construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCharacteristicTransport.S = Connes.SpecialLinear.SL3

@[reducible, inline]

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

The Q construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCharacteristicTransport.Q = Connes.Construction.PaperKernel.Q

@[reducible, inline]

abbrev Connes.PaperCharacteristicTransport.H : Type

The H construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCharacteristicTransport.H = (Connes.PaperCharacteristicTransport.S × ↥Connes.PaperCharacteristicTransport.Q)

noncomputable def Connes.PaperCharacteristicTransport.kernelSubgroup (action : H →* MulAut N) : Subgroup (Construction.PaperKernel.paperGammaCarrier action)

The kernelSubgroup construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCharacteristicTransport.kernelSubgroup action = SemidirectProduct.inl.range

theorem Connes.PaperCharacteristicTransport.mapCommutes {G : Type u_1} {M : Type u_2} [Group G] [Group M] (f : G →* M) (E : Subgroup G) (hcomm : ∀ (x y : ↥E), x * y = y * x) (x y : ↥(Subgroup.map f E)) : x * y = y * x

theorem Connes.PaperCharacteristicTransport.quotientImage_is_normal_commuting (action : H →* MulAut N) (E : Subgroup (Construction.PaperKernel.paperGammaCarrier action)) (hnormal : E.Normal) (hcomm : ∀ (x y : ↥E), x * y = y * x) : have R := Subgroup.map SemidirectProduct.rightHom E; R.Normal ∧ ∀ (x y : ↥R), x * y = y * x

theorem Connes.PaperCharacteristicTransport.sl3Image_is_bot (R : Subgroup H) (hnormal : R.Normal) (hcomm : ∀ (x y : ↥R), x * y = y * x) : Subgroup.map (MonoidHom.fst S ↥Q) R = ⊥

theorem Connes.PaperCharacteristicTransport.qImage_is_bot (R : Subgroup H) (hnormal : R.Normal) (hcomm : ∀ (x y : ↥R), x * y = y * x) : Subgroup.map (MonoidHom.snd S ↥Q) R = ⊥

theorem Connes.PaperCharacteristicTransport.paperSemidirectNormalAbelian_le_kernel (action : H →* MulAut N) (E : Subgroup (Construction.PaperKernel.paperGammaCarrier action)) (hnormal : E.Normal) (hcomm : ∀ (x y : ↥E), x * y = y * x) : E ≤ kernelSubgroup action

theorem Connes.PaperCharacteristicTransport.kernelSubgroup_normal (action : H →* MulAut N) : (kernelSubgroup action).Normal

theorem Connes.PaperCharacteristicTransport.kernelSubgroup_commuting (action : H →* MulAut N) (x y : ↥(kernelSubgroup action)) : x * y = y * x

theorem Connes.PaperCharacteristicTransport.kernelSubgroup_characteristic (action₁ action₂ : H →* MulAut N) (f : Construction.PaperKernel.paperGammaCarrier action₁ ≃* Construction.PaperKernel.paperGammaCarrier action₂) : Subgroup.map f.toMonoidHom (kernelSubgroup action₁) = kernelSubgroup action₂