Universal-lattice and relative-property-(T) foundations

theorem ConnesRigidity.FeedbackBooleanPolynomial.eq_one_of_ne_zero_zmod_two (a : ZMod 2) (ha : a ≠ 0) : a = 1

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

structure ConnesRigidity.CountableDiscreteGroup : Type (u + 1)

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

• Carrier : Type u

  The underlying carrier of the packaged group.

• group : Group self.Carrier
• countable : Countable self.Carrier

@[instance_reducible]

instance ConnesRigidity.CountableDiscreteGroup.instCoeSortType : CoeSort CountableDiscreteGroup (Type u)

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

Equations

• ConnesRigidity.CountableDiscreteGroup.instCoeSortType = { coe := ConnesRigidity.CountableDiscreteGroup.Carrier }

def ConnesRigidity.conjugacyClass (G : CountableDiscreteGroup) (g : G.Carrier) : Set G.Carrier

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

Equations

• ConnesRigidity.conjugacyClass G g = {h : G.Carrier | ∃ (x : G.Carrier), h = x * g * x⁻¹}

def ConnesRigidity.IsICC (G : CountableDiscreteGroup) : Prop

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

Equations

• ConnesRigidity.IsICC G = (Infinite G.Carrier ∧ ∀ (g : G.Carrier), g ≠ 1 → (ConnesRigidity.conjugacyClass G g).Infinite)

def ConnesRigidity.GroupsIsomorphic (G : CountableDiscreteGroup) (H : CountableDiscreteGroup) : Prop

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

Equations

• ConnesRigidity.GroupsIsomorphic G H = Nonempty (G.Carrier ≃* H.Carrier)

@[reducible, inline]

