This file proves the concrete quotient and module transport in Zhou's Section 6 argument. It uses public project statements only.

noncomputable def Connes.PaperCharacteristicTransport.qSubgroup : Subgroup H

The qSubgroup construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCharacteristicTransport.qSubgroup = (MonoidHom.fst Connes.PaperCharacteristicTransport.S ↥Connes.PaperCharacteristicTransport.Q).ker

theorem Connes.PaperCharacteristicTransport.qSubgroup_normal : qSubgroup.Normal

The quotient factor is normal as a direct-product kernel (Zhou §6).

theorem Connes.PaperCharacteristicTransport.qSubgroup_eq_range : qSubgroup = (MonoidHom.inr S ↥Q).range

theorem Connes.PaperCharacteristicTransport.qSubgroup_finite : (↑qSubgroup).Finite

theorem Connes.PaperCharacteristicTransport.finiteNormalSubgroup_sl3_bot (L : Subgroup S) (hfinite : (↑L).Finite) (hnormal : L.Normal) : L = ⊥

theorem Connes.PaperCharacteristicTransport.finiteNormalSubgroup_le_q (R : Subgroup H) (hfinite : (↑R).Finite) (hnormal : R.Normal) : R ≤ qSubgroup

theorem Connes.PaperCharacteristicTransport.qSubgroup_characteristic (f : H ≃* H) : Subgroup.map f.toMonoidHom qSubgroup = qSubgroup

noncomputable def Connes.PaperCharacteristicTransport.qSubgroupEquiv : ↥Q ≃* ↥qSubgroup

The qSubgroupEquiv construction used in the Connes rigidity formalization.

Equations

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

def Connes.PaperCharacteristicTransport.restrictEquiv {G : Type u_1} {M : Type u_2} [Group G] [Group M] (f : G ≃* M) {K : Subgroup G} {L : Subgroup M} (h : Subgroup.map f.toMonoidHom K = L) : ↥K ≃* ↥L

A group isomorphism restricts to an invariant subgroup (Zhou §6).

Equations

