The normal fixed component of the Connes rigidity formalization.

def Connes.normalFixedSubmodule {G : Type u} [Group G] {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : Subgroup G) (π : UnitaryRepresentation G K) : Submodule ℂ K

Vectors fixed by a subgroup under a unitary representation. Paper: §4.

Equations

• Connes.normalFixedSubmodule N π = { carrier := {x : K | ∀ (n : ↥N), ↑(π ↑n) x = x}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Connes.mem_normalFixedSubmodule {G : Type u} [Group G] {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : Subgroup G) (π : UnitaryRepresentation G K) (x : K) : x ∈ normalFixedSubmodule N π ↔ ∀ (n : ↥N), ↑(π ↑n) x = x

theorem Connes.normalFixedSubmodule_isClosed {G : Type u} [Group G] {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : Subgroup G) (π : UnitaryRepresentation G K) : IsClosed ↑(normalFixedSubmodule N π)

The fixed subspace is closed, hence complete. Paper: §4.

instance Connes.normalFixedSubmodule_completeSpace {G : Type u} [Group G] {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : Subgroup G) (π : UnitaryRepresentation G K) : CompleteSpace ↥(normalFixedSubmodule N π)

theorem Connes.unitary_mem_normalFixedSubmodule {G : Type u} [Group G] {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : Subgroup G) [N.Normal] (π : UnitaryRepresentation G K) (g : G) {x : K} (hx : x ∈ normalFixedSubmodule N π) : ↑(π g) x ∈ normalFixedSubmodule N π

Normality makes the fixed subspace invariant. Paper: §4.

theorem Connes.unitary_mem_normalFixedSubmodule_orthogonal {G : Type u} [Group G] {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : Subgroup G) [N.Normal] (π : UnitaryRepresentation G K) (g : G) {x : K} (hx : x ∈ (normalFixedSubmodule N π)ᗮ) : ↑(π g) x ∈ (normalFixedSubmodule N π)ᗮ

The orthogonal complement is invariant as well. Paper: §4.

noncomputable def Connes.normalFixedLinearIsometryEquiv {G : Type u} [Group G] {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : Subgroup G) [N.Normal] (π : UnitaryRepresentation G K) (g : G) : ↥(normalFixedSubmodule N π) ≃ₗᵢ[ℂ] ↥(normalFixedSubmodule N π)

The normalFixedLinearIsometryEquiv construction used in the Connes rigidity formalization.

Equations

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

noncomputable def Connes.normalFixedRepresentation {G : Type u} [Group G] {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : Subgroup G) [N.Normal] (π : UnitaryRepresentation G K) : UnitaryRepresentation G ↥(normalFixedSubmodule N π)

The restricted representation on the fixed subspace. Paper: §4.

Equations

• Connes.normalFixedRepresentation N π = { toFun := fun (g : G) => Unitary.linearIsometryEquiv.symm (Connes.normalFixedLinearIsometryEquiv N π g), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Connes.normalFixedRepresentation_apply {G : Type u} [Group G] {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : Subgroup G) [N.Normal] (π : UnitaryRepresentation G K) (g : G) (x : ↥(normalFixedSubmodule N π)) : ↑(↑((normalFixedRepresentation N π) g) x) = ↑(π g) ↑x

theorem Connes.normalFixedRepresentation_apply_eq_one {G : Type u} [Group G] {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : Subgroup G) [N.Normal] (π : UnitaryRepresentation G K) (n : G) (hn : n ∈ N) : (normalFixedRepresentation N π) n = 1

noncomputable def Connes.normalFixedQuotientRepresentation {G : Type u} [Group G] {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : Subgroup G) [N.Normal] (π : UnitaryRepresentation G K) : UnitaryRepresentation (G ⧸ N) ↥(normalFixedSubmodule N π)

The quotient representation on the normal-fixed subspace. Paper: §4.

Equations

• Connes.normalFixedQuotientRepresentation N π = QuotientGroup.lift N (Connes.normalFixedRepresentation N π) ⋯

theorem Connes.normalFixedQuotientRepresentation_apply_mk {G : Type u} [Group G] {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : Subgroup G) [N.Normal] (π : UnitaryRepresentation G K) (g : G) (x : ↥(normalFixedSubmodule N π)) : ↑(↑((normalFixedQuotientRepresentation N π) ((QuotientGroup.mk' N) g)) x) = ↑(π g) ↑x

noncomputable def Connes.normalFixedOrthogonalLinearIsometryEquiv {G : Type u} [Group G] {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : Subgroup G) [N.Normal] (π : UnitaryRepresentation G K) (g : G) : ↥(normalFixedSubmodule N π)ᗮ ≃ₗᵢ[ℂ] ↥(normalFixedSubmodule N π)ᗮ

The normalFixedOrthogonalLinearIsometryEquiv construction used in the Connes rigidity formalization.

Equations

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

noncomputable def Connes.normalFixedOrthogonalRepresentation {G : Type u} [Group G] {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : Subgroup G) [N.Normal] (π : UnitaryRepresentation G K) : UnitaryRepresentation G ↥(normalFixedSubmodule N π)ᗮ

The restricted representation on the orthogonal complement. Paper: §4.

Equations

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

@[simp]

theorem Connes.normalFixedOrthogonalRepresentation_apply {G : Type u} [Group G] {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : Subgroup G) [N.Normal] (π : UnitaryRepresentation G K) (g : G) (x : ↥(normalFixedSubmodule N π)ᗮ) : ↑(↑((normalFixedOrthogonalRepresentation N π) g) x) = ↑(π g) ↑x

theorem Connes.normalFixedOrthogonalRepresentation_no_fixed {G : Type u} [Group G] {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : Subgroup G) [N.Normal] (π : UnitaryRepresentation G K) (x : ↥(normalFixedSubmodule N π)ᗮ) (hx : ∀ (n : ↥N), ↑((normalFixedOrthogonalRepresentation N π) ↑n) x = x) : x = 0

theorem Connes.normalFixed_starProjection_commute {G : Type u} [Group G] {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : Subgroup G) [N.Normal] (π : UnitaryRepresentation G K) (g : G) (x : K) : (normalFixedSubmodule N π).starProjection (↑(π g) x) = ↑(π g) ((normalFixedSubmodule N π).starProjection x)

The normal fixed projection commutes with the representation. Paper: §4.

theorem Connes.normalFixed_orthogonalResidual_displacement_le {G : Type u} [Group G] {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : Subgroup G) [N.Normal] (π : UnitaryRepresentation G K) (g : G) (x : K) : ‖↑(π g) (x - (normalFixedSubmodule N π).starProjection x) - (x - (normalFixedSubmodule N π).starProjection x)‖ ≤ ‖↑(π g) x - x‖

Passing to the orthogonal residual cannot increase displacement. Paper: §4.