abbrev ConnesRigidity.UnitaryRepresentation (G : Type u) [Group G] (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : Type u

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

Equations

• ConnesRigidity.UnitaryRepresentation G H = (G →* ↥(unitary (H →L[ℂ] H)))

def ConnesRigidity.UnitaryRepresentation.IsInvariant {G H : Type u} [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : UnitaryRepresentation G H) (ξ : H) : Prop

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

Equations

• π.IsInvariant ξ = ∀ (g : G), ↑(π g) ξ = ξ

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

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

Equations

• π.HasAlmostInvariantUnitVectors = ∀ (K : Finset G) (ε : ℝ), 0 < ε → ∃ (ξ : H), ‖ξ‖ = 1 ∧ ∀ g ∈ K, ‖↑(π g) ξ - ξ‖ < ε

def ConnesRigidity.HasKazhdanPropertyT (G : CountableDiscreteGroup) : Prop

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

Equations

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

@[reducible, inline]

noncomputable abbrev ConnesRigidity.GroupL2 (G : Type u) : AddSubgroup (PreLp fun (x : G) => ℂ)

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

Equations

• ConnesRigidity.GroupL2 G = lp (fun (x : G) => ℂ) 2

def ConnesRigidity.l2Reindex {α : Type u} {β : Type v} (e : α ≃ β) : ↥(GroupL2 α) ≃ₗᵢ[ℂ] ↥(GroupL2 β)

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

Equations

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

@[simp]

theorem ConnesRigidity.l2Reindex_apply {α : Type u} {β : Type v} (e : α ≃ β) (f : ↥(GroupL2 α)) (j : β) : ↑((l2Reindex e) f) j = ↑f (e.symm j)

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

noncomputable def ConnesRigidity.leftRegularUnitary {G : Type u} [Group G] (g : G) : ↥(unitary (↥(GroupL2 G) →L[ℂ] ↥(GroupL2 G)))

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

Equations

• ConnesRigidity.leftRegularUnitary g = Unitary.linearIsometryEquiv.symm (ConnesRigidity.l2Reindex (Equiv.mulLeft g))

@[simp]

theorem ConnesRigidity.leftRegularUnitary_apply {G : Type u} [Group G] (g : G) (f : ↥(GroupL2 G)) (h : G) : ↑(↑(leftRegularUnitary g) f) h = ↑f (g⁻¹ * h)

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

noncomputable def ConnesRigidity.leftRegularRepresentation (G : Type u) [Group G] : G →* ↥(unitary (↥(GroupL2 G) →L[ℂ] ↥(GroupL2 G)))

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

Equations

• ConnesRigidity.leftRegularRepresentation G = { toFun := ConnesRigidity.leftRegularUnitary, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def ConnesRigidity.vonNeumannClosure {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : Set (H →L[ℂ] H)) : VonNeumannAlgebra H

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

Equations

• ConnesRigidity.vonNeumannClosure S = { toStarSubalgebra := StarSubalgebra.centralizer ℂ ↑(StarSubalgebra.centralizer ℂ S), centralizer_centralizer' := ⋯ }

noncomputable def ConnesRigidity.groupVonNeumannAlgebra (G : CountableDiscreteGroup) : VonNeumannAlgebra ↥(GroupL2 G.Carrier)

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

Equations

• ConnesRigidity.groupVonNeumannAlgebra G = ConnesRigidity.vonNeumannClosure (Set.range fun (g : G.Carrier) => ↑((ConnesRigidity.leftRegularRepresentation G.Carrier) g))

@[reducible, inline]

noncomputable abbrev ConnesRigidity.GroupVonNeumannAlgebra (G : CountableDiscreteGroup) : StarSubalgebra ℂ (↥(GroupL2 G.Carrier) →L[ℂ] ↥(GroupL2 G.Carrier))

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

Equations

• ConnesRigidity.GroupVonNeumannAlgebra G = (ConnesRigidity.groupVonNeumannAlgebra G).toStarSubalgebra

noncomputable def ConnesRigidity.delta (G : CountableDiscreteGroup) (g : G.Carrier) : ↥(GroupL2 G.Carrier)

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

Equations

• ConnesRigidity.delta G g = lp.single 2 g 1

noncomputable def ConnesRigidity.canonicalTrace (G : CountableDiscreteGroup) : ↥(GroupVonNeumannAlgebra G) → ℂ

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

Equations

• ConnesRigidity.canonicalTrace G x = inner ℂ (ConnesRigidity.delta G 1) (↑x (ConnesRigidity.delta G 1))

def ConnesRigidity.ProjectionLE {A : Type u} [Mul A] (p q : A) : Prop

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

Equations

• ConnesRigidity.ProjectionLE p q = (p * q = p)

def ConnesRigidity.IsProjectionSupremum {A : Type u} [Mul A] [Star A] (S : Set A) (p : A) : Prop

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

Equations

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

def ConnesRigidity.IsNormalStarAlgEquiv {A : Type u} {B : Type v} [Semiring A] [StarRing A] [Algebra ℂ A] [Semiring B] [StarRing B] [Algebra ℂ B] (e : A ≃⋆ₐ[ℂ] B) : Prop

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

Equations

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

structure ConnesRigidity.TracialGroupFactorEquiv (G : CountableDiscreteGroup) (H : CountableDiscreteGroup) : Type (max u v)

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

• toStarAlgEquiv : ↥(GroupVonNeumannAlgebra G) ≃⋆ₐ[ℂ] ↥(GroupVonNeumannAlgebra H)

  The star-algebra equivalence between the two group factors.

• normal : IsNormalStarAlgEquiv self.toStarAlgEquiv
• trace_preserving (x : ↥(GroupVonNeumannAlgebra G)) : canonicalTrace H (self.toStarAlgEquiv x) = canonicalTrace G x

def ConnesRigidity.TracialGroupFactorsIsomorphic (G : CountableDiscreteGroup) (H : CountableDiscreteGroup) : Prop

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

Equations

• ConnesRigidity.TracialGroupFactorsIsomorphic G H = Nonempty (ConnesRigidity.TracialGroupFactorEquiv G H)

theorem ConnesRigidity.UnitaryRepresentation.hasAlmostInvariantUnitVectors_comp {G H K : Type u} [Group G] [Group H] [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (π : UnitaryRepresentation H K) (f : G →* H) (hπ : π.HasAlmostInvariantUnitVectors) : HasAlmostInvariantUnitVectors (MonoidHom.comp π f)

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

def ConnesRigidity.CountableDiscreteGroup.subgroup (G : CountableDiscreteGroup) (S : Subgroup G.Carrier) : CountableDiscreteGroup

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

Equations

• G.subgroup S = { Carrier := ↥S, group := inferInstance, countable := ⋯ }

@[instance_reducible]

noncomputable def ConnesRigidity.FiniteIndex.finiteIndexQuotientFintype {G : Type u} [Group G] (S : Subgroup G) [S.FiniteIndex] : Fintype (G ⧸ S)

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

Equations

• ConnesRigidity.FiniteIndex.finiteIndexQuotientFintype S = Subgroup.fintypeQuotientOfFiniteIndex

@[reducible, inline]

abbrev ConnesRigidity.F : Type

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

Equations

• ConnesRigidity.F = ZMod 2

@[reducible, inline]

abbrev ConnesRigidity.R : Type

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

Equations

• ConnesRigidity.R = Polynomial ConnesRigidity.F

@[reducible, inline]

abbrev ConnesRigidity.V : Type

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

Equations

• ConnesRigidity.V = (Fin 4 → ConnesRigidity.R)

noncomputable def ConnesRigidity.e : V

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

Equations

• ConnesRigidity.e i = if i = 0 then 1 else 0

@[simp]

theorem ConnesRigidity.e_apply (i : Fin 4) : e i = if i = 0 then 1 else 0

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

theorem ConnesRigidity.e_ne_zero : e ≠ 0

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

@[reducible, inline]

abbrev ConnesRigidity.T : Type

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

Equations

• ConnesRigidity.T = TensorProduct ConnesRigidity.F ConnesRigidity.V ConnesRigidity.V

noncomputable def ConnesRigidity.square (v : V) : T

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

Equations

• ConnesRigidity.square v = v ⊗ₜ[ConnesRigidity.F] v

noncomputable def ConnesRigidity.B : Submodule F T

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

Equations

• ConnesRigidity.B = Submodule.span ConnesRigidity.F (Set.range ConnesRigidity.square)

@[reducible, inline]

abbrev ConnesRigidity.D : Type

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

Equations

• ConnesRigidity.D = (ConnesRigidity.V × ↥ConnesRigidity.B)

theorem ConnesRigidity.square_mem (v : V) : square v ∈ B

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

noncomputable def ConnesRigidity.diagonal (v : V) : ↥B

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

Equations

• ConnesRigidity.diagonal v = ⟨ConnesRigidity.square v, ⋯⟩

@[simp]

theorem ConnesRigidity.diagonal_val (v : V) : ↑(diagonal v) = square v

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

theorem ConnesRigidity.symmetric_tmul_mem (u v : V) : u ⊗ₜ[F] v + v ⊗ₜ[F] u ∈ B

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

noncomputable def ConnesRigidity.polarization (u v : V) : ↥B

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

Equations

• ConnesRigidity.polarization u v = ⟨u ⊗ₜ[ConnesRigidity.F] v + v ⊗ₜ[ConnesRigidity.F] u, ⋯⟩

theorem ConnesRigidity.diagonal_add (u v : V) : diagonal (u + v) = diagonal u + diagonal v + polarization u v

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

theorem ConnesRigidity.add_self_eq_zero {M : Type u_1} [AddCommGroup M] [Module F M] (x : M) : x + x = 0

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

theorem ConnesRigidity.D_add_self (d : D) : d + d = 0

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

@[reducible, inline]

abbrev ConnesRigidity.TruncatedPolynomial (n : ℕ) : Type

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

Equations

• ConnesRigidity.TruncatedPolynomial n = AdjoinRoot (Polynomial.X ^ n)

@[reducible, inline]

abbrev ConnesRigidity.TruncatedVector (n : ℕ) : Type

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

Equations

• ConnesRigidity.TruncatedVector n = (Fin 4 → ConnesRigidity.TruncatedPolynomial n)

noncomputable def ConnesRigidity.truncatedPolynomialEquiv (n : ℕ) : TruncatedPolynomial n ≃ₗ[F] Fin n → F

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

Equations

• ConnesRigidity.truncatedPolynomialEquiv n = ⋯.mp (AdjoinRoot.powerBasisAux' ⋯).equivFun

noncomputable def ConnesRigidity.truncatedVectorEquiv (n : ℕ) : TruncatedVector n ≃ₗ[F] Fin 4 → Fin n → F

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

Equations

• ConnesRigidity.truncatedVectorEquiv n = LinearEquiv.piCongrRight fun (x : Fin 4) => ConnesRigidity.truncatedPolynomialEquiv n

noncomputable def ConnesRigidity.truncatePolynomial (n : ℕ) : R →ₗ[F] TruncatedPolynomial n

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

Equations

• ConnesRigidity.truncatePolynomial n = (AdjoinRoot.mkₐ (Polynomial.X ^ n)).toLinearMap

noncomputable def ConnesRigidity.truncateVector (n : ℕ) : V →ₗ[F] TruncatedVector n

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

Equations

• ConnesRigidity.truncateVector n = (ConnesRigidity.truncatePolynomial n).compLeft (Fin 4)

theorem ConnesRigidity.truncateVector_surjective (n : ℕ) : Function.Surjective ⇑(truncateVector n)

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

noncomputable def ConnesRigidity.shiftedSubmodule (n : ℕ) : Submodule F V

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

Equations

• ConnesRigidity.shiftedSubmodule n = (ConnesRigidity.truncateVector n).ker

theorem ConnesRigidity.mem_shiftedSubmodule_iff (n : ℕ) (v : V) : v ∈ shiftedSubmodule n ↔ ∀ (i : Fin 4), Polynomial.X ^ n ∣ v i

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

@[reducible, inline]

abbrev ConnesRigidity.ShiftedQuotient (n : ℕ) : Type

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

Equations

• ConnesRigidity.ShiftedQuotient n = (ConnesRigidity.V ⧸ ConnesRigidity.shiftedSubmodule n)

noncomputable def ConnesRigidity.shiftedQuotientEquiv (n : ℕ) : ShiftedQuotient n ≃ₗ[F] TruncatedVector n

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

Equations

• ConnesRigidity.shiftedQuotientEquiv n = (ConnesRigidity.truncateVector n).quotKerEquivOfSurjective ⋯

noncomputable def ConnesRigidity.shiftedQuotientCoeffEquiv (n : ℕ) : ShiftedQuotient n ≃ₗ[F] Fin 4 → Fin n → F

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

Equations

• ConnesRigidity.shiftedQuotientCoeffEquiv n = (ConnesRigidity.shiftedQuotientEquiv n).trans (ConnesRigidity.truncatedVectorEquiv n)

theorem ConnesRigidity.shiftedQuotient_card (n : ℕ) : Nat.card (ShiftedQuotient n) = 2 ^ (4 * n)

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

@[reducible, inline]

abbrev ConnesRigidity.Index : Type

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

Equations

• ConnesRigidity.Index = Fin 4

@[reducible, inline]

abbrev ConnesRigidity.IntegralPolynomial : Type

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

Equations

• ConnesRigidity.IntegralPolynomial = Polynomial ℤ

instance ConnesRigidity.instCountableIntegralPolynomial : Countable IntegralPolynomial

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

@[reducible, inline]

abbrev ConnesRigidity.BinaryPolynomial : Type

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

Equations

• ConnesRigidity.BinaryPolynomial = ConnesRigidity.R

instance ConnesRigidity.instCountableBinaryPolynomial : Countable BinaryPolynomial

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

@[reducible, inline]

abbrev ConnesRigidity.IntegralSpecialLinearGroup : Type

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

Equations

• ConnesRigidity.IntegralSpecialLinearGroup = Matrix.SpecialLinearGroup ConnesRigidity.Index ConnesRigidity.IntegralPolynomial

instance ConnesRigidity.instCountableIntegralSpecialLinearGroup : Countable IntegralSpecialLinearGroup

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

@[reducible, inline]

abbrev ConnesRigidity.TernarySpecialLinearGroup : Type

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

Equations

• ConnesRigidity.TernarySpecialLinearGroup = Matrix.SpecialLinearGroup ConnesRigidity.Index (ZMod 3)

@[reducible, inline]

abbrev ConnesRigidity.Q : Type

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

Equations

• ConnesRigidity.Q = Matrix.SpecialLinearGroup ConnesRigidity.Index ConnesRigidity.BinaryPolynomial

noncomputable def ConnesRigidity.modThreeAtZero : IntegralPolynomial →+* ZMod 3

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

Equations

• ConnesRigidity.modThreeAtZero = (Int.castRingHom (ZMod 3)).comp (Polynomial.evalRingHom 0)

noncomputable def ConnesRigidity.modThreeGroupHom : IntegralSpecialLinearGroup →* TernarySpecialLinearGroup

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

Equations

• ConnesRigidity.modThreeGroupHom = Matrix.SpecialLinearGroup.map ConnesRigidity.modThreeAtZero

@[reducible, inline]

noncomputable abbrev ConnesRigidity.K : Subgroup IntegralSpecialLinearGroup

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

Equations

• ConnesRigidity.K = ConnesRigidity.modThreeGroupHom.ker

instance ConnesRigidity.instCountableSubtypeIntegralSpecialLinearGroupMemSubgroupK : Countable ↥K

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

noncomputable def ConnesRigidity.integralGroup : CountableDiscreteGroup

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

Equations

• ConnesRigidity.integralGroup = { Carrier := ConnesRigidity.IntegralSpecialLinearGroup, group := inferInstance, countable := ConnesRigidity.integralGroup._proof_1 }

noncomputable def ConnesRigidity.actingGroup : CountableDiscreteGroup

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

Equations

• ConnesRigidity.actingGroup = { Carrier := ↥ConnesRigidity.K, group := inferInstance, countable := ConnesRigidity.actingGroup._proof_1 }

instance ConnesRigidity.instFiniteIndexIntegralSpecialLinearGroupKerTernarySpecialLinearGroupModThreeGroupHom : modThreeGroupHom.ker.FiniteIndex

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

noncomputable def ConnesRigidity.modTwoPolynomial : IntegralPolynomial →+* BinaryPolynomial

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

Equations

• ConnesRigidity.modTwoPolynomial = Polynomial.mapRingHom (Int.castRingHom (ZMod 2))

noncomputable def ConnesRigidity.modTwoGroupHom : IntegralSpecialLinearGroup →* Q

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

Equations

• ConnesRigidity.modTwoGroupHom = Matrix.SpecialLinearGroup.map ConnesRigidity.modTwoPolynomial

noncomputable def ConnesRigidity.pi₂ : ↥K →* Q

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

Equations

• ConnesRigidity.pi₂ = ConnesRigidity.modTwoGroupHom.comp ConnesRigidity.modThreeGroupHom.ker.subtype

theorem ConnesRigidity.specialLinear_map_transvection_baseChange {ι : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing A] [CommRing B] (f : A →+* B) {i j : ι} (hij : i ≠ j) (a : A) : (Matrix.SpecialLinearGroup.map f) (Matrix.SpecialLinearGroup.transvection hij a) = Matrix.SpecialLinearGroup.transvection hij (f a)

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

theorem ConnesRigidity.integralTransvection_mem_KSubgroup {i j : Index} (hij : i ≠ j) (a : IntegralPolynomial) : Matrix.SpecialLinearGroup.transvection hij (3 * a) ∈ modThreeGroupHom.ker

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

noncomputable def ConnesRigidity.liftedIntegralTransvection {i j : Index} (hij : i ≠ j) (a : IntegralPolynomial) : ↥K

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

Equations

• ConnesRigidity.liftedIntegralTransvection hij a = ⟨Matrix.SpecialLinearGroup.transvection hij (3 * a), ⋯⟩

def ConnesRigidity.elementaryTransvections : Set Q

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

Equations

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

def ConnesRigidity.ElementaryGeneration : Prop

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

Equations

• ConnesRigidity.ElementaryGeneration = (Subgroup.closure ConnesRigidity.elementaryTransvections = ⊤)

theorem ConnesRigidity.pi₂_surjective_of_elementaryGeneration (h : ElementaryGeneration) : Function.Surjective ⇑pi₂

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

@[reducible, inline]

abbrev ConnesRigidity.IntegerSpecialLinearGroup : Type

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

Equations

• ConnesRigidity.IntegerSpecialLinearGroup = Matrix.SpecialLinearGroup ConnesRigidity.Index ℤ

def ConnesRigidity.levelThreeIntegerReduction : IntegerSpecialLinearGroup →* TernarySpecialLinearGroup

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

Equations

• ConnesRigidity.levelThreeIntegerReduction = Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod 3))

def ConnesRigidity.levelThreeIntegerSubgroup : Subgroup IntegerSpecialLinearGroup

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

Equations

• ConnesRigidity.levelThreeIntegerSubgroup = ConnesRigidity.levelThreeIntegerReduction.ker

def ConnesRigidity.LevelThreeIntegerTorsionFree : Prop

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

Equations

• ConnesRigidity.LevelThreeIntegerTorsionFree = ∀ (g : ↥ConnesRigidity.levelThreeIntegerSubgroup), IsOfFinOrder g → g = 1

theorem ConnesRigidity.K_no_nontrivial_torsion_of_levelThree_torsionFree (hlevel : LevelThreeIntegerTorsionFree) (g : ↥K) : IsOfFinOrder g → g = 1

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

theorem ConnesRigidity.hasKazhdanPropertyT_finitelyGenerated (G : CountableDiscreteGroup) (hT : HasKazhdanPropertyT G) : Group.FG G.Carrier

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

def ConnesRigidity.ErshovJaikinUniversalLatticePropertyT : Prop

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

Equations

• ConnesRigidity.ErshovJaikinUniversalLatticePropertyT = ConnesRigidity.HasKazhdanPropertyT ConnesRigidity.integralGroup

theorem ConnesRigidity.actingGroup_hasKazhdanPropertyT (hUniversalLattice : ErshovJaikinUniversalLatticePropertyT) : HasKazhdanPropertyT actingGroup

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

theorem ConnesRigidity.specialLinear_transvection_commutator {ι : Type u_1} {A : Type u_2} [Fintype ι] [DecidableEq ι] [CommRing A] (i j k : ι) (hij : i ≠ j) (hjk : j ≠ k) (hik : i ≠ k) (a b : A) : Matrix.SpecialLinearGroup.transvection hij a * Matrix.SpecialLinearGroup.transvection hjk b * (Matrix.SpecialLinearGroup.transvection hij a)⁻¹ * (Matrix.SpecialLinearGroup.transvection hjk b)⁻¹ = Matrix.SpecialLinearGroup.transvection hik (a * b)

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

theorem ConnesRigidity.integral_transvection_mem_of_one_and_X (H : Subgroup IntegralSpecialLinearGroup) (hone : ∀ (i j : Index) (h : i ≠ j), Matrix.SpecialLinearGroup.transvection h 1 ∈ H) (hX : ∀ (i j : Index) (h : i ≠ j), Matrix.SpecialLinearGroup.transvection h Polynomial.X ∈ H) (i j : Index) (hij : i ≠ j) (p : IntegralPolynomial) : Matrix.SpecialLinearGroup.transvection hij p ∈ H

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

noncomputable def ConnesRigidity.integralElementarySubgroup : Subgroup IntegralSpecialLinearGroup

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

Equations

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

noncomputable def ConnesRigidity.integralElementaryGroup : CountableDiscreteGroup

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

Equations

• ConnesRigidity.integralElementaryGroup = { Carrier := ↥ConnesRigidity.integralElementarySubgroup, group := inferInstance, countable := ConnesRigidity.integralElementaryGroup._proof_1 }

def ConnesRigidity.SuslinElementaryGeneration : Prop

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

Equations

• ConnesRigidity.SuslinElementaryGeneration = (ConnesRigidity.integralElementarySubgroup = ⊤)

def ConnesRigidity.ErshovJaikinElementaryPropertyT : Prop

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

Equations

• ConnesRigidity.ErshovJaikinElementaryPropertyT = ConnesRigidity.HasKazhdanPropertyT ConnesRigidity.integralElementaryGroup

theorem ConnesRigidity.universalLatticePropertyT_of_elementary (hSuslin : SuslinElementaryGeneration) (hElementary : ErshovJaikinElementaryPropertyT) : ErshovJaikinUniversalLatticePropertyT

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

theorem ConnesRigidity.integralElementaryGroup_isPerfect : Group.IsPerfect integralElementaryGroup.Carrier

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

noncomputable def ConnesRigidity.suslinEvaluation : IntegralSpecialLinearGroup →* IntegerSpecialLinearGroup

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

Equations

• ConnesRigidity.suslinEvaluation = Matrix.SpecialLinearGroup.map (Polynomial.evalRingHom 0)

noncomputable def ConnesRigidity.suslinConstantSection : IntegerSpecialLinearGroup →* IntegralSpecialLinearGroup

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

Equations

• ConnesRigidity.suslinConstantSection = Matrix.SpecialLinearGroup.map Polynomial.C

def ConnesRigidity.integerElementarySubgroup : Subgroup IntegerSpecialLinearGroup

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

Equations

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

def ConnesRigidity.IntegerElementaryGeneration : Prop

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

Equations

• ConnesRigidity.IntegerElementaryGeneration = (ConnesRigidity.integerElementarySubgroup = ⊤)

noncomputable def ConnesRigidity.suslinAugmentationKernel : Subgroup IntegralSpecialLinearGroup

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

Equations

• ConnesRigidity.suslinAugmentationKernel = ConnesRigidity.suslinEvaluation.ker

def ConnesRigidity.SuslinRelativeElementaryGeneration : Prop

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

Equations

• ConnesRigidity.SuslinRelativeElementaryGeneration = (ConnesRigidity.suslinAugmentationKernel ≤ ConnesRigidity.integralElementarySubgroup)

theorem ConnesRigidity.suslinElementaryGeneration_iff_base_and_relative : SuslinElementaryGeneration ↔ IntegerElementaryGeneration ∧ SuslinRelativeElementaryGeneration

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

def ConnesRigidity.localGlobalElementarySubgroup (R : Type u_1) [CommRing R] : Subgroup (Matrix.SpecialLinearGroup Index R)

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

Equations

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

theorem ConnesRigidity.map_localGlobalElementarySubgroup_le {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) : Subgroup.map (Matrix.SpecialLinearGroup.map f) (localGlobalElementarySubgroup R) ≤ localGlobalElementarySubgroup S

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

noncomputable def ConnesRigidity.suslinDifferenceDilationRingHom {A : Type u} [CommRing A] (a : A) : Polynomial A →+* Polynomial A

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

Equations

• ConnesRigidity.suslinDifferenceDilationRingHom a = (Polynomial.C a * Polynomial.X).compRingHom

noncomputable def ConnesRigidity.suslinDifferenceDilation {A : Type u} [CommRing A] (a : A) : Matrix.SpecialLinearGroup Index (Polynomial A) →* Matrix.SpecialLinearGroup Index (Polynomial A)

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

Equations

• ConnesRigidity.suslinDifferenceDilation a = Matrix.SpecialLinearGroup.map (ConnesRigidity.suslinDifferenceDilationRingHom a)

noncomputable def ConnesRigidity.suslinBivariateShiftRingHom {A : Type u} [CommRing A] (a : A) : Polynomial A →+* Polynomial (Polynomial A)

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

Equations

• ConnesRigidity.suslinBivariateShiftRingHom a = Polynomial.eval₂RingHom (Polynomial.C.comp Polynomial.C) (Polynomial.C (Polynomial.C a * Polynomial.X) + Polynomial.X)

noncomputable def ConnesRigidity.suslinBivariateConstantRingHom {A : Type u} [CommRing A] : Polynomial A →+* Polynomial (Polynomial A)

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

Equations

• ConnesRigidity.suslinBivariateConstantRingHom = Polynomial.C

noncomputable def ConnesRigidity.suslinDifferencePath {A : Type u} [CommRing A] (a : A) (g : Matrix.SpecialLinearGroup Index (Polynomial A)) : Matrix.SpecialLinearGroup Index (Polynomial (Polynomial A))

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

Equations

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

theorem ConnesRigidity.suslinDifferencePath_eval_mul_X {A : Type u} [CommRing A] (a b : A) (g : Matrix.SpecialLinearGroup Index (Polynomial A)) : (Matrix.SpecialLinearGroup.map (Polynomial.evalRingHom (Polynomial.C b * Polynomial.X))) (suslinDifferencePath a g) = (suslinDifferenceDilation (a + b)) g * ((suslinDifferenceDilation a) g)⁻¹

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

theorem ConnesRigidity.suslinDifferenceDilation_baseChange {A : Type u} [CommRing A] {B : Type v} [CommRing B] (f : A →+* B) (a : A) (g : Matrix.SpecialLinearGroup Index (Polynomial A)) : (Matrix.SpecialLinearGroup.map (Polynomial.mapRingHom f)) ((suslinDifferenceDilation a) g) = (suslinDifferenceDilation (f a)) ((Matrix.SpecialLinearGroup.map (Polynomial.mapRingHom f)) g)

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

theorem ConnesRigidity.suslinDifferencePath_baseChange {A : Type u} [CommRing A] {B : Type v} [CommRing B] (f : A →+* B) (a : A) (g : Matrix.SpecialLinearGroup Index (Polynomial A)) : (Matrix.SpecialLinearGroup.map (Polynomial.mapRingHom (Polynomial.mapRingHom f))) (suslinDifferencePath a g) = suslinDifferencePath (f a) ((Matrix.SpecialLinearGroup.map (Polynomial.mapRingHom f)) g)

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

theorem ConnesRigidity.suslinDifferencePath_relative_elementary_of_baseChange {A : Type u} [CommRing A] {B : Type v} [CommRing B] (f : A →+* B) (a : A) (g : Matrix.SpecialLinearGroup Index (Polynomial A)) (hg : (Matrix.SpecialLinearGroup.map (Polynomial.mapRingHom f)) g ∈ localGlobalElementarySubgroup (Polynomial B)) : (Matrix.SpecialLinearGroup.map (Polynomial.mapRingHom (Polynomial.mapRingHom f))) (suslinDifferencePath a g) ∈ localGlobalElementarySubgroup (Polynomial (Polynomial B)) ∧ (Matrix.SpecialLinearGroup.map (Polynomial.evalRingHom 0)) ((Matrix.SpecialLinearGroup.map (Polynomial.mapRingHom (Polynomial.mapRingHom f))) (suslinDifferencePath a g)) = 1

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

def ConnesRigidity.suslinElementarySubgroup (ι : Type u) (A : Type v) [Fintype ι] [DecidableEq ι] [CommRing A] : Subgroup (Matrix.SpecialLinearGroup ι A)

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

Equations

• ConnesRigidity.suslinElementarySubgroup ι A = Subgroup.closure {g : Matrix.SpecialLinearGroup ι A | ∃ (i : ι) (j : ι) (h : i ≠ j) (a : A), g = Matrix.SpecialLinearGroup.transvection h a}

theorem ConnesRigidity.suslin_transvection_conj_noncomposable {ι : Type u_1} {A : Type u_2} [Fintype ι] [DecidableEq ι] [CommRing A] {i j k l : ι} (hij : i ≠ j) (hkl : k ≠ l) (hjk : j ≠ k) (hli : l ≠ i) (a b : A) : Matrix.SpecialLinearGroup.transvection hij a * Matrix.SpecialLinearGroup.transvection hkl b * (Matrix.SpecialLinearGroup.transvection hij a)⁻¹ = Matrix.SpecialLinearGroup.transvection hkl b

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

theorem ConnesRigidity.suslin_transvection_conj_adjacent {ι : Type u_1} {A : Type u_2} [Fintype ι] [DecidableEq ι] [CommRing A] (i j k : ι) (hij : i ≠ j) (hjk : j ≠ k) (hik : i ≠ k) (a b : A) : Matrix.SpecialLinearGroup.transvection hij a * Matrix.SpecialLinearGroup.transvection hjk b * (Matrix.SpecialLinearGroup.transvection hij a)⁻¹ = Matrix.SpecialLinearGroup.transvection hik (a * b) * Matrix.SpecialLinearGroup.transvection hjk b

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

theorem ConnesRigidity.suslin_transvection_conj_reverse_adjacent {ι : Type u_1} {A : Type u_2} [Fintype ι] [DecidableEq ι] [CommRing A] (i j k : ι) (hij : i ≠ j) (hjk : j ≠ k) (hik : i ≠ k) (a b : A) : Matrix.SpecialLinearGroup.transvection hij a * Matrix.SpecialLinearGroup.transvection ⋯ b * (Matrix.SpecialLinearGroup.transvection hij a)⁻¹ = Matrix.SpecialLinearGroup.transvection ⋯ (-(b * a)) * Matrix.SpecialLinearGroup.transvection ⋯ b

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

@[reducible, inline]

abbrev ConnesRigidity.SuslinPolynomialSL (R : Type u_1) [CommRing R] : Type u_1

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

Equations

• ConnesRigidity.SuslinPolynomialSL R = Matrix.SpecialLinearGroup ConnesRigidity.Index (Polynomial R)

noncomputable def ConnesRigidity.suslinDilation (R : Type u_1) [CommRing R] (a : R) : SuslinPolynomialSL R →* SuslinPolynomialSL R

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

Equations

• ConnesRigidity.suslinDilation R a = Matrix.SpecialLinearGroup.map (Polynomial.C a * Polynomial.X).compRingHom

noncomputable def ConnesRigidity.suslinPolynomialBaseChange {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] : SuslinPolynomialSL A →* SuslinPolynomialSL B

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

Equations

• ConnesRigidity.suslinPolynomialBaseChange = Matrix.SpecialLinearGroup.map (Polynomial.mapRingHom (algebraMap A B))

theorem ConnesRigidity.suslinPolynomialBaseChange_dilation {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] (a : A) (g : SuslinPolynomialSL A) : suslinPolynomialBaseChange ((suslinDilation A a) g) = (suslinDilation B ((algebraMap A B) a)) (suslinPolynomialBaseChange g)

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

def ConnesRigidity.suslinEventuallyElementaryLift {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] (M : Submonoid A) : Set (SuslinPolynomialSL B)

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

Equations

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

theorem ConnesRigidity.suslinEventuallyElementaryLift_one {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] (M : Submonoid A) : 1 ∈ suslinEventuallyElementaryLift M

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

theorem ConnesRigidity.suslinEventuallyElementaryLift_inv {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] (M : Submonoid A) {g : SuslinPolynomialSL B} (hg : g ∈ suslinEventuallyElementaryLift M) : g⁻¹ ∈ suslinEventuallyElementaryLift M

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

theorem ConnesRigidity.suslinEventuallyElementaryLift_mul {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] (M : Submonoid A) {g h : SuslinPolynomialSL B} (hg : g ∈ suslinEventuallyElementaryLift M) (hh : h ∈ suslinEventuallyElementaryLift M) : g * h ∈ suslinEventuallyElementaryLift M

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

def ConnesRigidity.suslinEventuallyElementarySubgroup {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] (M : Submonoid A) : Subgroup (SuslinPolynomialSL B)

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

Equations

• ConnesRigidity.suslinEventuallyElementarySubgroup M = { carrier := ConnesRigidity.suslinEventuallyElementaryLift M, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem ConnesRigidity.suslin_polynomial_relative_z_mem_eventual {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] (M : Submonoid A) [IsLocalization M B] (i j : Index) (hij : i ≠ j) (a p : Polynomial B) (hp : p.coeff 0 = 0) : Matrix.SpecialLinearGroup.transvection ⋯ a * Matrix.SpecialLinearGroup.transvection hij p * (Matrix.SpecialLinearGroup.transvection ⋯ a)⁻¹ ∈ suslinEventuallyElementarySubgroup M

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

def ConnesRigidity.UnimodularRow {A : Type u_1} [CommRing A] {n : ℕ} (v : Fin n → A) : Prop

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

Equations

• ConnesRigidity.UnimodularRow v = ∃ (c : Fin n → A), ∑ i : Fin n, c i * v i = 1

def ConnesRigidity.BassStableRangeAtMost (A : Type u_1) [CommRing A] (n : ℕ) : Prop

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

Equations

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

@[reducible, inline]

abbrev ConnesRigidity.IntegralPolynomialStableRangeThree : Prop

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

Equations

• ConnesRigidity.IntegralPolynomialStableRangeThree = ConnesRigidity.BassStableRangeAtMost ConnesRigidity.IntegralPolynomial 3

theorem ConnesRigidity.integralSpecialLinear_lastColumn_stableRange_shorten (hstable : IntegralPolynomialStableRangeThree) (g : IntegralSpecialLinearGroup) : ∃ (c : Fin 3 → IntegralPolynomial), UnimodularRow fun (i : Fin 3) => ↑g i.castSucc 3 + c i * ↑g 3 3

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

theorem ConnesRigidity.bassStableRangeThree_of_noetherian_domain_dimension_two {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] (hdim : ringKrullDim A = 2) : BassStableRangeAtMost A 3

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

theorem ConnesRigidity.integralPolynomial_stableRangeThree : IntegralPolynomialStableRangeThree

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

def ConnesRigidity.LocalElementaryProof.localElementarySubgroup (A : Type u) [CommRing A] : Subgroup (Matrix.SpecialLinearGroup (Fin 4) A)

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

Equations

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

theorem ConnesRigidity.LocalElementaryProof.transvection_mem {A : Type u} [CommRing A] (i j : Fin 4) (h : i ≠ j) (a : A) : Matrix.SpecialLinearGroup.transvection h a ∈ localElementarySubgroup A

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

theorem ConnesRigidity.LocalElementaryProof.transvection_smul_same {A : Type u} [CommRing A] (i j : Fin 4) (h : i ≠ j) (a : A) (v : Fin 4 → A) : (Matrix.SpecialLinearGroup.transvection h a • v) i = v i + a * v j

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

theorem ConnesRigidity.LocalElementaryProof.transvection_smul_other {A : Type u} [CommRing A] (i j k : Fin 4) (h : i ≠ j) (hk : k ≠ i) (a : A) (v : Fin 4 → A) : (Matrix.SpecialLinearGroup.transvection h a • v) k = v k

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

def ConnesRigidity.LocalElementaryProof.coordinateRotation {A : Type u} [CommRing A] (i j : Fin 4) (h : i ≠ j) : Matrix.SpecialLinearGroup (Fin 4) A

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

Equations

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

def ConnesRigidity.MonicMatrixElimination.lowerBlockMatrix {R : Type u} [CommRing R] (b : Matrix (Fin 3) (Fin 3) R) : Matrix (Fin 4) (Fin 4) R

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

Equations

• ConnesRigidity.MonicMatrixElimination.lowerBlockMatrix b i j = Fin.cases (Fin.cases 1 (fun (x : Fin 3) => 0) j) (fun (i' : Fin 3) => Fin.cases 0 (fun (j' : Fin 3) => b i' j') j) i

def ConnesRigidity.MonicMatrixElimination.lowerBlockSpecialLinear {R : Type u} [CommRing R] (b : Matrix.SpecialLinearGroup (Fin 3) R) : Matrix.SpecialLinearGroup (Fin 4) R

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

Equations

• ConnesRigidity.MonicMatrixElimination.lowerBlockSpecialLinear b = ⟨ConnesRigidity.MonicMatrixElimination.lowerBlockMatrix ↑b, ⋯⟩

def ConnesRigidity.StabilizedBlockReduction.StabilizedThreeElementaryGeneration (R : Type u) [CommRing R] : Prop

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

Equations

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

def ConnesRigidity.StabilizedBlockReduction.stabilizedTwoMatrix {R : Type u} [CommRing R] (b : Matrix (Fin 2) (Fin 2) R) : Matrix (Fin 3) (Fin 3) R

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

Equations

• ConnesRigidity.StabilizedBlockReduction.stabilizedTwoMatrix b = (Matrix.reindex finSumFinEquiv finSumFinEquiv) (Matrix.fromBlocks b 0 0 1)

def ConnesRigidity.StabilizedBlockReduction.stabilizedTwoSpecialLinear {R : Type u} [CommRing R] (b : Matrix.SpecialLinearGroup (Fin 2) R) : Matrix.SpecialLinearGroup (Fin 3) R

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

Equations

• ConnesRigidity.StabilizedBlockReduction.stabilizedTwoSpecialLinear b = ⟨ConnesRigidity.StabilizedBlockReduction.stabilizedTwoMatrix ↑b, ⋯⟩

@[simp]

theorem ConnesRigidity.StabilizedBlockReduction.stabilizedTwoSpecialLinear_one {R : Type u} [CommRing R] : stabilizedTwoSpecialLinear 1 = 1

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

@[simp]

theorem ConnesRigidity.StabilizedBlockReduction.stabilizedTwoSpecialLinear_mul {R : Type u} [CommRing R] (b c : Matrix.SpecialLinearGroup (Fin 2) R) : stabilizedTwoSpecialLinear (b * c) = stabilizedTwoSpecialLinear b * stabilizedTwoSpecialLinear c

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

def ConnesRigidity.StabilizedBlockReduction.stabilizedTwoHom {R : Type u} [CommRing R] : Matrix.SpecialLinearGroup (Fin 2) R →* Matrix.SpecialLinearGroup (Fin 3) R

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

Equations

• ConnesRigidity.StabilizedBlockReduction.stabilizedTwoHom = { toFun := ConnesRigidity.StabilizedBlockReduction.stabilizedTwoSpecialLinear, map_one' := ⋯, map_mul' := ⋯ }

def ConnesRigidity.StabilizedBlockReduction.elementaryThreeSubgroup (R : Type u) [CommRing R] : Subgroup (Matrix.SpecialLinearGroup (Fin 3) R)

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

Equations

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

theorem ConnesRigidity.StabilizedBlockReduction.lowerBlock_mem_of_elementaryThree {R : Type u} [CommRing R] (b : Matrix.SpecialLinearGroup (Fin 3) R) (hb : b ∈ elementaryThreeSubgroup R) : MonicMatrixElimination.lowerBlockSpecialLinear b ∈ localGlobalElementarySubgroup R

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

@[reducible, inline]

abbrev ConnesRigidity.FieldPolynomialElementaryThree.G (R : Type u_2) [EuclideanDomain R] : Type u_2

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

Equations

• ConnesRigidity.FieldPolynomialElementaryThree.G R = Matrix.SpecialLinearGroup (Fin 3) R

theorem ConnesRigidity.suslin_exists_finset_denominators_of_primeCompl {A : Type u} [CommRing A] (P : A → Prop) (hlocal : ∀ (m : Ideal A) [inst : m.IsMaximal], ∃ (d : ↥m.primeCompl), P ↑d) : ∃ (s : Finset A), (∀ d ∈ s, P d) ∧ Ideal.span ↑s = ⊤

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

noncomputable def ConnesRigidity.suslinAwayToAtPrime {A : Type u} [CommRing A] (m : Ideal A) [m.IsPrime] (d : ↥m.primeCompl) : Localization.Away ↑d →+* Localization.AtPrime m

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

Equations

• ConnesRigidity.suslinAwayToAtPrime m d = IsLocalization.Away.lift ↑d ⋯

@[simp]

theorem ConnesRigidity.suslinAwayToAtPrime_algebraMap {A : Type u} [CommRing A] (m : Ideal A) [m.IsPrime] (d : ↥m.primeCompl) (a : A) : (suslinAwayToAtPrime m d) ((algebraMap A (Localization.Away ↑d)) a) = (algebraMap A (Localization.AtPrime m)) a

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

def ConnesRigidity.suslinAwayElementary {A : Type u} [CommRing A] (g : Matrix.SpecialLinearGroup Index (Polynomial A)) (d : A) : Prop

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

Equations

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

theorem ConnesRigidity.suslin_exists_away_elementary_word_lift_atPrime {A : Type u} [CommRing A] (m : Ideal A) [m.IsPrime] (g : Matrix.SpecialLinearGroup Index (Polynomial (Localization.AtPrime m))) (hg : g ∈ localGlobalElementarySubgroup (Polynomial (Localization.AtPrime m))) : ∃ (d : ↥m.primeCompl), ∃ q ∈ localGlobalElementarySubgroup (Polynomial (Localization.Away ↑d)), (Matrix.SpecialLinearGroup.map (Polynomial.mapRingHom (suslinAwayToAtPrime m d))) q = g

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

theorem ConnesRigidity.suslin_specialLinear_elementary_of_stableRangeThree_of_stabilizedThree {R : Type u} [CommRing R] (hstable : BassStableRangeAtMost R 3) (hblock : StabilizedBlockReduction.StabilizedThreeElementaryGeneration R) (g : Matrix.SpecialLinearGroup (Fin 4) R) : g ∈ localGlobalElementarySubgroup R

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

theorem ConnesRigidity.MennickeIdentity.specialLinear_mul_transvection_apply {ι : Type u_1} {A : Type u_2} [Fintype ι] [DecidableEq ι] [CommRing A] (x : Matrix.SpecialLinearGroup ι A) {i j : ι} (hij : i ≠ j) (r : A) (a b : ι) : ↑(x * Matrix.SpecialLinearGroup.transvection hij r) a b = if b = j then ↑x a j + r * ↑x a i else ↑x a b

Right multiplication by a transvection, entrywise. Shared by the block computations in CarryAndCrossedProduct and GroupConstruction, so keep it exported.

theorem ConnesRigidity.suslin_dvr_stabilized_two_mem {A : Type u} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (b : Matrix.SpecialLinearGroup (Fin 2) (Polynomial A)) : StabilizedBlockReduction.stabilizedTwoHom b ∈ StabilizedBlockReduction.elementaryThreeSubgroup (Polynomial A)

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

theorem ConnesRigidity.suslin_valuation_unimodular_three_elementary_reduce {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (v : Fin 3 → Polynomial A) (hv : UnimodularRow v) : ∃ e ∈ StabilizedBlockReduction.elementaryThreeSubgroup (Polynomial A), e • v = Pi.single 2 1

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

theorem ConnesRigidity.HorrocksValuationInduction.specialLinearThree_mem_of_lastColumnTransitivity_and_stabilizedTwo {R : Type u} [CommRing R] (htrans : ∀ (v : Fin 3 → R), UnimodularRow v → ∃ e ∈ StabilizedBlockReduction.elementaryThreeSubgroup R, e • v = Pi.single 2 1) (hblock : ∀ (b : Matrix.SpecialLinearGroup (Fin 2) R), StabilizedBlockReduction.stabilizedTwoHom b ∈ StabilizedBlockReduction.elementaryThreeSubgroup R) (g : Matrix.SpecialLinearGroup (Fin 3) R) : g ∈ StabilizedBlockReduction.elementaryThreeSubgroup R

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

@[reducible, inline]

abbrev ConnesRigidity.IntegerElementaryProof.IGroup : Type

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

Equations

• ConnesRigidity.IntegerElementaryProof.IGroup = ConnesRigidity.IntegerSpecialLinearGroup

@[reducible, inline]

abbrev ConnesRigidity.IntegerElementaryProof.IVec : Type

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

Equations

• ConnesRigidity.IntegerElementaryProof.IVec = (ConnesRigidity.Index → ℤ)

def ConnesRigidity.IntegerElementaryProof.elementary : Subgroup IGroup

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

Equations

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

theorem ConnesRigidity.IntegerElementaryProof.transvection_mem (i j : Index) (h : i ≠ j) (a : ℤ) : Matrix.SpecialLinearGroup.transvection h a ∈ elementary

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

theorem ConnesRigidity.IntegerElementaryProof.transvection_smul_same (i j : Index) (h : i ≠ j) (c : ℤ) (v : IVec) : (Matrix.SpecialLinearGroup.transvection h c • v) i = v i + c * v j

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

theorem ConnesRigidity.IntegerElementaryProof.transvection_smul_other (i j k : Index) (h : i ≠ j) (hk : k ≠ i) (c : ℤ) (v : IVec) : (Matrix.SpecialLinearGroup.transvection h c • v) k = v k

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

def ConnesRigidity.IntegerElementaryProof.coordinateRotation (i j : Index) (h : i ≠ j) : IGroup

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

Equations

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

def ConnesRigidity.IntegerElementaryProof.euclideanStep (i j : Index) (h : i ≠ j) (a b : ℤ) : IGroup

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

Equations

• ConnesRigidity.IntegerElementaryProof.euclideanStep i j h a b = ConnesRigidity.IntegerElementaryProof.coordinateRotation i j h * Matrix.SpecialLinearGroup.transvection ⋯ (-(b / a))

theorem ConnesRigidity.IntegerElementaryProof.euclideanStep_mem (i j : Index) (h : i ≠ j) (a b : ℤ) : euclideanStep i j h a b ∈ elementary

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

theorem ConnesRigidity.IntegerElementaryProof.euclideanStep_smul_left (i j : Index) (h : i ≠ j) (v : IVec) : (euclideanStep i j h (v i) (v j) • v) i = v j % v i

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

theorem ConnesRigidity.IntegerElementaryProof.euclideanStep_smul_right (i j : Index) (h : i ≠ j) (v : IVec) : (euclideanStep i j h (v i) (v j) • v) j = -v i

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

theorem ConnesRigidity.IntegerElementaryProof.euclideanStep_smul_other (i j k : Index) (h : i ≠ j) (hki : k ≠ i) (hkj : k ≠ j) (v : IVec) : (euclideanStep i j h (v i) (v j) • v) k = v k

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

theorem ConnesRigidity.IntegerElementaryProof.pair_reduce (i j : Index) (h : i ≠ j) (v : IVec) : ∃ g ∈ elementary, (g • v) j = 0 ∧ (∀ (k : Index), k ≠ i → k ≠ j → (g • v) k = v k) ∧ ∀ (w : IVec), w i = 0 → w j = 0 → g • w = w

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

theorem ConnesRigidity.IntegerElementaryProof.first_column_reduce (A : IGroup) : ∃ g ∈ elementary, ↑(g * A) 1 0 = 0 ∧ ↑(g * A) 2 0 = 0 ∧ ↑(g * A) 3 0 = 0

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

theorem ConnesRigidity.IntegerElementaryProof.second_column_reduce (A : IGroup) (h₁₀ : ↑A 1 0 = 0) (h₂₀ : ↑A 2 0 = 0) (h₃₀ : ↑A 3 0 = 0) : ∃ p ∈ elementary, ↑(p * A) 1 0 = 0 ∧ ↑(p * A) 2 0 = 0 ∧ ↑(p * A) 3 0 = 0 ∧ ↑(p * A) 2 1 = 0 ∧ ↑(p * A) 3 1 = 0

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

theorem ConnesRigidity.IntegerElementaryProof.third_column_reduce (A : IGroup) (h10 : ↑A 1 0 = 0) (h20 : ↑A 2 0 = 0) (h30 : ↑A 3 0 = 0) (h21 : ↑A 2 1 = 0) (h31 : ↑A 3 1 = 0) : ∃ p ∈ elementary, ↑(p * A) 1 0 = 0 ∧ ↑(p * A) 2 0 = 0 ∧ ↑(p * A) 3 0 = 0 ∧ ↑(p * A) 2 1 = 0 ∧ ↑(p * A) 3 1 = 0 ∧ ↑(p * A) 3 2 = 0

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

theorem ConnesRigidity.IntegerElementaryProof.fin_four_upperTriangular_of_six (A : IGroup) (h10 : ↑A 1 0 = 0) (h20 : ↑A 2 0 = 0) (h30 : ↑A 3 0 = 0) (h21 : ↑A 2 1 = 0) (h31 : ↑A 3 1 = 0) (h32 : ↑A 3 2 = 0) (i j : Index) : j < i → ↑A i j = 0

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

theorem ConnesRigidity.IntegerElementaryProof.upper_triangularize (A : IGroup) : ∃ g ∈ elementary, ∀ (i j : Index), j < i → ↑(g * A) i j = 0

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

theorem ConnesRigidity.IntegerElementaryProof.upperUnitriangular_factorization (g : IGroup) (hu : ∀ (i j : Index), j < i → ↑g i j = 0) (hd : ∀ (i : Index), ↑g i i = 1) : g = Matrix.SpecialLinearGroup.transvection ⋯ (↑g 2 3) * Matrix.SpecialLinearGroup.transvection ⋯ (↑g 1 3) * Matrix.SpecialLinearGroup.transvection ⋯ (↑g 1 2) * Matrix.SpecialLinearGroup.transvection ⋯ (↑g 0 3) * Matrix.SpecialLinearGroup.transvection ⋯ (↑g 0 2) * Matrix.SpecialLinearGroup.transvection ⋯ (↑g 0 1)

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

theorem ConnesRigidity.IntegerElementaryProof.upperUnitriangular_mem (g : IGroup) (hu : ∀ (i j : Index), j < i → ↑g i j = 0) (hd : ∀ (i : Index), ↑g i i = 1) : g ∈ elementary

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

theorem ConnesRigidity.IntegerElementaryProof.elementary_eq_top : elementary = ⊤

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