Documentation

theorem ConnesRigidity.IsMinimizingAffinePair.sub_eq_of_norm_eq {G : Type u} [Group G] {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℂ V] {α : AffineHilbertAction G V} {K₁ K₂ : Subgroup G} {x₁ x₂ : V} (hmin : IsMinimizingAffinePair α K₁ K₂ x₁ x₂) {y₁ y₂ : V} (hy₁ : IsAffineFixed α K₁ y₁) (hy₂ : IsAffineFixed α K₂ y₂) (hdist : ‖y₁ - y₂‖ = ‖x₁ - x₂‖) :

x₁ - x₂ = y₁ - y₂

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.IsMinimizingAffinePair.sub_eq_normalizer_sub {G : Type u} [Group G] {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℂ V] {α : AffineHilbertAction G V} {K₁ K₂ : Subgroup G} {x₁ x₂ : V} (hmin : IsMinimizingAffinePair α K₁ K₂ x₁ x₂) (g : G) (hg₁ : g ∈ Subgroup.normalizer ↑K₁) (hg₂ : g ∈ Subgroup.normalizer ↑K₂) :

x₁ - x₂ = (α g) x₁ - (α g) x₂

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.IsMinimizingAffinePair.normalizer_fixed_of_no_linear_invariants {G : Type u} [Group G] {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] {α : AffineHilbertAction G V} {K₁ K₂ : Subgroup G} {x₁ x₂ : V} (hmin : IsMinimizingAffinePair α K₁ K₂ x₁ x₂) (hgen : K₁ ⊔ K₂ = ⊤) (hno : ∀ (x : V), (affineLinearRepresentation α).IsInvariant x → x = 0) (g : G) (hg₁ : g ∈ Subgroup.normalizer ↑K₁) (hg₂ : g ∈ Subgroup.normalizer ↑K₂) :

(α g) x₁ = x₁ ∧ (α g) x₂ = x₂

Cross-module support for the infinite Connes-rigidity construction.

structure ConnesRigidity.CornulierUltralimit.HilbertKernelRealization {I : Type u} (K : Matrix I I ℂ) :

Type (u + 1)

Cross-module support for the infinite Connes-rigidity construction.

carrier : Type u
The Hilbert-space carrier of the realization.
normed : NormedAddCommGroup self.carrier
The normed additive group structure on the carrier.
inner : InnerProductSpace ℂ self.carrier
The inner-product-space structure on the carrier.
complete : CompleteSpace self.carrier
vector : I → self.carrier
The realizing vector attached to each index.
gram (g h : I) : Inner.inner ℂ (self.vector g) (self.vector h) = K g h

Instances For

@[instance_reducible]

instance ConnesRigidity.CornulierUltralimit.hilbertKernelRealizationNormedAddCommGroup {I : Type u} {K : Matrix I I ℂ} (R : HilbertKernelRealization K) :

NormedAddCommGroup R.carrier

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.CornulierUltralimit.hilbertKernelRealizationNormedAddCommGroup R = R.normed

@[instance_reducible]

instance ConnesRigidity.CornulierUltralimit.hilbertKernelRealizationInnerProductSpace {I : Type u} {K : Matrix I I ℂ} (R : HilbertKernelRealization K) :

InnerProductSpace ℂ R.carrier

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.CornulierUltralimit.hilbertKernelRealizationInnerProductSpace R = R.inner

instance ConnesRigidity.CornulierUltralimit.hilbertKernelRealizationCompleteSpace {I : Type u} {K : Matrix I I ℂ} (R : HilbertKernelRealization K) :

CompleteSpace R.carrier

Cross-module support for the infinite Connes-rigidity construction.

