diff --git a/LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean b/LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean index 9c61c2b982..8d7ef5e10c 100644 --- a/LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean +++ b/LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean @@ -7,28 +7,22 @@ Authors: OpenAI, Dean Cureton module public import Mathlib.Algebra.Group.MinimalAxioms -public import Mathlib.Algebra.Module.ZMod public import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar -public import Mathlib.Data.Finsupp.Encodable public import Mathlib.Data.Finsupp.Pointwise public import Mathlib.GroupTheory.SemidirectProduct -public import Mathlib.LinearAlgebra.Countable -public import Mathlib.MeasureTheory.Function.ContinuousMapDense public import Mathlib.MeasureTheory.Function.Holder public import Mathlib.MeasureTheory.Function.L2Space -public import Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm -public import Mathlib.MeasureTheory.Group.Integral -public import Mathlib.MeasureTheory.Measure.Regular -public import Mathlib.RingTheory.DedekindDomain.Dvr -public import Mathlib.RingTheory.KrullDimension.Polynomial -public import Mathlib.RingTheory.Localization.Algebra public import Mathlib.Topology.Algebra.PontryaginDual -public import Mathlib.Topology.Constructions -public import Mathlib.Topology.ContinuousMap.SecondCountableSpace -public import Mathlib.Topology.ContinuousMap.StoneWeierstrass public import Mathlib.Topology.Instances.ZMod -public import Mathlib.Topology.Metrizable.Urysohn public import LeanPool.InfiniteConnesRigidity.UniversalLattice +import Mathlib.LinearAlgebra.Countable +import Mathlib.MeasureTheory.Function.ContinuousMapDense +import Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm +import Mathlib.MeasureTheory.Group.Integral +import Mathlib.RingTheory.KrullDimension.Polynomial +import Mathlib.Topology.ContinuousMap.SecondCountableSpace +import Mathlib.Topology.ContinuousMap.StoneWeierstrass +import Mathlib.Topology.Metrizable.Urysohn /-! # Carry groups, duality, and crossed products @@ -1919,15 +1913,12 @@ private theorem cornulierColumnRootProduct_apply (v : Index → IntegralPolynomi (show (2 : Index) ≠ cornulierLast by decide) (v 2) : IntegralSpecialLinearGroup) p q = _ fin_cases p <;> fin_cases q <;> - simp only [cornulierLast, Fin.isValue, Nat.reduceAdd, Fin.zero_eta, - Matrix.SpecialLinearGroup.coe_mul, - Matrix.SpecialLinearGroup.transvection_coe, Matrix.mul_apply, - Matrix.add_apply, Matrix.one_apply, Matrix.single_apply, true_and, - Fin.sum_univ_four, ↓reduceIte, Fin.reduceEq, add_zero, one_ne_zero, - false_and, mul_ite, mul_one, mul_zero, zero_ne_one, zero_mul, ite_self, - zero_add, and_false, - Finset.sum_ite_eq', Finset.mem_univ, Fin.mk_one, Fin.reduceFinMk, - and_true, ite_mul, one_mul, Finset.sum_ite_eq] + simp only [cornulierLast, Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + ConnesRigidity.MennickeIdentity.specialLinear_mul_transvection_apply, Fin.reduceEq, + ↓reduceIte, + Matrix.SpecialLinearGroup.transvection_coe, Matrix.add_apply, Matrix.one_apply, + Matrix.single_apply, one_ne_zero, zero_ne_one, and_self, and_false, and_true, mul_one, + mul_zero, add_zero, zero_add] /-- Cross-module support for the infinite Connes-rigidity construction. -/ private def cornulierRowRootProduct (v : Index → IntegralPolynomial) : @@ -1962,15 +1953,12 @@ private theorem cornulierRowRootProduct_apply (v : Index → IntegralPolynomial) (show cornulierLast ≠ (2 : Index) by decide) (v 2) : IntegralSpecialLinearGroup) p q = _ fin_cases p <;> fin_cases q <;> - simp only [cornulierLast, Fin.isValue, Nat.reduceAdd, Fin.zero_eta, - Matrix.SpecialLinearGroup.coe_mul, - Matrix.SpecialLinearGroup.transvection_coe, Matrix.mul_apply, - Matrix.add_apply, Matrix.one_apply, Matrix.single_apply, true_and, - Fin.sum_univ_four, ↓reduceIte, Fin.reduceEq, add_zero, one_ne_zero, - false_and, mul_ite, mul_one, mul_zero, zero_ne_one, zero_mul, ite_self, - zero_add, and_false, - Finset.sum_ite_eq', Finset.mem_univ, Fin.mk_one, Fin.reduceFinMk, - and_true, ite_mul, one_mul, Finset.sum_ite_eq] + simp only [cornulierLast, Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + ConnesRigidity.MennickeIdentity.specialLinear_mul_transvection_apply, Fin.reduceEq, + ↓reduceIte, + Matrix.SpecialLinearGroup.transvection_coe, Matrix.add_apply, Matrix.one_apply, + Matrix.single_apply, one_ne_zero, zero_ne_one, and_self, and_false, and_true, mul_one, + mul_zero, add_zero, zero_add] /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem cornulier_conjugate_K₁_root_mem @@ -4384,7 +4372,8 @@ def coordinateProduct : V →ₗ[F] V →ₗ[F] V where apply auxiliaryBasis.repr.injective ext i simp only [map_smul, Basis.repr_symm_apply, Basis.repr_linearCombination, Finsupp.mul_apply, - Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, mul_left_comm, RingHom.id_apply] } + Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, RingHom.id_apply] + ring } map_add' x y := by apply LinearMap.ext intro z @@ -6276,9 +6265,12 @@ public def kDLinear : K →* (D ≃ₗ[F] D) where toFun k := (kLinear k).prodCongr (kDividedSquareLinear k) map_one' := by - ext d <;> simp + ext d <;> + simp only [map_one, LinearEquiv.prodCongr_apply, LinearEquiv.coe_one, id_eq, Prod.mk.eta] map_mul' k l := by - ext d <;> simp + ext d <;> + simp only [map_mul, LinearEquiv.prodCongr_apply, LinearEquiv.mul_apply, kLinear_apply, + kDividedSquareLinear_val] @@ -7113,13 +7105,13 @@ def crossedIndexEquiv ⟨fun k ↦ ξ (e.symm k), by change Memℓp (fun k ↦ ξ (e.symm k)) 2 rw [memℓp_gen_iff (by norm_num : 0 < (2 : ℝ≥0∞).toReal)] - exact (e.symm.summable_iff).2 + exact (e.symm.summable_iff (f := fun i ↦ ‖ξ i‖ ^ (2 : ℝ≥0∞).toReal)).2 ((lp.memℓp ξ).summable (by norm_num : 0 < (2 : ℝ≥0∞).toReal))⟩ invFun := fun ξ ↦ ⟨fun k ↦ ξ (e k), by change Memℓp (fun k ↦ ξ (e k)) 2 rw [memℓp_gen_iff (by norm_num : 0 < (2 : ℝ≥0∞).toReal)] - exact (e.summable_iff).2 + exact (e.summable_iff (f := fun i ↦ ‖ξ i‖ ^ (2 : ℝ≥0∞).toReal)).2 ((lp.memℓp ξ).summable (by norm_num : 0 < (2 : ℝ≥0∞).toReal))⟩ left_inv := by intro ξ diff --git a/LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean b/LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean index 89e4841e0c..9e30dedc75 100644 --- a/LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean +++ b/LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean @@ -3449,8 +3449,7 @@ private def gammaGroupFactorUnitary (n : ℕ) : private def lambdaGroupFactorUnitary : GroupL2 lambdaGroup ≃ₗᵢ[ℂ] crossedHilbert paperSplitHaarAction := by - change GroupL2 (SemidirectProduct (Multiplicative D) K kDAction) ≃ₗᵢ[ℂ] - crossedHilbert paperSplitHaarAction + change GroupL2 Lambda ≃ₗᵢ[ℂ] crossedHilbert paperSplitHaarAction exact groupFactorUnitary kDAction paperSplitHaarAction splitFourierEquiv end @@ -3730,12 +3729,8 @@ private theorem lambdaGroupFactorUnitary_conj_inr (k : K) : paperSplitHaarAction k).toContinuousLinearEquiv.toContinuousLinearMap := by change (groupFactorUnitary kDAction paperSplitHaarAction splitFourierEquiv).conjStarAlgEquiv - (leftRegularUnitary - (SemidirectProduct.inr k : - SemidirectProduct (Multiplicative D) K kDAction) : - GroupL2 (SemidirectProduct (Multiplicative D) K kDAction) - →L[ℂ] - GroupL2 (SemidirectProduct (Multiplicative D) K kDAction)) = + (leftRegularUnitary (SemidirectProduct.inr k : Lambda) : + GroupL2 Lambda →L[ℂ] GroupL2 Lambda) = (crossedGroupUnitary paperSplitHaarAction k).toContinuousLinearEquiv.toContinuousLinearMap apply groupFactorUnitary_conj_inr exact splitTaggedFourierCovariance @@ -3847,17 +3842,17 @@ private def toStarAlgEquiv (U : PaperFactorUnitaryWitness G H) : exact U.unitary.conjStarAlgEquiv.apply_symm_apply y map_mul' x y := by apply Subtype.ext - exact map_mul U.unitary.conjStarAlgEquiv + exact U.unitary.conjStarAlgEquiv.map_mul' (x : GroupL2 G →L[ℂ] GroupL2 G) (y : GroupL2 G →L[ℂ] GroupL2 G) map_add' x y := by apply Subtype.ext - exact map_add U.unitary.conjStarAlgEquiv + exact U.unitary.conjStarAlgEquiv.map_add' (x : GroupL2 G →L[ℂ] GroupL2 G) (y : GroupL2 G →L[ℂ] GroupL2 G) map_star' x := by apply Subtype.ext - exact map_star U.unitary.conjStarAlgEquiv + exact U.unitary.conjStarAlgEquiv.map_star' (x : GroupL2 G →L[ℂ] GroupL2 G) map_smul' c x := by apply Subtype.ext @@ -5115,7 +5110,6 @@ private structure PaperAnalyticInput where /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem paperLambda_hasNoOrderFour : HasNoOrderFour Lambda := by - change HasNoOrderFour (SemidirectProduct (Multiplicative D) K kDAction) apply semidirect_hasNoOrderFour_of_no_nontrivial_torsion_of_exponentTwo (N := Multiplicative D) (Q := K) kDAction K_no_nontrivial_torsion intro d diff --git a/LeanPool/InfiniteConnesRigidity/GroupConstruction.lean b/LeanPool/InfiniteConnesRigidity/GroupConstruction.lean index c4a144d235..26544070d0 100644 --- a/LeanPool/InfiniteConnesRigidity/GroupConstruction.lean +++ b/LeanPool/InfiniteConnesRigidity/GroupConstruction.lean @@ -6263,7 +6263,7 @@ private theorem shalom_normalizedFixedVector_of_relativePair ((‖p‖ : ℂ)⁻¹) • (p : W)‖ < _ rw [map_smul, ← smul_sub, norm_smul, norm_inv, Complex.norm_real, Real.norm_of_nonneg (norm_nonneg p)] - simpa only [← Submodule.norm_coe, div_eq_mul_inv, mul_comm] using hfrac + simpa only [← Submodule.norm_coe, div_eq_inv_mul] using hfrac /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem shalom_normalizedConstantFixedVector_of_integerPair @@ -7533,15 +7533,12 @@ private theorem upperUnitriangular_factorization (g : Q) apply Matrix.SpecialLinearGroup.ext intro i j fin_cases i <;> fin_cases j <;> - simp only [Nat.reduceAdd, Fin.zero_eta, Fin.isValue, Fin.mk_one, - Fin.reduceFinMk, Matrix.SpecialLinearGroup.coe_mul, - Matrix.SpecialLinearGroup.transvection_coe, Matrix.mul_apply, - Matrix.add_apply, Matrix.one_apply, Fin.reduceEq, false_and, - not_false_eq_true, Matrix.single_apply_of_ne, add_zero, - Matrix.single_apply, ite_mul, one_mul, zero_mul, Finset.sum_ite_eq, - Finset.mem_univ, ↓reduceIte, one_ne_zero, true_and, - Fin.sum_univ_four, zero_ne_one, mul_ite, mul_one, mul_zero, - ite_self, zero_add, and_false, Finset.sum_ite_eq', and_true, + simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + ConnesRigidity.MennickeIdentity.specialLinear_mul_transvection_apply, Fin.reduceEq, + ↓reduceIte, + Matrix.SpecialLinearGroup.transvection_coe, Matrix.add_apply, Matrix.one_apply, + Matrix.single_apply, one_ne_zero, zero_ne_one, and_self, and_false, and_true, + mul_one, mul_zero, add_zero, zero_add, h00, h11, h22, h33, h10, h20, h21, h30, h31, h32] /-- Cross-module support for the infinite Connes-rigidity construction. -/ diff --git a/LeanPool/InfiniteConnesRigidity/SpectralAndPropertyT.lean b/LeanPool/InfiniteConnesRigidity/SpectralAndPropertyT.lean index 1ea4e6f78a..2e230d9c2d 100644 --- a/LeanPool/InfiniteConnesRigidity/SpectralAndPropertyT.lean +++ b/LeanPool/InfiniteConnesRigidity/SpectralAndPropertyT.lean @@ -6,17 +6,11 @@ Authors: OpenAI, Dean Cureton module -public import Mathlib.Algebra.Order.Module.PositiveLinearMap public import Mathlib.Analysis.CStarAlgebra.GelfandDuality -public import Mathlib.Analysis.InnerProductSpace.Reproducing public import Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real public import Mathlib.MeasureTheory.Measure.ProbabilityMeasure public import Mathlib.Order.CompletePartialOrder -public import Mathlib.Probability.ConditionalProbability -public import Mathlib.Topology.ContinuousMap.CompactlySupported -public import Mathlib.Topology.Algebra.LinearMapCompletion import Mathlib.Algebra.Ring.IsFormallyReal -import Mathlib.Analysis.Matrix.Order import Mathlib.RingTheory.PiTensorProduct import Mathlib.RingTheory.WittVector.IsPoly import Mathlib.Tactic.ENatToNat @@ -25,6 +19,9 @@ import Mathlib.Tactic.ReduceModChar import Mathlib.Topology.Metrizable.Urysohn import Std.Tactic.BVDecide.Normalize.Prop public import LeanPool.InfiniteConnesRigidity.CarryAndCrossedProduct +import Mathlib.Analysis.InnerProductSpace.Reproducing +import Mathlib.Analysis.Matrix.Order +import Mathlib.Topology.Algebra.LinearMapCompletion /-! # Spectral methods and property (T) @@ -579,7 +576,7 @@ private theorem invariant_of_kernel_and_quotient π.IsInvariant ξ := by intro g obtain ⟨a, h, rfl⟩ := E.exists_kernel_mul_splitting g - rw [map_mul] + rw [MonoidHom.map_mul] change (π (E.inclusion (Multiplicative.ofAdd a)) : V →L[ℂ] V) ((π (E.splitting h) : V →L[ℂ] V) ξ) = ξ @@ -1062,14 +1059,14 @@ private def quotientFixedOrthogonalIsometry change (↑(π (E.splitting h⁻¹) * π (E.splitting h)) : V →L[ℂ] V) x = x - rw [← map_mul, ← map_mul] + rw [← MonoidHom.map_mul, ← MonoidHom.map_mul] simp only [inv_mul_cancel, map_one, OneMemClass.coe_one, one_apply_eq_self] right_inv x := by apply Subtype.ext change (↑(π (E.splitting h) * π (E.splitting h⁻¹)) : V →L[ℂ] V) x = x - rw [← map_mul, ← map_mul] + rw [← MonoidHom.map_mul, ← MonoidHom.map_mul] simp only [mul_inv_cancel, map_one, OneMemClass.coe_one, one_apply_eq_self] map_add' x y := by apply Subtype.ext @@ -1096,7 +1093,7 @@ private def quotientFixedOrthogonalIsometryHom (π (E.splitting (g * h)) : V →L[ℂ] V) x = (π (E.splitting g) : V →L[ℂ] V) ((π (E.splitting h) : V →L[ℂ] V) x) - rw [map_mul, map_mul] + rw [MonoidHom.map_mul, MonoidHom.map_mul] rfl /-- Cross-module support for the infinite Connes-rigidity construction. -/ @@ -1699,7 +1696,7 @@ private theorem quotient_preserves_kernelFixedSubmodule let b : A := (Multiplicative.toAdd (E.action h⁻¹)) a have haction : (Multiplicative.toAdd (E.action h)) b = a := by change (Multiplicative.toAdd (E.action h * E.action h⁻¹)) a = a - rw [← map_mul] + rw [← MonoidHom.map_mul] simp only [mul_inv_cancel, map_one, toAdd_one, AddAut.zero_apply] have hconj := E.conjugation h b rw [haction] at hconj @@ -1717,12 +1714,12 @@ private theorem quotient_preserves_kernelFixedSubmodule (π (E.inclusion (Multiplicative.ofAdd a)) : V →L[ℂ] V) ((π (E.splitting h) : V →L[ℂ] V) x) = (π (E.inclusion (Multiplicative.ofAdd a) * E.splitting h) : - V →L[ℂ] V) x := by rw [map_mul]; rfl + V →L[ℂ] V) x := by rw [MonoidHom.map_mul]; rfl _ = (π (E.splitting h * E.inclusion (Multiplicative.ofAdd b)) : V →L[ℂ] V) x := by rw [hcomm] _ = (π (E.splitting h) : V →L[ℂ] V) ((π (E.inclusion (Multiplicative.ofAdd b)) : V →L[ℂ] V) x) := by - rw [map_mul] + rw [MonoidHom.map_mul] rfl _ = (π (E.splitting h) : V →L[ℂ] V) x := by rw [hfixed] @@ -1749,7 +1746,7 @@ private theorem quotient_map_kernelFixedSubmodule ((π (E.splitting h⁻¹) : V →L[ℂ] V) x) = x have hop : π (E.splitting h) * π (E.splitting h⁻¹) = 1 := by - rw [← map_mul, ← map_mul] + rw [← MonoidHom.map_mul, ← MonoidHom.map_mul] simp only [mul_inv_cancel, map_one] have hx' := DFunLike.congr_fun (congrArg (fun U : unitary (V →L[ℂ] V) ↦ (U : V →L[ℂ] V)) hop) x @@ -1867,12 +1864,12 @@ private theorem kernel_orbit_sub_norm E.inclusion (Multiplicative.ofAdd a) = E.inclusion (Multiplicative.ofAdd b) * E.inclusion (Multiplicative.ofAdd (a - b)) := by - rw [← map_mul] + rw [← MonoidHom.map_mul] apply congrArg E.inclusion apply Multiplicative.toAdd.injective change a = b + (a - b) abel - rw [hmul, map_mul] + rw [hmul, MonoidHom.map_mul] rfl rw [hfactor] exact Unitary.norm_map U z @@ -2638,7 +2635,7 @@ theorem dualCharacterAction_mul χ (Multiplicative.ofAdd ((Multiplicative.toAdd (action h⁻¹)) ((Multiplicative.toAdd (action g⁻¹)) (Multiplicative.toAdd a)))) - rw [mul_inv_rev, map_mul] + rw [mul_inv_rev, MonoidHom.map_mul] rfl /-- Cross-module support for the infinite Connes-rigidity construction. -/ @@ -2789,7 +2786,7 @@ private theorem quotientOperatorConjugation_kernel (↑(π (E.splitting h) * π (E.inclusion (Multiplicative.ofAdd a)) * π ((E.splitting h)⁻¹)) : V →L[ℂ] V) = _ - rw [← map_mul, ← map_mul, E.conjugation] + rw [← MonoidHom.map_mul, ← MonoidHom.map_mul, E.conjugation] omit [TopologicalSpace A] [DiscreteTopology A] in /-- Cross-module support for the infinite Connes-rigidity construction. -/ @@ -2809,7 +2806,7 @@ private theorem quotientOperatorConjugation_generators_image rw [quotientOperatorConjugation_kernel] congr 3 change (Multiplicative.toAdd (E.action h * E.action h⁻¹)) a = a - rw [← map_mul] + rw [← MonoidHom.map_mul] simp only [mul_inv_cancel, map_one, toAdd_one, AddAut.zero_apply] omit [TopologicalSpace A] [DiscreteTopology A] in @@ -2884,7 +2881,7 @@ private def quotientSpectralOperatorConjugation (S : V →L[ℂ] V) (T : V →L[ℂ] V) map_star' T := by apply Subtype.ext - exact map_star (quotientOperatorConjugation E π h) + exact (quotientOperatorConjugation E π h).map_star' (T : V →L[ℂ] V) map_smul' c T := by apply Subtype.ext @@ -3354,7 +3351,7 @@ private theorem kernelUnitary_preserves_closedConvexHull (Multiplicative.ofAdd a * Multiplicative.ofAdd b)) : V →L[ℂ] V) x = ((↑(π (E.inclusion (Multiplicative.ofAdd a)) * π (E.inclusion (Multiplicative.ofAdd b))) : V →L[ℂ] V)) x - rw [E.inclusion.map_mul, map_mul] + rw [E.inclusion.map_mul, MonoidHom.map_mul] have hhull : U '' convexHull ℝ orbit ⊆ convexHull ℝ orbit := by change U.toLinearMap '' convexHull ℝ orbit ⊆ convexHull ℝ orbit rw [LinearMap.image_convexHull] @@ -3892,7 +3889,7 @@ def affineLinearIsometryHom rfl map_mul' g h := by ext x - rw [map_mul] + rw [MonoidHom.map_mul] rfl /-- Cross-module support for the infinite Connes-rigidity construction. -/ @@ -3929,11 +3926,11 @@ theorem IsAffineFixed.normalizer_action group calc α (k : G) (α g x) = α ((k : G) * g) x := by - rw [map_mul] + rw [MonoidHom.map_mul] rfl _ = α (g * (k' : G)) x := by rw [hkg] _ = α g (α (k' : G) x) := by - rw [map_mul] + rw [MonoidHom.map_mul] rfl _ = α g x := by rw [hx k'] @@ -4003,7 +4000,7 @@ private def affineLinearStabilizer mul_mem' := by intro g h hg hh change (affineLinearRepresentation α (g * h) : V →L[ℂ] V) x = x - rw [map_mul] + rw [MonoidHom.map_mul] change (affineLinearRepresentation α g : V →L[ℂ] V) ((affineLinearRepresentation α h : V →L[ℂ] V) x) = x rw [hh, hg] @@ -4015,7 +4012,7 @@ private def affineLinearStabilizer (affineLinearRepresentation α g⁻¹ : V →L[ℂ] V) ((affineLinearRepresentation α g : V →L[ℂ] V) x) := by rw [hg] _ = (affineLinearRepresentation α (g⁻¹ * g) : V →L[ℂ] V) x := by - rw [map_mul] + rw [MonoidHom.map_mul] rfl _ = x := by simp only [inv_mul_cancel, map_one, OneMemClass.coe_one, one_apply_eq_self] @@ -4266,7 +4263,7 @@ private theorem actionPreKernelTranslation_mul_apply {G I : Type u} [Group G] Finsupp.domLCongr_single] change Finsupp.single (ρ (a * b) i.1, i.2) z = Finsupp.single (ρ a (ρ b i.1), i.2) z - rw [map_mul] + rw [MonoidHom.map_mul] rfl /-- Cross-module support for the infinite Connes-rigidity construction. -/ @@ -4538,7 +4535,7 @@ def unitaryCocycleAffineAction intro x change π (g * h) x + b (g * h) = π g (π h x + b h) + b g - rw [map_mul, hb, map_add] + rw [MonoidHom.map_mul, hb, map_add] change π g (π h x) + (b g + π g (b h)) = (π g (π h x) + π g (b h)) + b g abel @@ -4762,7 +4759,7 @@ theorem markedPairCocycle_mul markedPairCocycle R i₀ g + R.representation g (markedPairCocycle R i₀ h) := by unfold markedPairCocycle - rw [R.equivariant, map_mul] + rw [R.equivariant, MonoidHom.map_mul] change R.realization.vector (ρ g (ρ h i₀), i₀) = R.realization.vector (ρ g i₀, i₀) + R.realization.vector (ρ g (ρ h i₀), ρ g i₀) @@ -5152,7 +5149,7 @@ private theorem markedAffineOrbitPoint_action α a (markedAffineOrbitPoint α x y i) := by change α (a * i.1) (if i.2 then x else y) = α a (α i.1 (if i.2 then x else y)) - rw [map_mul] + rw [MonoidHom.map_mul] rfl /-- Cross-module support for the infinite Connes-rigidity construction. -/ @@ -5674,7 +5671,7 @@ private theorem unitary_mem_normalFixedSubmodule calc (π (n : G) : H →L[ℂ] H) ((π g : H →L[ℂ] H) x) = (π ((n : G) * g) : H →L[ℂ] H) x := by - rw [map_mul] + rw [MonoidHom.map_mul] rfl _ = (π (g * (n' : G)) : H →L[ℂ] H) x := by have heq : (n : G) * g = g * (g⁻¹ * (n : G) * g) := by @@ -5684,7 +5681,7 @@ private theorem unitary_mem_normalFixedSubmodule rw [heq] _ = (π g : H →L[ℂ] H) ((π (n' : G) : H →L[ℂ] H) x) := by - rw [map_mul] + rw [MonoidHom.map_mul] rfl _ = (π g : H →L[ℂ] H) x := by rw [hx n'] @@ -5706,7 +5703,7 @@ theorem unitary_mem_normalFixedSubmodule_orthogonal ((π g : H →L[ℂ] H) x) := by congr 1 change y = (↑(π g * π g⁻¹) : H →L[ℂ] H) y - rw [← map_mul] + rw [← MonoidHom.map_mul] simp only [mul_inv_cancel, map_one, OneMemClass.coe_one, one_apply_eq_self] _ = @inner ℂ H _ ((π g⁻¹ : H →L[ℂ] H) y) x := @@ -5729,12 +5726,12 @@ def normalFixedOrthogonalLinearIsometryEquiv (g : G) : left_inv x := by apply Subtype.ext change (↑(π g⁻¹ * π g) : H →L[ℂ] H) x = x - rw [← map_mul] + rw [← MonoidHom.map_mul] simp only [inv_mul_cancel, map_one, OneMemClass.coe_one, one_apply_eq_self] right_inv x := by apply Subtype.ext change (↑(π g * π g⁻¹) : H →L[ℂ] H) x = x - rw [← map_mul] + rw [← MonoidHom.map_mul] simp only [mul_inv_cancel, map_one, OneMemClass.coe_one, one_apply_eq_self] map_add' x y := Subtype.ext (map_add (π g : H →L[ℂ] H) (x : H) (y : H)) @@ -5763,7 +5760,7 @@ def normalFixedOrthogonalRepresentation : apply Subtype.ext change (π (g * h) : H →L[ℂ] H) (x : H) = (π g : H →L[ℂ] H) ((π h : H →L[ℂ] H) (x : H)) - rw [map_mul] + rw [MonoidHom.map_mul] rfl /-- Cross-module support for the infinite Connes-rigidity construction. -/ @@ -6083,7 +6080,7 @@ private theorem affineSubgroupOrbit_image · rintro ⟨_, ⟨k, rfl⟩, rfl⟩ refine ⟨n * k, ?_⟩ change α ((n : G) * (k : G)) x = α (n : G) (α (k : G) x) - rw [map_mul] + rw [MonoidHom.map_mul] rfl · rintro ⟨k, rfl⟩ let m : N := n⁻¹ * k @@ -6091,7 +6088,7 @@ private theorem affineSubgroupOrbit_image calc α (n : G) (α (m : G) x) = α ((n : G) * (m : G)) x := by - rw [map_mul] + rw [MonoidHom.map_mul] rfl _ = α (k : G) x := by congr 1 @@ -6198,7 +6195,7 @@ private def realInnerCharacter (f : G →* Multiplicative V) (v : V) : (Multiplicative.toAdd (f (g * h)))).re = (@inner ℂ V _ v (Multiplicative.toAdd (f g))).re + (@inner ℂ V _ v (Multiplicative.toAdd (f h))).re - rw [map_mul] + rw [MonoidHom.map_mul] change (@inner ℂ V _ v (Multiplicative.toAdd (f g) + Multiplicative.toAdd (f h))).re = _ rw [inner_add_right, Complex.add_re] @@ -6243,7 +6240,7 @@ private def affineInvariantProjectionHom (affineLinearRepresentation α)).starProjection (α g 0) + (normalFixedSubmodule (⊤ : Subgroup G) (affineLinearRepresentation α)).starProjection (α h 0) - rw [map_mul] + rw [MonoidHom.map_mul] have hact : α g (α h 0) = (affineLinearRepresentation α g : V →L[ℂ] V) (α h 0) + α g 0 := by @@ -6330,7 +6327,7 @@ def affineOrthogonalLinearHom change (affineLinearRepresentation α (g * h) : V →L[ℂ] V) x = (affineLinearRepresentation α g : V →L[ℂ] V) ((affineLinearRepresentation α h : V →L[ℂ] V) x) - rw [map_mul] + rw [MonoidHom.map_mul] rfl /-- Cross-module support for the infinite Connes-rigidity construction. -/ @@ -6346,7 +6343,7 @@ theorem affineOrthogonalTranslation_mul apply Subtype.ext change α (g * h) 0 = α g 0 + (affineLinearRepresentation α g : V →L[ℂ] V) (α h 0) - rw [map_mul] + rw [MonoidHom.map_mul] change α g (α h 0) = α g 0 + (affineLinearRepresentation α g : V →L[ℂ] V) (α h 0) have he := (α g).map_vsub (α h 0) 0 @@ -6534,7 +6531,7 @@ def diagonalLinearIsometryHom funext n change (π (g * h) : V →L[ℂ] V) (x n) = (π g : V →L[ℂ] V) ((π h : V →L[ℂ] V) (x n)) - rw [map_mul] + rw [MonoidHom.map_mul] rfl /-- Cross-module support for the infinite Connes-rigidity construction. -/ @@ -6568,7 +6565,7 @@ def diagonalAffineAction ((π h : V →L[ℂ] V) (x n) + ((π h : V →L[ℂ] V) (v n) - v n)) + ((π g : V →L[ℂ] V) (v n) - v n) - rw [map_mul] + rw [MonoidHom.map_mul] change (π g : V →L[ℂ] V) ((π h : V →L[ℂ] V) (x n)) + ((π g : V →L[ℂ] V) ((π h : V →L[ℂ] V) (v n)) - v n) = _ @@ -6977,7 +6974,7 @@ def rankTwoLinearAction (A : Type) [CommRing A] : change Matrix.SpecialLinearGroup.toLin' (g * h) (Multiplicative.toAdd v) = Matrix.SpecialLinearGroup.toLin' g (Matrix.SpecialLinearGroup.toLin' h (Multiplicative.toAdd v)) - rw [map_mul] + rw [MonoidHom.map_mul] rfl /-- Cross-module support for the infinite Connes-rigidity construction. -/ @@ -7791,7 +7788,7 @@ private theorem hasAffineGaussianRealization (Real.exp (-t * ‖α i x - α j x‖ ^ 2) : ℂ) have hd : ‖α (a * i) x - α (a * j) x‖ = ‖α i x - α j x‖ := by - rw [← dist_eq_norm, ← dist_eq_norm, map_mul, map_mul] + rw [← dist_eq_norm, ← dist_eq_norm, MonoidHom.map_mul, MonoidHom.map_mul] exact (α a).isometry.dist_eq (α i x) (α j x) rw [hd] let W := RKHS.OfKernel (CornulierUltralimit.scalarOperatorKernel K) @@ -7913,7 +7910,7 @@ private theorem unitary_displacement_mul_le ‖(π (g * h) : V →L[ℂ] V) ξ - ξ‖ ≤ ‖(π g : V →L[ℂ] V) ξ - ξ‖ + ‖(π h : V →L[ℂ] V) ξ - ξ‖ := by - rw [map_mul] + rw [MonoidHom.map_mul] change ‖(π g : V →L[ℂ] V) ((π h : V →L[ℂ] V) ξ) - ξ‖ ≤ _ calc @@ -8176,9 +8173,15 @@ private theorem rankTwoParabolicSpecialLinear_inr_root ElementaryRankTwoSemidirect A) k l = _ fin_cases i <;> fin_cases j <;> fin_cases k <;> fin_cases l <;> - simp_all [rankTwoParabolicMatrix, - Matrix.reindex_apply, Matrix.fromBlocks, elementaryRankTwoRoot, - Matrix.SpecialLinearGroup.transvection_coe] + simp_all only [rankTwoParabolicMatrix, Nat.reduceAdd, fromBlocks, elementaryRankTwoRoot, + Fin.zero_eta, Fin.isValue, SemidirectProduct.right_inr, + SpecialLinearGroup.transvection_coe, SemidirectProduct.left_inr, toAdd_one, + rankTwoColumnBlock_zero, reindex_apply, submatrix_apply, finTwoPlusTwo_symm_zero, of_apply, + Sum.elim_inl, Matrix.add_apply, one_apply_eq, single_apply_same, Fin.reduceCastAdd, + Fin.mk_one, finTwoPlusTwo_symm_one, ne_eq, zero_ne_one, not_false_eq_true, one_apply_ne, + and_false, single_apply_of_ne, add_zero, Fin.reduceFinMk, finTwoPlusTwo_symm_two, + Sum.elim_inr, Matrix.zero_apply, Fin.reduceEq, finTwoPlusTwo_symm_three, one_ne_zero, + and_true, and_self, zero_add] /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem rankTwoParabolicSpecialLinear_inr_mem_integral @@ -8218,7 +8221,7 @@ private theorem rankTwoParabolicSpecialLinear_inr_mem_integral elementaryRankTwo IntegralPolynomial) : ElementaryRankTwoSemidirect IntegralPolynomial) ∈ integralElementarySubgroup - rw [hxy, map_mul, map_mul] + rw [hxy, MonoidHom.map_mul, MonoidHom.map_mul] exact integralElementarySubgroup.mul_mem ihx ihy | inv x hx ihx => have hinv : @@ -8239,7 +8242,7 @@ public theorem rankTwoParabolicSpecialLinear_mem_integral (x : ElementaryRankTwoSemidirect IntegralPolynomial) : rankTwoParabolicSpecialLinear x ∈ integralElementarySubgroup := by - rw [← SemidirectProduct.inl_left_mul_inr_right x, map_mul] + rw [← SemidirectProduct.inl_left_mul_inr_right x, MonoidHom.map_mul] apply integralElementarySubgroup.mul_mem · have hleft := rankTwoParabolicSpecialLinear_inl (Multiplicative.toAdd x.left) @@ -8464,7 +8467,7 @@ private theorem integralRankTwoColumnEmbedding12_inl change integralElementaryReindexHom (Equiv.swap (0 : Index) 2) (integralRankTwoColumnEmbedding (SemidirectProduct.inl (Multiplicative.ofAdd v))) = _ - rw [integralRankTwoColumnEmbedding_inl, map_mul, + rw [integralRankTwoColumnEmbedding_inl, MonoidHom.map_mul, integralElementaryReindexHom_root, integralElementaryReindexHom_root] have hzero : (Equiv.swap (0 : Index) 2) 0 = 2 := by decide @@ -8483,7 +8486,7 @@ private theorem integralRankTwoRowEmbedding01_inl change integralElementaryTransposeInverseHom (integralRankTwoColumnEmbedding (SemidirectProduct.inl (Multiplicative.ofAdd v))) = _ - rw [integralRankTwoColumnEmbedding_inl, map_mul, + rw [integralRankTwoColumnEmbedding_inl, MonoidHom.map_mul, integralElementaryTransposeInverseHom_root, integralElementaryTransposeInverseHom_root] @@ -8498,7 +8501,7 @@ private theorem integralRankTwoRowEmbedding12_inl change integralElementaryTransposeInverseHom (integralRankTwoColumnEmbedding12 (SemidirectProduct.inl (Multiplicative.ofAdd v))) = _ - rw [integralRankTwoColumnEmbedding12_inl, map_mul, + rw [integralRankTwoColumnEmbedding12_inl, MonoidHom.map_mul, integralElementaryTransposeInverseHom_root, integralElementaryTransposeInverseHom_root] diff --git a/LeanPool/InfiniteConnesRigidity/UniversalLattice.lean b/LeanPool/InfiniteConnesRigidity/UniversalLattice.lean index fbd5bc3908..41c80d0115 100644 --- a/LeanPool/InfiniteConnesRigidity/UniversalLattice.lean +++ b/LeanPool/InfiniteConnesRigidity/UniversalLattice.lean @@ -163,12 +163,12 @@ def l2Reindex {α : Type u} {β : Type v} (e : α ≃ β) : { toFun := fun f ↦ ⟨(fun j : β ↦ f (e.symm j)), by change Memℓp (fun j : β ↦ f (e.symm j)) 2 rw [memℓp_gen_iff (by norm_num : 0 < (2 : ℝ≥0∞).toReal)] - exact (e.symm.summable_iff).2 + exact (e.symm.summable_iff (f := fun i ↦ ‖f i‖ ^ (2 : ℝ≥0∞).toReal)).2 ((lp.memℓp f).summable (by norm_num : 0 < (2 : ℝ≥0∞).toReal))⟩ invFun := fun f ↦ ⟨(fun j : α ↦ f (e j)), by change Memℓp (fun j : α ↦ f (e j)) 2 rw [memℓp_gen_iff (by norm_num : 0 < (2 : ℝ≥0∞).toReal)] - exact e.summable_iff.mpr + exact (e.summable_iff (f := fun i ↦ ‖f i‖ ^ (2 : ℝ≥0∞).toReal)).mpr ((lp.memℓp f).summable (by norm_num : 0 < (2 : ℝ≥0∞).toReal))⟩ left_inv := by intro f @@ -5763,8 +5763,9 @@ private def mennickeBlock (a b c d : R) (hdet : a * d - b * c = 1) : -/-- Cross-module support for the infinite Connes-rigidity construction. -/ -private theorem specialLinear_mul_transvection_apply +/-- Right multiplication by a transvection, entrywise. Shared by the block computations in +`CarryAndCrossedProduct` and `GroupConstruction`, so keep it exported. -/ +public theorem specialLinear_mul_transvection_apply {ι A : Type*} [Fintype ι] [DecidableEq ι] [CommRing A] (x : Matrix.SpecialLinearGroup ι A) {i j : ι} (hij : i ≠ j) (r : A) (a b : ι) : @@ -5777,6 +5778,20 @@ private theorem specialLinear_mul_transvection_apply exact Matrix.mul_transvection_apply_same (i := i) (j := j) a r x.val · exact Matrix.mul_transvection_apply_of_ne (i := i) (j := j) a b h r x.val +/-- Left multiplication by a transvection, entrywise. -/ +private theorem specialLinear_transvection_mul_apply + {ι A : Type*} [Fintype ι] [DecidableEq ι] [CommRing A] + (x : Matrix.SpecialLinearGroup ι A) {i j : ι} (hij : i ≠ j) + (r : A) (a b : ι) : + (Matrix.SpecialLinearGroup.transvection hij r * x) a b = + if a = i then x i b + r * x j b else x a b := by + rw [Matrix.SpecialLinearGroup.coe_mul, + Matrix.SpecialLinearGroup.transvection_coe] + split_ifs with h + · subst a + exact Matrix.transvection_mul_apply_same (i := i) (j := j) b r x.val + · exact Matrix.transvection_mul_apply_of_ne (i := i) (j := j) a b h r x.val + /-- Cross-module support for the infinite Connes-rigidity construction. -/ private def ContainsElementaryRoots (E : Subgroup (Matrix.SpecialLinearGroup (Fin 3) R)) : Prop := @@ -5840,28 +5855,42 @@ private theorem parkWoodburn_mennicke_identity have hw1 (i j : Fin 3) : w1 i j = !![1, 0, 0; -c * d, 1, 0; 0, 0, 1] i j := by dsimp only [w1] fin_cases i <;> fin_cases j <;> - simp [Matrix.SpecialLinearGroup.transvection_coe]; ring + simp only [Fin.isValue, Fin.zero_eta, SpecialLinearGroup.transvection_coe, + Matrix.add_apply, one_apply_eq, one_ne_zero, and_true, not_false_eq_true, + single_apply_of_ne, add_zero, neg_mul, of_apply, cons_val', cons_val_zero, + cons_val_fin_one, Fin.mk_one, Nat.reduceAdd, ne_eq, zero_ne_one, one_apply_ne, and_self, + cons_val_one, Fin.reduceFinMk, Fin.reduceEq, cons_val, single_apply_same, zero_add, + and_false]; ring let w2 := w1 * Matrix.SpecialLinearGroup.transvection (show (1 : Fin 3) ≠ 2 by decide) (a * d - 1) have hw2 (i j : Fin 3) : w2 i j = !![1, 0, 0; -c * d, 1, a * d - 1; 0, 0, 1] i j := by dsimp only [w2] rw [specialLinear_mul_transvection_apply] - fin_cases i <;> fin_cases j <;> simp [hw1] + fin_cases i <;> fin_cases j <;> + simp only [Fin.zero_eta, Fin.isValue, Fin.reduceEq, ↓reduceIte, hw1, neg_mul, of_apply, + cons_val', cons_val_zero, cons_val_fin_one, Fin.mk_one, cons_val_one, Fin.reduceFinMk, + cons_val, mul_zero, add_zero, mul_one, zero_add] let w3 := w2 * Matrix.SpecialLinearGroup.transvection (show (2 : Fin 3) ≠ 1 by decide) 1 have hw3 (i j : Fin 3) : w3 i j = !![1, 0, 0; -c * d, a * d, a * d - 1; 0, 1, 1] i j := by dsimp only [w3] rw [specialLinear_mul_transvection_apply] - fin_cases i <;> fin_cases j <;> simp [hw2] + fin_cases i <;> fin_cases j <;> + simp only [Fin.zero_eta, Fin.isValue, zero_ne_one, ↓reduceIte, hw2, neg_mul, of_apply, + cons_val', cons_val_zero, cons_val_fin_one, Fin.mk_one, cons_val_one, cons_val, mul_zero, + add_zero, Fin.reduceFinMk, Fin.reduceEq, one_mul, add_sub_cancel, mul_one, zero_add] let w4 := w3 * Matrix.SpecialLinearGroup.transvection (show (1 : Fin 3) ≠ 2 by decide) (-1) have hw4 (i j : Fin 3) : w4 i j = !![1, 0, 0; -c * d, a * d, -1; 0, 1, 0] i j := by dsimp only [w4] rw [specialLinear_mul_transvection_apply] - fin_cases i <;> fin_cases j <;> simp [hw3]; ring + fin_cases i <;> fin_cases j <;> + simp only [Fin.zero_eta, Fin.isValue, Fin.reduceEq, ↓reduceIte, hw3, neg_mul, of_apply, + cons_val', cons_val_zero, cons_val_fin_one, Fin.mk_one, cons_val_one, Fin.reduceFinMk, + cons_val, mul_zero, add_zero, one_mul, mul_one, add_neg_cancel]; ring let w5 := w4 * mennickeBlock a b c (ap * d) (mennicke_left_factor_det a ap b c d hdet) have hmiddleLeft : -(c * d * a) + a * d * c = 0 := by @@ -5873,29 +5902,42 @@ private theorem parkWoodburn_mennicke_identity dsimp only [w5] rw [Matrix.SpecialLinearGroup.coe_mul] fin_cases i <;> fin_cases j <;> - simp [Matrix.mul_apply, Fin.sum_univ_succ, mennickeBlock, hw4, - hmiddleLeft, hmiddleCenter] + simp only [mennickeBlock, Fin.zero_eta, Fin.isValue, Matrix.mul_apply, hw4, neg_mul, + of_apply, cons_val', cons_val_fin_one, cons_val_zero, Fin.sum_univ_succ, one_mul, + cons_val_succ, zero_mul, Finset.univ_unique, Fin.default_eq_zero, mul_zero, + Finset.sum_const_zero, add_zero, Fin.mk_one, cons_val_one, Fin.reduceFinMk, cons_val, + mul_one, hmiddleLeft, hmiddleCenter, Finset.sum_neg_distrib, Finset.sum_const, + Finset.card_singleton, one_smul, zero_add] let w6 := w5 * Matrix.SpecialLinearGroup.transvection (show (1 : Fin 3) ≠ 2 by decide) 1 have hw6 (i j : Fin 3) : w6 i j = !![a, b, b; 0, d, d - 1; c, ap * d, ap * d] i j := by dsimp only [w6] rw [specialLinear_mul_transvection_apply] - fin_cases i <;> fin_cases j <;> simp [hw5]; ring + fin_cases i <;> fin_cases j <;> + simp only [Fin.zero_eta, Fin.isValue, Fin.reduceEq, ↓reduceIte, hw5, of_apply, cons_val', + cons_val_zero, cons_val_fin_one, Fin.mk_one, cons_val_one, Fin.reduceFinMk, cons_val, + one_mul, zero_add]; ring let w7 := w6 * Matrix.SpecialLinearGroup.transvection (show (2 : Fin 3) ≠ 1 by decide) (-1) have hw7 (i j : Fin 3) : w7 i j = !![a, 0, b; 0, 1, d - 1; c, 0, ap * d] i j := by dsimp only [w7] rw [specialLinear_mul_transvection_apply] - fin_cases i <;> fin_cases j <;> simp [hw6] + fin_cases i <;> fin_cases j <;> + simp only [Fin.zero_eta, Fin.isValue, zero_ne_one, ↓reduceIte, hw6, of_apply, cons_val', + cons_val_zero, cons_val_fin_one, Fin.mk_one, cons_val_one, cons_val, neg_mul, one_mul, + add_neg_cancel, Fin.reduceFinMk, Fin.reduceEq, neg_sub, add_sub_cancel] let w8 := w7 * Matrix.SpecialLinearGroup.transvection (show (1 : Fin 3) ≠ 2 by decide) 1 have hw8 (i j : Fin 3) : w8 i j = !![a, 0, b; 0, 1, d; c, 0, ap * d] i j := by dsimp only [w8] rw [specialLinear_mul_transvection_apply] - fin_cases i <;> fin_cases j <;> simp [hw7] + fin_cases i <;> fin_cases j <;> + simp only [Fin.zero_eta, Fin.isValue, Fin.reduceEq, ↓reduceIte, hw7, of_apply, cons_val', + cons_val_zero, cons_val_fin_one, Fin.mk_one, cons_val_one, Fin.reduceFinMk, cons_val, + mul_zero, add_zero, mul_one, sub_add_cancel] let w9 := w8 * mennickeBlock ap b c (a * d) (mennicke_right_factor_det a ap b c d hdet) have hw9 (i j : Fin 3) : w9 i j = @@ -5903,7 +5945,11 @@ private theorem parkWoodburn_mennicke_identity dsimp only [w9] rw [Matrix.SpecialLinearGroup.coe_mul] fin_cases i <;> fin_cases j <;> - simp [Matrix.mul_apply, Fin.sum_univ_succ, mennickeBlock, hw8] <;> ring + simp only [mennickeBlock, Fin.zero_eta, Fin.isValue, Matrix.mul_apply, hw8, of_apply, + cons_val', cons_val_fin_one, cons_val_zero, Fin.sum_univ_succ, cons_val_succ, zero_mul, + Finset.univ_unique, Fin.default_eq_zero, mul_zero, Finset.sum_const_zero, add_zero, + Fin.mk_one, cons_val_one, Fin.reduceFinMk, cons_val, mul_one, Finset.sum_const, + Finset.card_singleton, one_smul, zero_add, one_mul] <;> ring let w10 := w9 * Matrix.SpecialLinearGroup.transvection (show (1 : Fin 3) ≠ 2 by decide) (-1) have hw10 (i j : Fin 3) : w10 i j = @@ -5911,7 +5957,10 @@ private theorem parkWoodburn_mennicke_identity ap * c, b * c, ap * d - b * c] i j := by dsimp only [w10] rw [specialLinear_mul_transvection_apply] - fin_cases i <;> fin_cases j <;> simp [hw9] <;> ring + fin_cases i <;> fin_cases j <;> + simp only [Fin.zero_eta, Fin.isValue, Fin.reduceEq, ↓reduceIte, hw9, of_apply, cons_val', + cons_val_zero, cons_val_fin_one, Fin.mk_one, cons_val_one, Fin.reduceFinMk, cons_val, + neg_mul, one_mul] <;> ring let w11 := w10 * Matrix.SpecialLinearGroup.transvection (show (2 : Fin 3) ≠ 1 by decide) 1 have hw11 (i j : Fin 3) : w11 i j = @@ -5919,7 +5968,10 @@ private theorem parkWoodburn_mennicke_identity ap * c, ap * d, ap * d - b * c] i j := by dsimp only [w11] rw [specialLinear_mul_transvection_apply] - fin_cases i <;> fin_cases j <;> simp [hw10] + fin_cases i <;> fin_cases j <;> + simp only [Fin.zero_eta, Fin.isValue, zero_ne_one, ↓reduceIte, hw10, of_apply, cons_val', + cons_val_zero, cons_val_fin_one, Fin.mk_one, cons_val_one, cons_val, one_mul, + add_sub_cancel, Fin.reduceFinMk, Fin.reduceEq] let w12 := w11 * Matrix.SpecialLinearGroup.transvection (show (1 : Fin 3) ≠ 2 by decide) (a - 1) have htopRight : b - a * b + (a - 1) * b = 0 := by @@ -5933,21 +5985,29 @@ private theorem parkWoodburn_mennicke_identity dsimp only [w12] rw [specialLinear_mul_transvection_apply] fin_cases i <;> fin_cases j <;> - simp [hw11, htopRight, hmiddleRight, hbottomRight] + simp only [Fin.zero_eta, Fin.isValue, Fin.reduceEq, ↓reduceIte, hw11, of_apply, cons_val', + cons_val_zero, cons_val_fin_one, Fin.mk_one, cons_val_one, Fin.reduceFinMk, cons_val, + htopRight, hmiddleRight, hbottomRight] let w13 := w12 * Matrix.SpecialLinearGroup.transvection (show (2 : Fin 3) ≠ 0 by decide) (-ap * c) have hw13 (i j : Fin 3) : w13 i j = !![a * ap, b, 0; c, d, 0; 0, ap * d, 1] i j := by dsimp only [w13] rw [specialLinear_mul_transvection_apply] - fin_cases i <;> fin_cases j <;> simp [hw12] + fin_cases i <;> fin_cases j <;> + simp only [Fin.zero_eta, Fin.isValue, ↓reduceIte, hw12, of_apply, cons_val', cons_val_zero, + cons_val_fin_one, neg_mul, cons_val, mul_zero, add_zero, Fin.mk_one, one_ne_zero, + cons_val_one, Fin.reduceFinMk, Fin.reduceEq, mul_one, add_neg_cancel] let w14 := w13 * Matrix.SpecialLinearGroup.transvection (show (2 : Fin 3) ≠ 1 by decide) (-(ap * d)) have hw14 (i j : Fin 3) : w14 i j = !![a * ap, b, 0; c, d, 0; 0, 0, 1] i j := by dsimp only [w14] rw [specialLinear_mul_transvection_apply] - fin_cases i <;> fin_cases j <;> simp [hw13] + fin_cases i <;> fin_cases j <;> + simp only [Fin.zero_eta, Fin.isValue, zero_ne_one, ↓reduceIte, hw13, of_apply, cons_val', + cons_val_zero, cons_val_fin_one, Fin.mk_one, cons_val_one, cons_val, mul_zero, add_zero, + Fin.reduceFinMk, Fin.reduceEq, mul_one, add_neg_cancel] change mennickeBlock (a * ap) b c d hdet = w14 apply Matrix.SpecialLinearGroup.ext intro i j @@ -6025,13 +6085,14 @@ private theorem mennickeBlock_rotation_conjugate Matrix.SpecialLinearGroup.transvection_inv] apply Matrix.SpecialLinearGroup.ext intro i j - have hmul (x y : Matrix.SpecialLinearGroup (Fin 3) R) (p q : Fin 3) : - (x * y) p q = ∑ k, x p k * y k q := rfl - simp_rw [hmul] fin_cases i <;> fin_cases j <;> - simp [mennickeBlock, - Fin.sum_univ_succ, Matrix.SpecialLinearGroup.transvection_coe, - Matrix.one_apply, Matrix.single_apply] + simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, ← mul_assoc, + specialLinear_mul_transvection_apply, Fin.reduceEq, ↓reduceIte] <;> + simp only [mul_assoc] <;> + simp only [specialLinear_transvection_mul_apply, Fin.isValue, Fin.reduceEq, ↓reduceIte] <;> + simp only [mennickeBlock, Matrix.of_apply, Matrix.cons_val', Matrix.cons_val_zero, + Matrix.cons_val_one, Matrix.cons_val_fin_one, Matrix.cons_val] <;> + ring /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem mennicke_swapped_left_factor_det @@ -6397,17 +6458,12 @@ private theorem unitEntry_diagonalUnitPair_apply if i = 0 then (a : R) else if i = 1 then (↑a⁻¹ : R) else 1 else 0 := by fin_cases i <;> fin_cases j <;> - simp only [unitEntry_diagonalUnitPair, Fin.isValue, Nat.reduceAdd, - Fin.zero_eta, Matrix.SpecialLinearGroup.coe_mul, - Matrix.SpecialLinearGroup.transvection_coe, Matrix.mul_apply, - Matrix.add_apply, Matrix.one_apply, Matrix.single_apply, true_and, - Fin.sum_univ_three, ↓reduceIte, one_ne_zero, add_zero, false_and, - mul_ite, mul_one, mul_zero, zero_ne_one, zero_add, Fin.reduceEq, - ite_self, mul_neg, Units.mul_inv, add_neg_cancel, zero_mul, ite_mul, - Finset.sum_ite_eq, Finset.mem_univ, and_false, - Finset.sum_ite_eq', Fin.mk_one, and_true, - neg_add_cancel, Fin.reduceFinMk, one_mul, neg_mul, Units.inv_mul, - neg_zero, Finset.sum_neg_distrib, neg_add_rev, neg_neg] + simp only [unitEntry_diagonalUnitPair, Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + MennickeIdentity.specialLinear_mul_transvection_apply, Fin.reduceEq, ↓reduceIte, + Matrix.SpecialLinearGroup.transvection_coe, Matrix.add_apply, Matrix.one_apply, + Matrix.single_apply, one_ne_zero, zero_ne_one, and_self, and_false, and_true, mul_one, + mul_zero, add_zero, zero_add, one_mul, mul_neg, neg_mul, neg_neg, + Units.mul_inv, Units.inv_mul, add_neg_cancel, neg_add_cancel] /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem stabilizedTwoByTwo_mem_elementaryThree_of_topLeft_isUnit @@ -6498,35 +6554,29 @@ private theorem mennickeBlock_mem_of_isUnit_topRight have hJ : J ∈ E := MennickeIdentity.mennickeRotation_mem E hroot have hrow : ∀ j : Fin 3, (B * J) 2 j = if j = 2 then 1 else 0 := by intro j - rw [Matrix.SpecialLinearGroup.coe_mul] fin_cases j <;> - simp [B, J, MennickeIdentity.mennickeBlock, - MennickeIdentity.mennickeRotation, - Matrix.SpecialLinearGroup.coe_mul, - Matrix.SpecialLinearGroup.transvection_coe, - Matrix.mul_apply, Fin.sum_univ_succ, - Matrix.single_apply, Matrix.one_apply] + simp only [B, J, MennickeIdentity.mennickeRotation, ← mul_assoc] <;> + simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + MennickeIdentity.specialLinear_mul_transvection_apply, Fin.reduceEq, ↓reduceIte] <;> + simp only [MennickeIdentity.mennickeBlock, Matrix.of_apply, Matrix.cons_val', + Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one, Matrix.cons_val, + mul_zero, add_zero] have hcolumn : ∀ i : Fin 3, (B * J) i 2 = if i = 2 then 1 else 0 := by intro i - rw [Matrix.SpecialLinearGroup.coe_mul] fin_cases i <;> - simp [B, J, MennickeIdentity.mennickeBlock, - MennickeIdentity.mennickeRotation, - Matrix.SpecialLinearGroup.coe_mul, - Matrix.SpecialLinearGroup.transvection_coe, - Matrix.mul_apply, Fin.sum_univ_succ, - Matrix.single_apply, Matrix.one_apply] + simp only [B, J, MennickeIdentity.mennickeRotation, ← mul_assoc] <;> + simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + MennickeIdentity.specialLinear_mul_transvection_apply, Fin.reduceEq, ↓reduceIte] <;> + simp only [MennickeIdentity.mennickeBlock, Matrix.of_apply, Matrix.cons_val', + Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one, Matrix.cons_val] have htop : IsUnit ((B * J) 0 0) := by have hentry : (B * J) 0 0 = -b := by - rw [Matrix.SpecialLinearGroup.coe_mul] - simp only [MennickeIdentity.mennickeBlock, MennickeIdentity.mennickeRotation, Fin.isValue, - Matrix.SpecialLinearGroup.coe_mul, SpecialLinearGroup.transvection_coe, Matrix.mul_apply, - of_apply, cons_val', cons_val_fin_one, cons_val_zero, Matrix.add_apply, Matrix.one_apply, - single_apply, Fin.sum_univ_succ, one_ne_zero, and_false, ↓reduceIte, add_zero, false_and, - mul_ite, mul_one, mul_zero, Fin.succ_zero_eq_one, and_true, true_and, Finset.univ_unique, - Fin.default_eq_zero, Finset.sum_singleton, Fin.succ_one_eq_two, Fin.reduceEq, - Finset.sum_ite_eq', Finset.mem_univ, zero_add, mul_neg, neg_add_rev, zero_ne_one, neg_zero, - add_neg_cancel, cons_val_succ, Fin.succ_ne_zero, zero_mul, Finset.sum_const_zero, B, J] + simp only [B, J, MennickeIdentity.mennickeRotation, ← mul_assoc] + simp only [Fin.isValue, MennickeIdentity.specialLinear_mul_transvection_apply, Fin.reduceEq, + ↓reduceIte] + simp only [MennickeIdentity.mennickeBlock, Matrix.of_apply, Matrix.cons_val', + Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one] + ring rw [hentry] exact hb.neg have hBJ : B * J ∈ E := @@ -6581,15 +6631,14 @@ private theorem mennickeBlock_X_constant_shear_mul mennickeBlock a g p X hdet := by apply Matrix.SpecialLinearGroup.ext intro i j - rw [Matrix.SpecialLinearGroup.coe_mul] fin_cases i <;> fin_cases j <;> - simp [mennickeBlock, - Matrix.SpecialLinearGroup.transvection_coe, - Matrix.mul_apply, Fin.sum_univ_succ, - Matrix.one_apply, Matrix.single_apply] - · ring - · have hdivide := Polynomial.divX_mul_X_add g - linear_combination hdivide + simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + MennickeIdentity.specialLinear_transvection_mul_apply, Fin.reduceEq, ↓reduceIte] <;> + simp only [MennickeIdentity.mennickeBlock, Matrix.of_apply, Matrix.cons_val', + Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one, Matrix.cons_val] <;> + first + | ring1 + | linear_combination Polynomial.divX_mul_X_add g /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem mennickeBlock_X_mem @@ -6983,12 +7032,12 @@ private theorem suslin_uniformizer_column_shear dsimp apply Matrix.SpecialLinearGroup.ext intro i j - rw [Matrix.SpecialLinearGroup.coe_mul] fin_cases i <;> fin_cases j <;> - simp [mennickeBlock, - Matrix.SpecialLinearGroup.transvection_coe, - Matrix.mul_apply, Fin.sum_univ_succ, Matrix.one_apply, - Matrix.single_apply] <;> ring + simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + MennickeIdentity.specialLinear_mul_transvection_apply, Fin.reduceEq, ↓reduceIte] <;> + simp only [MennickeIdentity.mennickeBlock, Matrix.of_apply, Matrix.cons_val', + Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one, Matrix.cons_val] <;> + ring /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem suslin_uniformizer_mennickeBlock_mem_elementary @@ -7217,8 +7266,8 @@ private theorem polynomial_valuation_coefficient_ascent (hunit : IsUnit (f.coeff m)) (hc : ¬ IsUnit c) (hlead : f.leadingCoeff = c * g.leadingCoeff) : - let s := g.natDegree - f.natDegree - let f' := X ^ s * f - C c * g + let s : ℕ := g.natDegree - f.natDegree + let f' : Polynomial A := X ^ s * f - C c * g f'.natDegree < g.natDegree ∧ IsUnit (f'.coeff (s + m)) ∧ m < s + m := by dsimp @@ -7399,12 +7448,12 @@ private theorem mennickeBlock_rowSecond_sub_mul mennickeBlock a b c d hdet := by apply Matrix.SpecialLinearGroup.ext intro i j - rw [Matrix.SpecialLinearGroup.coe_mul] fin_cases i <;> fin_cases j <;> - simp [mennickeBlock, - Matrix.SpecialLinearGroup.transvection_coe, - Matrix.mul_apply, Fin.sum_univ_succ, Matrix.one_apply, - Matrix.single_apply] <;> ring + simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + MennickeIdentity.specialLinear_transvection_mul_apply, Fin.reduceEq, ↓reduceIte] <;> + simp only [MennickeIdentity.mennickeBlock, Matrix.of_apply, Matrix.cons_val', + Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one, Matrix.cons_val] <;> + ring /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem mennickeBlock_columnFirst_sub_mul @@ -7416,12 +7465,12 @@ private theorem mennickeBlock_columnFirst_sub_mul (show (1 : Fin 3) ≠ 0 by decide) (-q) := by apply Matrix.SpecialLinearGroup.ext intro i j - rw [Matrix.SpecialLinearGroup.coe_mul] fin_cases i <;> fin_cases j <;> - simp [mennickeBlock, - Matrix.SpecialLinearGroup.transvection_coe, - Matrix.mul_apply, Fin.sum_univ_succ, Matrix.one_apply, - Matrix.single_apply] <;> ring + simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + MennickeIdentity.specialLinear_mul_transvection_apply, Fin.reduceEq, ↓reduceIte] <;> + simp only [MennickeIdentity.mennickeBlock, Matrix.of_apply, Matrix.cons_val', + Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one, Matrix.cons_val] <;> + ring /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem elementaryThree_contains_roots : @@ -7871,12 +7920,12 @@ private theorem mennickeBlock_mul_columnSubtract (mennickeBlock_columnSubtract_det f g p q t hdet) := by apply Matrix.SpecialLinearGroup.ext intro i j - rw [Matrix.SpecialLinearGroup.coe_mul] fin_cases i <;> fin_cases j <;> - simp [mennickeBlock, - Matrix.mul_apply, Fin.sum_univ_succ, - Matrix.SpecialLinearGroup.transvection_coe, - Matrix.one_apply, Matrix.single_apply] <;> ring + simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + MennickeIdentity.specialLinear_mul_transvection_apply, Fin.reduceEq, ↓reduceIte] <;> + simp only [MennickeIdentity.mennickeBlock, Matrix.of_apply, Matrix.cons_val', + Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one, Matrix.cons_val] <;> + ring /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem mennickeBlock_columnSubtract_mem_iff @@ -8995,15 +9044,11 @@ theorem upperUnitriangular_factorization (g : IGroup) apply Matrix.SpecialLinearGroup.ext intro i j fin_cases i <;> fin_cases j <;> - simp only [Nat.reduceAdd, Fin.zero_eta, Fin.isValue, Fin.mk_one, - Fin.reduceFinMk, Matrix.SpecialLinearGroup.coe_mul, - Matrix.SpecialLinearGroup.transvection_coe, Matrix.mul_apply, - Matrix.add_apply, Matrix.one_apply, Fin.reduceEq, false_and, - not_false_eq_true, Matrix.single_apply_of_ne, add_zero, - Matrix.single_apply, ite_mul, one_mul, zero_mul, Finset.sum_ite_eq, - Finset.mem_univ, ↓reduceIte, one_ne_zero, true_and, - Fin.sum_univ_four, zero_ne_one, mul_ite, mul_one, mul_zero, - ite_self, zero_add, and_false, Finset.sum_ite_eq', and_true, + simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + MennickeIdentity.specialLinear_mul_transvection_apply, Fin.reduceEq, ↓reduceIte, + Matrix.SpecialLinearGroup.transvection_coe, Matrix.add_apply, Matrix.one_apply, + Matrix.single_apply, one_ne_zero, zero_ne_one, and_self, and_false, and_true, + mul_one, mul_zero, add_zero, zero_add, h00, h11, h22, h33, h10, h20, h21, h30, h31, h32] /-- Cross-module support for the infinite Connes-rigidity construction. -/