The split abelian extension component of the Connes rigidity formalization.

structure Connes.SplitAbelianExtension (A : Type u) [AddCommGroup A] (G H : CountableDiscreteGroup) : Type u

Split abelian extension data for the spectral property-(T) argument. Paper: §4.

• inclusion : Multiplicative A →* G.Carrier

  The inclusion component of SplitAbelianExtension.

• quotient : G.Carrier →* H.Carrier

  The quotient component of SplitAbelianExtension.

• splitting : H.Carrier →* G.Carrier

  The splitting component of SplitAbelianExtension.

• quotient_splitting : self.quotient.comp self.splitting = MonoidHom.id H.Carrier
• exact : self.quotient.ker = self.inclusion.range
• action : H.Carrier →* Multiplicative (AddAut A)

  The action component of SplitAbelianExtension.

• conjugation (h : H.Carrier) (a : A) : self.splitting h * self.inclusion (Multiplicative.ofAdd a) * (self.splitting h)⁻¹ = self.inclusion (Multiplicative.ofAdd ((Multiplicative.toAdd (self.action h)) a))

@[simp]

theorem Connes.SplitAbelianExtension.quotient_splitting_apply {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) (h : H.Carrier) : E.quotient (E.splitting h) = h

The split quotient evaluates to the identity on its section. Paper: §4.

theorem Connes.SplitAbelianExtension.exists_kernel_mul_splitting {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) (g : G.Carrier) : ∃ (a : A) (h : H.Carrier), g = E.inclusion (Multiplicative.ofAdd a) * E.splitting h

Every extension element has kernel-section coordinates. Paper: §4.

theorem Connes.SplitAbelianExtension.invariant_of_kernel_and_quotient {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G.Carrier V) (ξ : V) (hkernel : ∀ (a : A), ↑(π (E.inclusion (Multiplicative.ofAdd a))) ξ = ξ) (hquotient : ∀ (h : H.Carrier), ↑(π (E.splitting h)) ξ = ξ) : π.IsInvariant ξ

Kernel and quotient fixedness give full invariance. Paper: §4.