noncomputable def ConnesRigidity.CornulierUltralimit.unitaryCocycleAffineAction {G H : Type u} [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (π : G →* H ≃ₗᵢ[ℂ ] H) (b : G → H) (hb : ∀ (g h : G), b (g * h) = b g + (π g) (b h)) :

G →* H ≃ᵃⁱ[ℂ ] H

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

def ConnesRigidity.CornulierUltralimit.markedPairAction {G I : Type u} [Group G] (ρ : G →* Equiv.Perm I) :

G →* Equiv.Perm (I × I)

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.CornulierUltralimit.markedPairAction ρ = { toFun := fun (g : G) => Equiv.prodCongr (ρ g) (ρ g), map_one' := ⋯, map_mul' := ⋯ }

Instances For

structure ConnesRigidity.CornulierUltralimit.EquivariantMarkedHilbertKernelRealization {G I : Type u} [Group G] (ρ : G →* Equiv.Perm I) (K : Matrix (I × I) (I × I) ℂ) :

Type (u + 1)

Cross-module support for the infinite Connes-rigidity construction.

realization : HilbertKernelRealization K
The underlying Hilbert-kernel realization.
representation : G →* self.realization.carrier ≃ₗᵢ[ℂ ] self.realization.carrier
The group representation on the realization.
equivariant (g : G) (i j : I) : (self.representation g) (self.realization.vector (i, j)) = self.realization.vector ((ρ g) i, (ρ g) j)

Instances For

theorem ConnesRigidity.CornulierUltralimit.tendsto_norm_finsupp_sum_of_gram {N : Type u_1} {I : Type u_2} {H : Type u_3} {V : N → Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [(n : N) → NormedAddCommGroup (V n)] [(n : N) → InnerProductSpace ℂ (V n)] (l : Filter N) (v : (n : N) → I → V n) (w : I → H) (hgram : ∀ (i j : I), Filter.Tendsto (fun (n : N) => inner ℂ (v n i) (v n j)) l (nhds (inner ℂ (w i) (w j)))) (c : I →₀ ℂ) :

Filter.Tendsto (fun (n : N) => ‖c.sum fun (i : I) (a : ℂ) => a • v n i‖) l (nhds ‖c.sum fun (i : I) (a : ℂ) => a • w i‖)

Cross-module support for the infinite Connes-rigidity construction.

def ConnesRigidity.CornulierUltralimit.markedPairCocycle {G I : Type u} [Group G] {ρ : G →* Equiv.Perm I} {K : Matrix (I × I) (I × I) ℂ} (R : EquivariantMarkedHilbertKernelRealization ρ K) (i₀ : I) (g : G) :

R.realization.carrier

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.CornulierUltralimit.markedPairCocycle R i₀ g = R.realization.vector ((ρ g) i₀, i₀)

Instances For

theorem ConnesRigidity.CornulierUltralimit.markedPairCocycle_mul {G I : Type u} [Group G] {ρ : G →* Equiv.Perm I} (K : Matrix (I × I) (I × I) ℂ) (R : EquivariantMarkedHilbertKernelRealization ρ K) (hadd : ∀ (i j k : I) (q : I × I), K (i, j) q + K (j, k) q = K (i, k) q) (i₀ : I) (g h : G) :

markedPairCocycle R i₀ (g * h) = markedPairCocycle R i₀ g + (R.representation g) (markedPairCocycle R i₀ h)

Cross-module support for the infinite Connes-rigidity construction.

noncomputable def ConnesRigidity.CornulierUltralimit.markedPairAffineAction {G I : Type u} [Group G] {ρ : G →* Equiv.Perm I} (K : Matrix (I × I) (I × I) ℂ) (R : EquivariantMarkedHilbertKernelRealization ρ K) (hadd : ∀ (i j k : I) (q : I × I), K (i, j) q + K (j, k) q = K (i, k) q) (i₀ : I) :

G →* R.realization.carrier ≃ᵃⁱ[ℂ ] R.realization.carrier

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

def ConnesRigidity.CornulierUltralimit.markedPairPoint {G I : Type u} [Group G] {ρ : G →* Equiv.Perm I} {K : Matrix (I × I) (I × I) ℂ} (R : EquivariantMarkedHilbertKernelRealization ρ K) (i₀ i : I) :

R.realization.carrier

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.CornulierUltralimit.markedPairPoint R i₀ i = R.realization.vector (i, i₀)

Instances For

def ConnesRigidity.CornulierUltralimit.AffineUniformGeneratorDisplacement {G H : Type u} [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (α : G →* H ≃ᵃⁱ[ℂ ] H) (S : Finset G) :

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.CornulierUltralimit.AffineUniformGeneratorDisplacement α S = ∀ (z : H), ∃ s ∈ S, 1 ≤ ‖(α s) z - z‖

Instances For

theorem ConnesRigidity.CornulierUltralimit.AffineUniformGeneratorDisplacement.no_global_fixed {G H : Type u} [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] {α : G →* H ≃ᵃⁱ[ℂ ] H} {S : Finset G} (h : AffineUniformGeneratorDisplacement α S) :

¬∃ (z : H), ∀ (g : G), (α g) z = z

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.CornulierUltralimit.ultrafilter_eventually_exists_finset {N : Type u_1} {G : Type u_2} (U : Ultrafilter N) (S : Finset G) (P : N → G → Prop) (h : ∀ᶠ (n : N) in ↑U, ∃ s ∈ S, P n s) :

∃ s ∈ S, ∀ᶠ (n : N) in ↑U, P n s

Cross-module support for the infinite Connes-rigidity construction.

noncomputable def ConnesRigidity.CornulierUltralimit.markedDisplacementCoefficients {G I : Type u} [Group G] (ρ : G →* Equiv.Perm I) (i₀ : I) (g : G) (c : I × I →₀ ℂ) :

I × I →₀ ℂ

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

def ConnesRigidity.CornulierUltralimit.markedOrbitAction (G : Type u) [Group G] :

G →* Equiv.Perm (G × Bool)

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.CornulierUltralimit.markedOrbitAction G = { toFun := fun (a : G) => Equiv.prodCongr (Equiv.mulLeft a) (Equiv.refl Bool), map_one' := ⋯, map_mul' := ⋯ }

Instances For

def ConnesRigidity.CornulierUltralimit.markedAffineOrbitPoint {G H : Type u} [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (α : G →* H ≃ᵃⁱ[ℂ ] H) (x y : H) (i : G × Bool) :

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.CornulierUltralimit.markedAffineOrbitPoint α x y i = (α i.1) (if i.2 = true then x else y)

Instances For

def ConnesRigidity.CornulierUltralimit.markedAffinePairDisplacement {G H : Type u} [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (α : G →* H ≃ᵃⁱ[ℂ ] H) (x y : H) (q : (G × Bool) × G × Bool) :

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

theorem ConnesRigidity.CornulierUltralimit.markedAffinePairDisplacement_finsupp_action {G H : Type u} [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (α : G →* H ≃ᵃⁱ[ℂ ] H) (x y : H) (g : G) (c : (G × Bool) × G × Bool →₀ ℂ) :

((markedDisplacementCoefficients (markedOrbitAction G) (1, false ) g c).sum fun (q : (G × Bool) × G × Bool) (a : ℂ) => a • markedAffinePairDisplacement α x y q) = (α g) (y + c.sum fun (q : (G × Bool) × G × Bool) (a : ℂ) => a • markedAffinePairDisplacement α x y q) - (y + c.sum fun (q : (G × Bool) × G × Bool) (a : ℂ) => a • markedAffinePairDisplacement α x y q)

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.CornulierUltralimit.markedPairAffineAction_finsupp_action {G I : Type u} [Group G] {ρ : G →* Equiv.Perm I} (K : Matrix (I × I) (I × I) ℂ) (R : EquivariantMarkedHilbertKernelRealization ρ K) (hadd : ∀ (i j k : I) (q : I × I), K (i, j) q + K (j, k) q = K (i, k) q) (i₀ : I) (g : G) (c : I × I →₀ ℂ) :

((markedDisplacementCoefficients ρ i₀ g c).sum fun (q : I × I) (a : ℂ) => a • R.realization.vector q) = ((markedPairAffineAction K R hadd i₀) g) (c.sum fun (q : I × I) (a : ℂ) => a • R.realization.vector q) - c.sum fun (q : I × I) (a : ℂ) => a • R.realization.vector q

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.CornulierUltralimit.affineUniformGeneratorDisplacement_of_dense {G H : Type u} [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (α : G →* H ≃ᵃⁱ[ℂ ] H) (S : Finset G) {T : Set H} (hT : Dense T) (hlower : ∀ z ∈ T, ∃ s ∈ S, 1 ≤ ‖(α s) z - z‖) :

AffineUniformGeneratorDisplacement α S

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.CornulierUltralimit.exists_marked_affine_ultralimit {G : Type u} [Group G] {H : ℕ → Type u} [(n : ℕ) → NormedAddCommGroup (H n)] [(n : ℕ) → InnerProductSpace ℂ (H n)] (α : (n : ℕ) → G →* H n ≃ᵃⁱ[ℂ ] H n) (x y : (n : ℕ) → H n) (K₁ K₂ : Subgroup G) (hx : ∀ (n : ℕ), IsAffineFixed (α n) K₁ (x n)) (hy : ∀ (n : ℕ), IsAffineFixed (α n) K₂ (y n)) (B : (G × Bool) × G × Bool → ℝ) (hbound : ∀ (n : ℕ) (q : (G × Bool) × G × Bool), ‖markedAffinePairDisplacement (α n) (x n) (y n) q‖ ≤ B q) (d : ℝ) (hdist : Filter.Tendsto (fun (n : ℕ) => ‖x n - y n‖) Filter.atTop (nhds d)) :

∃ (L : Matrix ((G × Bool) × G × Bool) ((G × Bool) × G × Bool) ℂ) (R : EquivariantMarkedHilbertKernelRealization (markedOrbitAction G) L) (hadd : ∀ (i j k : G × Bool) (q : (G × Bool) × G × Bool), L (i, j) q + L (j, k) q = L (i, k) q), L.PosSemidef ∧ Dense ↑(Submodule.span ℂ (Set.range R.realization.vector)) ∧ (∀ (a : G) (i j k l : G × Bool), L (((markedOrbitAction G) a) i, ((markedOrbitAction G) a) j) (((markedOrbitAction G) a) k, ((markedOrbitAction G) a) l) = L (i, j) (k, l)) ∧ IsAffineFixed (markedPairAffineAction L R hadd (1, false )) K₁ (markedPairPoint R (1, false ) (1, true )) ∧ IsAffineFixed (markedPairAffineAction L R hadd (1, false )) K₂ (markedPairPoint R (1, false ) (1, false )) ∧ ‖markedPairPoint R (1, false ) (1, true ) - markedPairPoint R (1, false ) (1, false )‖ = d ∧ ∀ (q r : (G × Bool) × G × Bool), Filter.Tendsto (fun (n : ℕ) => inner ℂ (markedAffinePairDisplacement (α n) (x n) (y n) q) (markedAffinePairDisplacement (α n) (x n) (y n) r)) (↑(Filter.hyperfilter ℕ)) (nhds (inner ℂ (R.realization.vector q) (R.realization.vector r)))

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.CornulierUltralimit.exists_marked_affine_ultralimit_normalized {G : Type u} [Group G] {H : ℕ → Type u} [(n : ℕ) → NormedAddCommGroup (H n)] [(n : ℕ) → InnerProductSpace ℂ (H n)] (α : (n : ℕ) → G →* H n ≃ᵃⁱ[ℂ ] H n) (x y : (n : ℕ) → H n) (K₁ K₂ : Subgroup G) (hx : ∀ (n : ℕ), IsAffineFixed (α n) K₁ (x n)) (hy : ∀ (n : ℕ), IsAffineFixed (α n) K₂ (y n)) (B : (G × Bool) × G × Bool → ℝ) (hbound : ∀ (n : ℕ) (q : (G × Bool) × G × Bool), ‖markedAffinePairDisplacement (α n) (x n) (y n) q‖ ≤ B q) (d : ℝ) (hdist : Filter.Tendsto (fun (n : ℕ) => ‖x n - y n‖) Filter.atTop (nhds d)) (S : Finset G) (hnormalized : ∀ (n : ℕ), AffineUniformGeneratorDisplacement (α n) S) :

∃ (L : Matrix ((G × Bool) × G × Bool) ((G × Bool) × G × Bool) ℂ) (R : EquivariantMarkedHilbertKernelRealization (markedOrbitAction G) L) (hadd : ∀ (i j k : G × Bool) (q : (G × Bool) × G × Bool), L (i, j) q + L (j, k) q = L (i, k) q), L.PosSemidef ∧ Dense ↑(Submodule.span ℂ (Set.range R.realization.vector)) ∧ (∀ (a : G) (i j k l : G × Bool), L (((markedOrbitAction G) a) i, ((markedOrbitAction G) a) j) (((markedOrbitAction G) a) k, ((markedOrbitAction G) a) l) = L (i, j) (k, l)) ∧ IsAffineFixed (markedPairAffineAction L R hadd (1, false )) K₁ (markedPairPoint R (1, false ) (1, true )) ∧ IsAffineFixed (markedPairAffineAction L R hadd (1, false )) K₂ (markedPairPoint R (1, false ) (1, false )) ∧ ‖markedPairPoint R (1, false ) (1, true ) - markedPairPoint R (1, false ) (1, false )‖ = d ∧ AffineUniformGeneratorDisplacement (markedPairAffineAction L R hadd (1, false )) S ∧ ∀ (q r : (G × Bool) × G × Bool), Filter.Tendsto (fun (n : ℕ) => inner ℂ (markedAffinePairDisplacement (α n) (x n) (y n) q) (markedAffinePairDisplacement (α n) (x n) (y n) r)) (↑(Filter.hyperfilter ℕ)) (nhds (inner ℂ (R.realization.vector q) (R.realization.vector r)))

Cross-module support for the infinite Connes-rigidity construction.

def ConnesRigidity.normalFixedSubmodule {G H : Type u} [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : Subgroup G) (π : UnitaryRepresentation G H) :

Submodule ℂ H

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

instance ConnesRigidity.normalFixedSubmodule_completeSpace {G H : Type u} [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : Subgroup G) (π : UnitaryRepresentation G H) :

CompleteSpace ↥(normalFixedSubmodule N π)

Cross-module support for the infinite Connes-rigidity construction.

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

↑(π g) x ∈ (normalFixedSubmodule N π)ᗮ

Cross-module support for the infinite Connes-rigidity construction.

def ConnesRigidity.normalFixedOrthogonalLinearIsometryEquiv {G H : Type u} [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : Subgroup G) [N.Normal] (π : UnitaryRepresentation G H) (g : G) :

↥(normalFixedSubmodule N π)ᗮ ≃ₗᵢ[ℂ ] ↥(normalFixedSubmodule N π)ᗮ

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

noncomputable def ConnesRigidity.normalFixedOrthogonalRepresentation {G H : Type u} [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : Subgroup G) [N.Normal] (π : UnitaryRepresentation G H) :

UnitaryRepresentation G ↥(normalFixedSubmodule N π)ᗮ

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

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

x = 0

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.normalFixed_starProjection_commute {G H : Type u} [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : Subgroup G) [N.Normal] (π : UnitaryRepresentation G H) (g : G) (x : H) :

(normalFixedSubmodule N π).starProjection (↑(π g) x) = ↑(π g) ((normalFixedSubmodule N π).starProjection x)

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.normalFixed_orthogonalResidual_displacement_le {G H : Type u} [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : Subgroup G) [N.Normal] (π : UnitaryRepresentation G H) (g : G) (x : H) :

‖↑(π g) (x - (normalFixedSubmodule N π).starProjection x) - (x - (normalFixedSubmodule N π).starProjection x)‖ ≤ ‖↑(π g) x - x‖

Cross-module support for the infinite Connes-rigidity construction.

def ConnesRigidity.HasCorelativeAffineOrbitBound {G : Type u} [Group G] (H : Subgroup G) :

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

theorem ConnesRigidity.cornulier_normalized_minimizing_action_false {G V : Type u} [Group G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (H K₁ K₂ : Subgroup G) (S : Finset G) (hgen : K₁ ⊔ K₂ = ⊤) (hH₁ : H ≤ Subgroup.normalizer ↑K₁) (hH₂ : H ≤ Subgroup.normalizer ↑K₂) (hcorel : HasCorelativeAffineOrbitBound H) (α : AffineHilbertAction G V) (hnormal : CornulierUltralimit.AffineUniformGeneratorDisplacement α S) (x₁ x₂ : V) (hmin : IsMinimizingAffinePair α K₁ K₂ x₁ x₂) (hno : ∀ (x : V), (affineLinearRepresentation α).IsInvariant x → x = 0) :

False

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.affineInvariantProjection_zero_of_no_real_characters {G V : Type u} [Group G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (hreal : ∀ (φ : G →* Multiplicative ℝ) (g : G), Multiplicative.toAdd (φ g) = 0) (α : AffineHilbertAction G V) (g : G) :

(normalFixedSubmodule ⊤ (affineLinearRepresentation α)).starProjection ((α g) 0) = 0

Cross-module support for the infinite Connes-rigidity construction.

noncomputable def ConnesRigidity.affineOrthogonalComplement {G V : Type u} [Group G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (α : AffineHilbertAction G V) :

Submodule ℂ V

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.affineOrthogonalComplement α = (ConnesRigidity.normalFixedSubmodule ⊤ (ConnesRigidity.affineLinearRepresentation α))ᗮ

Instances For

instance ConnesRigidity.affineOrthogonalComplement_completeSpace {G V : Type u} [Group G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (α : AffineHilbertAction G V) :

CompleteSpace ↥(affineOrthogonalComplement α)

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.affineTranslation_mem_orthogonal_of_no_real_characters {G V : Type u} [Group G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (hreal : ∀ (φ : G →* Multiplicative ℝ) (g : G), Multiplicative.toAdd (φ g) = 0) (α : AffineHilbertAction G V) (g : G) :

(α g) 0 ∈ affineOrthogonalComplement α

Cross-module support for the infinite Connes-rigidity construction.

def ConnesRigidity.affineOrthogonalTranslation {G V : Type u} [Group G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (hreal : ∀ (φ : G →* Multiplicative ℝ) (g : G), Multiplicative.toAdd (φ g) = 0) (α : AffineHilbertAction G V) (g : G) :

↥(affineOrthogonalComplement α)

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.affineOrthogonalTranslation hreal α g = ⟨(α g) 0, ⋯⟩

Instances For

noncomputable def ConnesRigidity.affineOrthogonalLinearHom {G V : Type u} [Group G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (α : AffineHilbertAction G V) :

G →* ↥(affineOrthogonalComplement α) ≃ₗᵢ[ℂ ] ↥(affineOrthogonalComplement α)

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

theorem ConnesRigidity.affineOrthogonalTranslation_mul {G V : Type u} [Group G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (hreal : ∀ (φ : G →* Multiplicative ℝ) (g : G), Multiplicative.toAdd (φ g) = 0) (α : AffineHilbertAction G V) (g h : G) :

affineOrthogonalTranslation hreal α (g * h) = affineOrthogonalTranslation hreal α g + ((affineOrthogonalLinearHom α) g) (affineOrthogonalTranslation hreal α h)

Cross-module support for the infinite Connes-rigidity construction.

noncomputable def ConnesRigidity.affineOrthogonalAction {G V : Type u} [Group G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (hreal : ∀ (φ : G →* Multiplicative ℝ) (g : G), Multiplicative.toAdd (φ g) = 0) (α : AffineHilbertAction G V) :

AffineHilbertAction G ↥(affineOrthogonalComplement α)

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

@[simp]

theorem ConnesRigidity.affineOrthogonalAction_apply_coe {G V : Type u} [Group G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (hreal : ∀ (φ : G →* Multiplicative ℝ) (g : G), Multiplicative.toAdd (φ g) = 0) (α : AffineHilbertAction G V) (g : G) (x : ↥(affineOrthogonalComplement α)) :

↑(((affineOrthogonalAction hreal α) g) x) = (α g) ↑x

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.affineOrthogonalAction_no_linear_invariants {G V : Type u} [Group G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (hreal : ∀ (φ : G →* Multiplicative ℝ) (g : G), Multiplicative.toAdd (φ g) = 0) (α : AffineHilbertAction G V) (x : ↥(affineOrthogonalComplement α)) (hx : (affineLinearRepresentation (affineOrthogonalAction hreal α)).IsInvariant x) :

x = 0

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.affineDiagonal_nonzero_invariant_of_fixed {G V : Type u} [Group G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G V) (v : ℕ → V) (hv : ∀ (n : ℕ), ‖v n‖ = 1) (α : AffineHilbertAction G ↥(lp (fun (x : ℕ) => V) 2)) (hα : ∀ (g : G) (x : ↥(lp (fun (x : ℕ) => V) 2)) (n : ℕ), ↑((α g) x) n = ↑(π g) (↑x n + v n) - v n) (x : ↥(lp (fun (x : ℕ) => V) 2)) (hx : ∀ (g : G), (α g) x = x) :

∃ (ξ : V), ξ ≠ 0 ∧ π.IsInvariant ξ

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.diagonalDisplacement_memℓp_of_summable {G V : Type u} [Group G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G V) (v : ℕ → V) (g : G) (hsum : Summable fun (n : ℕ) => ‖↑(π g) (v n) - v n‖ ^ 2) :

Memℓp (fun (n : ℕ) => ↑(π g) (v n) - v n) 2

Cross-module support for the infinite Connes-rigidity construction.

def ConnesRigidity.diagonalDisplacement {G V : Type u} [Group G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G V) (v : ℕ → V) (hsum : ∀ (g : G), Summable fun (n : ℕ) => ‖↑(π g) (v n) - v n‖ ^ 2) (g : G) :

↥(lp (fun (x : ℕ) => V) 2)

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.diagonalDisplacement π v hsum g = ⟨fun (n : ℕ) => ↑(π g) (v n) - v n, ⋯⟩

Instances For

noncomputable def ConnesRigidity.diagonalLinearIsometryHom {G V : Type u} [Group G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G V) :

G →* ↥(lp (fun (x : ℕ) => V) 2) ≃ₗᵢ[ℂ ] ↥(lp (fun (x : ℕ) => V) 2)

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.diagonalLinearIsometryHom π = { toFun := fun (g : G) => ConnesRigidity.crossedFiberwiseEquiv (Unitary.linearIsometryEquiv (π g)), map_one' := ⋯, map_mul' := ⋯ }

Instances For

noncomputable def ConnesRigidity.diagonalAffineAction {G V : Type u} [Group G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G V) (v : ℕ → V) (hsum : ∀ (g : G), Summable fun (n : ℕ) => ‖↑(π g) (v n) - v n‖ ^ 2) :

AffineHilbertAction G ↥(lp (fun (x : ℕ) => V) 2)

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

@[simp]

theorem ConnesRigidity.diagonalAffineAction_apply {G V : Type u} [Group G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G V) (v : ℕ → V) (hsum : ∀ (g : G), Summable fun (n : ℕ) => ‖↑(π g) (v n) - v n‖ ^ 2) (g : G) (x : ↥(lp (fun (x : ℕ) => V) 2)) (n : ℕ) :

↑(((diagonalAffineAction π v hsum) g) x) n = ↑(π g) (↑x n + v n) - v n

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.exists_almostInvariantUnitSequence_summable {G V : Type u} [Group G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] [Countable G] (π : UnitaryRepresentation G V) (hπ : π.HasAlmostInvariantUnitVectors) :

∃ (ξ : ℕ → V), (∀ (n : ℕ), ‖ξ n‖ = 1) ∧ ∀ (g : G), Summable fun (n : ℕ) => ‖↑(π g) (ξ n) - ξ n‖ ^ 2

Cross-module support for the infinite Connes-rigidity construction.

CornulierBoundedFactorization

theorem ConnesRigidity.cornulierBoundedFactorization :

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.rankTwo_transvection_smul_single {A : Type} [CommRing A] {i j : Fin 2} (hij : i ≠ j) (a b : A) :

Matrix.SpecialLinearGroup.transvection hij a • Pi.single j b = Pi.single j b + Pi.single i (a * b)

Cross-module support for the infinite Connes-rigidity construction.

def ConnesRigidity.elementaryRankTwo (A : Type) [CommRing A] :

Subgroup (Matrix.SpecialLinearGroup (Fin 2) A)

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

def ConnesRigidity.elementaryRankTwoRoot {A : Type} [CommRing A] {i j : Fin 2} (hij : i ≠ j) (a : A) :

↥(elementaryRankTwo A)

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.elementaryRankTwoRoot hij a = ⟨Matrix.SpecialLinearGroup.transvection hij a, ⋯⟩

Instances For

def ConnesRigidity.rankTwoLinearAction (A : Type) [CommRing A] :

Matrix.SpecialLinearGroup (Fin 2) A →* MulAut (Multiplicative (Fin 2 → A))

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

def ConnesRigidity.elementaryRankTwoAction (A : Type) [CommRing A] :

↥(elementaryRankTwo A) →* MulAut (Multiplicative (Fin 2 → A))

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.elementaryRankTwoAction A = (ConnesRigidity.rankTwoLinearAction A).comp (ConnesRigidity.elementaryRankTwo A).subtype

Instances For

@[reducible, inline]

abbrev ConnesRigidity.ElementaryRankTwoSemidirect (A : Type) [CommRing A] :

Type

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.ElementaryRankTwoSemidirect A = (Multiplicative (Fin 2 → A) ⋊[ConnesRigidity.elementaryRankTwoAction A] ↥(ConnesRigidity.elementaryRankTwo A))

Instances For

def ConnesRigidity.elementaryRankTwoTranslationSubgroup (A : Type) [CommRing A] :

Subgroup (ElementaryRankTwoSemidirect A)

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.elementaryRankTwoTranslationSubgroup A = SemidirectProduct.inl.range

Instances For

instance ConnesRigidity.elementaryRankTwoMatrix_countable {A : Type} [CommRing A] [Countable A] :

Countable (Matrix.SpecialLinearGroup (Fin 2) A)

Cross-module support for the infinite Connes-rigidity construction.

instance ConnesRigidity.elementaryRankTwo_countable {A : Type} [CommRing A] [Countable A] :

Countable ↥(elementaryRankTwo A)

Cross-module support for the infinite Connes-rigidity construction.

instance ConnesRigidity.elementaryRankTwoMultiplicative_countable {A : Type} [Countable A] :

Countable (Multiplicative (Fin 2 → A))

Cross-module support for the infinite Connes-rigidity construction.

instance ConnesRigidity.elementaryRankTwoSemidirect_countable {A : Type} [CommRing A] [Countable A] :

Countable (ElementaryRankTwoSemidirect A)

Cross-module support for the infinite Connes-rigidity construction.

noncomputable def ConnesRigidity.integralElementaryRankTwoGroup :

CountableDiscreteGroup

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

Subgroup integralElementaryRankTwoGroup.Carrier

@[reducible, inline]

noncomputable abbrev ConnesRigidity.integralElementaryRankTwoTranslationSubgroup :

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.integralElementaryRankTwoTranslationSubgroup = ConnesRigidity.elementaryRankTwoTranslationSubgroup ConnesRigidity.IntegralPolynomial

Instances For

noncomputable def ConnesRigidity.integralElementaryRankTwoActingGroup :

CountableDiscreteGroup

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

@[reducible, inline]

noncomputable abbrev ConnesRigidity.integralElementaryRankTwoInl :

Multiplicative (Fin 2 → IntegralPolynomial) →* integralElementaryRankTwoGroup.Carrier

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.integralElementaryRankTwoInl = SemidirectProduct.inl

Instances For

integralElementaryRankTwoActingGroup.Carrier →* integralElementaryRankTwoGroup.Carrier

@[reducible, inline]

noncomputable abbrev ConnesRigidity.integralElementaryRankTwoInr :

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.integralElementaryRankTwoInr = SemidirectProduct.inr

Instances For

integralElementaryRankTwoGroup.Carrier →* integralElementaryRankTwoActingGroup.Carrier

@[reducible, inline]

noncomputable abbrev ConnesRigidity.integralElementaryRankTwoProjection :

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.integralElementaryRankTwoProjection = SemidirectProduct.rightHom

Instances For

SplitAbelianExtension (Fin 2 → IntegralPolynomial) integralElementaryRankTwoGroup integralElementaryRankTwoActingGroup

noncomputable def ConnesRigidity.integralElementaryRankTwoSplitAbelianExtension :

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

integralElementaryRankTwoTranslationSubgroup.Normal

instance ConnesRigidity.integralElementaryRankTwoTranslationSubgroup_normal :

Cross-module support for the infinite Connes-rigidity construction.

def ConnesRigidity.HasUniformRelativeKazhdanDisplacement (G : CountableDiscreteGroup) (N : Subgroup G.Carrier) :

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

def ConnesRigidity.IsRelativeKazhdanPair (G : CountableDiscreteGroup) (N : Subgroup G.Carrier) (F : Finset G.Carrier) (κ : ℝ) :

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

theorem ConnesRigidity.HasUniformRelativeKazhdanDisplacement.map {G H : CountableDiscreteGroup} {N : Subgroup G.Carrier} (h : HasUniformRelativeKazhdanDisplacement G N) (f : G.Carrier →* H.Carrier) :

HasUniformRelativeKazhdanDisplacement H (Subgroup.map f N)

Cross-module support for the infinite Connes-rigidity construction.

noncomputable def ConnesRigidity.shalomPolynomialKazhdanConstant (m : ℕ) :

ℝ

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.shalomPolynomialKazhdanConstant m = 2 / 22 ^ (m + 1)

Instances For

theorem ConnesRigidity.shalomPolynomialKazhdanConstant_pos (m : ℕ) :

0 < shalomPolynomialKazhdanConstant m

Cross-module support for the infinite Connes-rigidity construction.

@[simp]

theorem ConnesRigidity.shalomPolynomialKazhdanConstant_zero :

shalomPolynomialKazhdanConstant 0 = 1 / 11

Cross-module support for the infinite Connes-rigidity construction.

@[simp]

theorem ConnesRigidity.shalomPolynomialKazhdanConstant_one :

shalomPolynomialKazhdanConstant 1 = 1 / 242

Cross-module support for the infinite Connes-rigidity construction.

integralElementaryRankTwoGroup.Carrier

noncomputable def ConnesRigidity.shalomPolynomialTranslation (i : Fin 2) (a : IntegralPolynomial) :

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.shalomPolynomialTranslation i a = ConnesRigidity.integralElementaryRankTwoInl (Multiplicative.ofAdd (Pi.single i a))

Instances For

integralElementaryRankTwoGroup.Carrier

noncomputable def ConnesRigidity.shalomPolynomialUpperShear (a : IntegralPolynomial) :

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.shalomPolynomialUpperShear a = ConnesRigidity.integralElementaryRankTwoInr (ConnesRigidity.elementaryRankTwoRoot ConnesRigidity.shalomPolynomialUpperShear._proof_3 a)

Instances For

integralElementaryRankTwoGroup.Carrier

noncomputable def ConnesRigidity.shalomPolynomialLowerShear (a : IntegralPolynomial) :

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.shalomPolynomialLowerShear a = ConnesRigidity.integralElementaryRankTwoInr (ConnesRigidity.elementaryRankTwoRoot ConnesRigidity.shalomPolynomialLowerShear._proof_2 a)

Instances For

Finset integralElementaryRankTwoGroup.Carrier

noncomputable def ConnesRigidity.shalomPolynomialTranslationGenerators :

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

Finset integralElementaryRankTwoGroup.Carrier

noncomputable def ConnesRigidity.shalomPolynomialShearGenerators :

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

Finset integralElementaryRankTwoGroup.Carrier

noncomputable def ConnesRigidity.shalomPolynomialKazhdanGenerators :

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.shalomPolynomialKazhdanGenerators = ConnesRigidity.shalomPolynomialTranslationGenerators ∪ ConnesRigidity.shalomPolynomialShearGenerators

Instances For

def ConnesRigidity.ShalomIntegralPolynomialRelativePair :

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

HasUniformRelativeKazhdanDisplacement integralElementaryRankTwoGroup integralElementaryRankTwoTranslationSubgroup

theorem ConnesRigidity.shalom_uniformPolynomialTranslationDisplacement (h : ShalomIntegralPolynomialRelativePair) :

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.cornulierRelativeAffineFixed_of_uniform (G : CountableDiscreteGroup) (N : Subgroup G.Carrier) (huniform : HasUniformRelativeKazhdanDisplacement G N) (V : Type u) (x✝ : NormedAddCommGroup V) (x✝¹ : InnerProductSpace ℂ V) :

CompleteSpace V → ∀ (α : AffineHilbertAction G.Carrier V), ∃ (y : V), IsAffineFixed α N y

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.HasUniformRelativeKazhdanDisplacement.sup_of_elementwise_commute {G : CountableDiscreteGroup} {N₁ N₂ : Subgroup G.Carrier} (h₁ : HasUniformRelativeKazhdanDisplacement G N₁) (h₂ : HasUniformRelativeKazhdanDisplacement G N₂) (hcomm : ∀ g ∈ N₁, ∀ h ∈ N₂, Commute g h) :

HasUniformRelativeKazhdanDisplacement G (N₁ ⊔ N₂)

Cross-module support for the infinite Connes-rigidity construction.

HasUniformRelativeKazhdanDisplacement G M

theorem ConnesRigidity.HasUniformRelativeKazhdanDisplacement.mono {G : CountableDiscreteGroup} {N M : Subgroup G.Carrier} (hN : HasUniformRelativeKazhdanDisplacement G N) (hMN : M ≤ N) :

def ConnesRigidity.rankTwoColumnBlock {A : Type} [CommRing A] (v : Fin 2 → A) :

Matrix (Fin 2) (Fin 2) A

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.rankTwoColumnBlock v i j = if j = 1 then v i else 0

Instances For

def ConnesRigidity.rankTwoParabolicMatrix {A : Type} [CommRing A] (x : ElementaryRankTwoSemidirect A) :

Matrix (Fin 4) (Fin 4) A

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.rankTwoParabolicMatrix x = (Matrix.reindex finSumFinEquiv finSumFinEquiv) (Matrix.fromBlocks (↑↑x.right) (ConnesRigidity.rankTwoColumnBlock (Multiplicative.toAdd x.left)) 0 1)

Instances For

theorem ConnesRigidity.rankTwoParabolicMatrix_det {A : Type} [CommRing A] (x : ElementaryRankTwoSemidirect A) :

(rankTwoParabolicMatrix x).det = 1

Cross-module support for the infinite Connes-rigidity construction.

def ConnesRigidity.rankTwoParabolicSpecialLinear {A : Type} [CommRing A] :

ElementaryRankTwoSemidirect A →* Matrix.SpecialLinearGroup (Fin 4) A

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.rankTwoParabolicSpecialLinear = { toFun := fun (x : ConnesRigidity.ElementaryRankTwoSemidirect A) => ⟨ConnesRigidity.rankTwoParabolicMatrix x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

Instances For

rankTwoParabolicSpecialLinear x ∈ integralElementarySubgroup

theorem ConnesRigidity.rankTwoParabolicSpecialLinear_mem_integral (x : ElementaryRankTwoSemidirect IntegralPolynomial) :

Cross-module support for the infinite Connes-rigidity construction.

integralElementaryRankTwoGroup.Carrier →* integralElementaryGroup.Carrier

noncomputable def ConnesRigidity.integralRankTwoColumnEmbedding :

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

def ConnesRigidity.specialLinearReindexHom {A : Type} [CommRing A] (e : Equiv.Perm (Fin 4)) :

Matrix.SpecialLinearGroup (Fin 4) A →* Matrix.SpecialLinearGroup (Fin 4) A

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.specialLinearReindexHom e = { toFun := fun (g : Matrix.SpecialLinearGroup (Fin 4) A) => ⟨(Matrix.reindex e e) ↑g, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

Instances For

Subgroup.map (specialLinearReindexHom e) integralElementarySubgroup ≤ integralElementarySubgroup

theorem ConnesRigidity.specialLinearReindexHom_mem_integral (e : Equiv.Perm Index) :

Cross-module support for the infinite Connes-rigidity construction.

integralElementaryGroup.Carrier →* integralElementaryGroup.Carrier

noncomputable def ConnesRigidity.integralElementaryReindexHom (e : Equiv.Perm Index) :

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

def ConnesRigidity.specialLinearTransposeInverseHom {A : Type} [CommRing A] :

Matrix.SpecialLinearGroup (Fin 4) A →* Matrix.SpecialLinearGroup (Fin 4) A

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.specialLinearTransposeInverseHom = { toFun := fun (g : Matrix.SpecialLinearGroup (Fin 4) A) => g⁻¹.transpose, map_one' := ⋯, map_mul' := ⋯ }

Instances For

Subgroup.map specialLinearTransposeInverseHom integralElementarySubgroup ≤ integralElementarySubgroup

theorem ConnesRigidity.specialLinearTransposeInverseHom_mem_integral :

Cross-module support for the infinite Connes-rigidity construction.

integralElementaryGroup.Carrier →* integralElementaryGroup.Carrier

noncomputable def ConnesRigidity.integralElementaryTransposeInverseHom :

Cross-module support for the infinite Connes-rigidity construction.

Equations

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

Instances For

integralElementaryRankTwoGroup.Carrier →* integralElementaryGroup.Carrier

noncomputable def ConnesRigidity.integralRankTwoColumnEmbedding12 :

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.integralRankTwoColumnEmbedding12 = (ConnesRigidity.integralElementaryReindexHom (Equiv.swap 0 2)).comp ConnesRigidity.integralRankTwoColumnEmbedding

Instances For

integralElementaryRankTwoGroup.Carrier →* integralElementaryGroup.Carrier

noncomputable def ConnesRigidity.integralRankTwoRowEmbedding01 :

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.integralRankTwoRowEmbedding01 = ConnesRigidity.integralElementaryTransposeInverseHom.comp ConnesRigidity.integralRankTwoColumnEmbedding

Instances For

integralElementaryRankTwoGroup.Carrier →* integralElementaryGroup.Carrier

noncomputable def ConnesRigidity.integralRankTwoRowEmbedding12 :

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.integralRankTwoRowEmbedding12 = ConnesRigidity.integralElementaryTransposeInverseHom.comp ConnesRigidity.integralRankTwoColumnEmbedding12

Instances For

noncomputable def ConnesRigidity.cornulierColumnPlane01 :

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.cornulierColumnPlane01 = Subgroup.map ConnesRigidity.integralRankTwoColumnEmbedding ConnesRigidity.integralElementaryRankTwoTranslationSubgroup

Instances For

noncomputable def ConnesRigidity.cornulierColumnPlane12 :

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.cornulierColumnPlane12 = Subgroup.map ConnesRigidity.integralRankTwoColumnEmbedding12 ConnesRigidity.integralElementaryRankTwoTranslationSubgroup

Instances For

noncomputable def ConnesRigidity.cornulierRowPlane01 :

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.cornulierRowPlane01 = Subgroup.map ConnesRigidity.integralRankTwoRowEmbedding01 ConnesRigidity.integralElementaryRankTwoTranslationSubgroup

Instances For

noncomputable def ConnesRigidity.cornulierRowPlane12 :

Cross-module support for the infinite Connes-rigidity construction.

Equations

ConnesRigidity.cornulierRowPlane12 = Subgroup.map ConnesRigidity.integralRankTwoRowEmbedding12 ConnesRigidity.integralElementaryRankTwoTranslationSubgroup

Instances For

theorem ConnesRigidity.cornulierColumnPlanes_sup_eq_K₁ :

cornulierColumnPlane01 ⊔ cornulierColumnPlane12 = cornulierK₁

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.cornulierRowPlanes_sup_eq_K₂ :

cornulierRowPlane01 ⊔ cornulierRowPlane12 = cornulierK₂

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.cornulierColumnPlanes_commute (g : integralElementaryGroup.Carrier) (hg : g ∈ cornulierColumnPlane01) (h : integralElementaryGroup.Carrier) (hh : h ∈ cornulierColumnPlane12) :

Commute g h

Cross-module support for the infinite Connes-rigidity construction.