• Connes.PaperCharacteristicTransport.restrictEquiv f h = { toFun := fun (x : ↥K) => ⟨f ↑x, ⋯⟩, invFun := fun (y : ↥L) => ⟨f.symm ↑y, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

noncomputable def Connes.PaperCharacteristicTransport.quotientMap (action₁ action₂ : H →* MulAut N) (f : Construction.PaperKernel.paperGammaCarrier action₁ ≃* Construction.PaperKernel.paperGammaCarrier action₂) : H →* H

The quotient homomorphism induced by a semidirect-product isomorphism (Zhou §6).

Equations

• Connes.PaperCharacteristicTransport.quotientMap action₁ action₂ f = SemidirectProduct.rightHom.comp (f.toMonoidHom.comp SemidirectProduct.inr)

theorem Connes.PaperCharacteristicTransport.semidirect_decompose (action : H →* MulAut N) (x : Construction.PaperKernel.paperGammaCarrier action) : x = SemidirectProduct.inl x.left * SemidirectProduct.inr x.right

Every semidirect element splits into kernel and quotient coordinates (Zhou §6).

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

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

The quotientEquiv construction used in the Connes rigidity formalization.

Equations

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

noncomputable def Connes.PaperCharacteristicTransport.quotientAutomorphism (action₁ action₂ : H →* MulAut N) (f : Construction.PaperKernel.paperGammaCarrier action₁ ≃* Construction.PaperKernel.paperGammaCarrier action₂) (hchar : Subgroup.map f.toMonoidHom (kernelSubgroup action₁) = kernelSubgroup action₂) : ↥Q ≃* ↥Q

The induced quotient automorphism restricts to the finite factor (Zhou §6).

Equations

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

noncomputable def Connes.PaperCharacteristicTransport.kernelSubgroupEquiv (action : H →* MulAut N) : N ≃* ↥(kernelSubgroup action)

Coordinates identify the kernel with the semidirect kernel subgroup (Zhou §6).

Equations

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

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

The kernel map induced by a group isomorphism (Zhou §6).

Equations

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

theorem Connes.PaperCharacteristicTransport.kernelMap_apply_left (action₁ action₂ : H →* MulAut N) (f : Construction.PaperKernel.paperGammaCarrier action₁ ≃* Construction.PaperKernel.paperGammaCarrier action₂) (hchar : Subgroup.map f.toMonoidHom (kernelSubgroup action₁) = kernelSubgroup action₂) (n : N) : (kernelMap action₁ action₂ f hchar) n = (f (SemidirectProduct.inl n)).left

The kernel map is read from the kernel coordinate (Zhou §6).

theorem Connes.PaperCharacteristicTransport.kernelMap_inl (action₁ action₂ : H →* MulAut N) (f : Construction.PaperKernel.paperGammaCarrier action₁ ≃* Construction.PaperKernel.paperGammaCarrier action₂) (hchar : Subgroup.map f.toMonoidHom (kernelSubgroup action₁) = kernelSubgroup action₂) (n : N) : SemidirectProduct.inl ((kernelMap action₁ action₂ f hchar) n) = f (SemidirectProduct.inl n)

theorem Connes.PaperCharacteristicTransport.inl_conjugation_ignores_kernel (action : H →* MulAut N) (a n : N) (h : H) : SemidirectProduct.inl a * SemidirectProduct.inr h * SemidirectProduct.inl n * (SemidirectProduct.inl a * SemidirectProduct.inr h)⁻¹ = SemidirectProduct.inr h * SemidirectProduct.inl n * SemidirectProduct.inr h⁻¹

theorem Connes.PaperCharacteristicTransport.kernelMap_intertwines (action₁ action₂ : H →* MulAut N) (f : Construction.PaperKernel.paperGammaCarrier action₁ ≃* Construction.PaperKernel.paperGammaCarrier action₂) (hchar : Subgroup.map f.toMonoidHom (kernelSubgroup action₁) = kernelSubgroup action₂) (h : H) (n : N) : (kernelMap action₁ action₂ f hchar) ((action₁ h) n) = (action₂ ((quotientEquiv action₁ action₂ f hchar) h)) ((kernelMap action₁ action₂ f hchar) n)

noncomputable def Connes.PaperCharacteristicTransport.kernelLinearEquiv (action₁ action₂ : H →* MulAut N) (f : Construction.PaperKernel.paperGammaCarrier action₁ ≃* Construction.PaperKernel.paperGammaCarrier action₂) (hchar : Subgroup.map f.toMonoidHom (kernelSubgroup action₁) = kernelSubgroup action₂) : Construction.PaperKernel.D ≃ₗ[Construction.k] Construction.PaperKernel.D

The kernelLinearEquiv construction used in the Connes rigidity formalization.

Equations

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

theorem Connes.PaperCharacteristicTransport.kernelLinearEquiv_intertwines (f : Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaOneHom ≃* Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaTwoHom) (hchar : Subgroup.map f.toMonoidHom (kernelSubgroup Construction.PaperKernel.paperThetaOneHom) = kernelSubgroup Construction.PaperKernel.paperThetaTwoHom) (h : H) (d : Construction.PaperKernel.D) : (kernelLinearEquiv Construction.PaperKernel.paperThetaOneHom Construction.PaperKernel.paperThetaTwoHom f hchar) ((Construction.PaperKernel.paperThetaOneLinearHom h) d) = (Construction.PaperKernel.paperThetaTwoLinearHom ((quotientEquiv Construction.PaperKernel.paperThetaOneHom Construction.PaperKernel.paperThetaTwoHom f hchar) h)) ((kernelLinearEquiv Construction.PaperKernel.paperThetaOneHom Construction.PaperKernel.paperThetaTwoHom f hchar) d)

The transported linear kernel map respects the paper actions (Zhou §6).

theorem Connes.PaperCharacteristicTransport.quotientAutomorphism_lift (f : Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaOneHom ≃* Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaTwoHom) (hchar : Subgroup.map f.toMonoidHom (kernelSubgroup Construction.PaperKernel.paperThetaOneHom) = kernelSubgroup Construction.PaperKernel.paperThetaTwoHom) (q : ↥Q) : (quotientEquiv Construction.PaperKernel.paperThetaOneHom Construction.PaperKernel.paperThetaTwoHom f hchar) (1, q) = (1, (quotientAutomorphism Construction.PaperKernel.paperThetaOneHom Construction.PaperKernel.paperThetaTwoHom f hchar) q)

noncomputable def Connes.PaperCharacteristicTransport.moduleMapOfLinearEquiv (ρ σ : Representation Construction.k (↥Q) Construction.PaperKernel.D) (e : Construction.PaperKernel.D ≃ₗ[Construction.k] Construction.PaperKernel.D) (he : ∀ (q : ↥Q) (d : Construction.PaperKernel.D), e ((ρ q) d) = (σ q) (e d)) : ρ.asModule →ₗ[PaperNonisomorphism.Ring] σ.asModule

The moduleMapOfLinearEquiv construction used in the Connes rigidity formalization.

Equations

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

theorem Connes.PaperCharacteristicTransport.moduleMapOfLinearEquiv_bijective (ρ σ : Representation Construction.k (↥Q) Construction.PaperKernel.D) (e : Construction.PaperKernel.D ≃ₗ[Construction.k] Construction.PaperKernel.D) (he : ∀ (q : ↥Q) (d : Construction.PaperKernel.D), e ((ρ q) d) = (σ q) (e d)) : Function.Bijective ⇑(moduleMapOfLinearEquiv ρ σ e he)

The induced group-algebra map is bijective (Zhou §6).

noncomputable def Connes.PaperCharacteristicTransport.paperModuleIntertwining (f : Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaOneHom ≃* Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaTwoHom) (hchar : Subgroup.map f.toMonoidHom (kernelSubgroup Construction.PaperKernel.paperThetaOneHom) = kernelSubgroup Construction.PaperKernel.paperThetaTwoHom) : PaperNonisomorphism.qRepresentationOne.IntertwiningMap (PaperNonisomorphism.qRepresentationTwoAlong (quotientAutomorphism Construction.PaperKernel.paperThetaOneHom Construction.PaperKernel.paperThetaTwoHom f hchar))

The paperModuleIntertwining construction used in the Connes rigidity formalization.

Equations

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

noncomputable def Connes.PaperCharacteristicTransport.paperModuleLinearMap (f : Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaOneHom ≃* Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaTwoHom) (hchar : Subgroup.map f.toMonoidHom (kernelSubgroup Construction.PaperKernel.paperThetaOneHom) = kernelSubgroup Construction.PaperKernel.paperThetaTwoHom) : PaperNonisomorphism.qRepresentationOne.asModule →ₗ[PaperNonisomorphism.Ring] (PaperNonisomorphism.qRepresentationTwoAlong (quotientAutomorphism Construction.PaperKernel.paperThetaOneHom Construction.PaperKernel.paperThetaTwoHom f hchar)).asModule

The concrete module map induced by a group isomorphism (Zhou §6).

Equations

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

theorem Connes.PaperCharacteristicTransport.paperModuleLinearMap_bijective (f : Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaOneHom ≃* Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaTwoHom) (hchar : Subgroup.map f.toMonoidHom (kernelSubgroup Construction.PaperKernel.paperThetaOneHom) = kernelSubgroup Construction.PaperKernel.paperThetaTwoHom) : Function.Bijective ⇑(paperModuleLinearMap f hchar)