ICC transfer for Zhou §5. Since the acting group is SL₃(R) × Sp₄(F₂), the proof uses the paper's three-case criterion on the concrete product quotient.

@[reducible, inline]

abbrev Connes.PaperICC.N : Type

The N construction used in the Connes rigidity formalization.

Equations

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

@[reducible, inline]

abbrev Connes.PaperICC.S : Type

The S construction used in the Connes rigidity formalization.

Equations

• Connes.PaperICC.S = Connes.SpecialLinear.SL3

@[reducible, inline]

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

The Q construction used in the Connes rigidity formalization.

Equations

• Connes.PaperICC.Q = Connes.Construction.PaperKernel.Q

@[reducible, inline]

abbrev Connes.PaperICC.H : Type

The H construction used in the Connes rigidity formalization.

Equations

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

structure Connes.PaperICC.ActionData (action : H →* MulAut N) : Prop

Infinite SL₃ orbits of nonzero kernel elements. Paper: §5.

• kernel_orbit (a : N) : a ≠ 1 → (Set.range fun (s : S) => (action (s, 1)) a).Infinite
• q_displacement (q : ↥Q) : q ≠ 1 → ∃ (a : N), a * ((action (1, q)) a)⁻¹ ≠ 1 ∧ (Set.range fun (s : S) => (action (s, 1)) (a * ((action (1, q)) a)⁻¹)).Infinite

def Connes.PaperICC.projectionS (action : H →* MulAut N) : Construction.PaperKernel.paperGammaCarrier action →* S

The projection of the actual semidirect product to the SL₃ factor.

Equations

• Connes.PaperICC.projectionS action = { toFun := fun (x : Connes.Construction.PaperKernel.paperGammaCarrier action) => x.right.1, map_one' := ⋯, map_mul' := ⋯ }

theorem Connes.PaperICC.isICC_of_product_quotient (action : H →* MulAut N) (data : ActionData action) : IsICC (Construction.PaperKernel.paperGammaOf action)

Three-case ICC transfer for the product quotient in Zhou §5.