diff --git a/LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean b/LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean index e4cc49aed5..d809f29557 100644 --- a/LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean +++ b/LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean @@ -435,7 +435,7 @@ private theorem subgroup_mem_of_powered_partition_patches rw [List.mem_reverse, List.mem_map] at hx obtain ⟨j, hj, rfl⟩ := hx have hjn : j < n := List.mem_range.mp hj - simpa [f, suslinPoweredPrefix_succ] using hpatch j hjn + simpa only [f, suslinPoweredPrefix_succ] using hpatch j hjn dsimp [f] at htel rw [hend, suslinPoweredPrefix_zero, hzero, inv_one, mul_one] at htel rw [← htel] @@ -1340,7 +1340,8 @@ private theorem suslinSymbolicPoweredIncrement_of_elementary_dilation (Matrix.SpecialLinearGroup.map (Polynomial.mapRingHom f) (suslinDifferencePath (Polynomial.X : Polynomial ℤ) (suslinSymbolicLift g))) at h - simpa [f, suslinSymbolicDifference_eval] using h + simpa only [f, suslinSymbolicDifference_eval, eq_intCast, Int.cast_pow, map_pow, map_intCast, + coe_mapRingHom, Polynomial.map_pow, Polynomial.map_intCast] using h have heval : Matrix.SpecialLinearGroup.map r (suslinDilation (Polynomial (Polynomial ℤ)) @@ -1455,15 +1456,12 @@ private theorem suslin_uniform_symbolic_differencePath_elementary (Polynomial.mapRingHom (Polynomial.C : L →+* B₁)) (Matrix.SpecialLinearGroup.map (Polynomial.mapRingHom f) g) := by - apply Matrix.SpecialLinearGroup.ext - intro i j - change - Polynomial.map f₁ - (Polynomial.map (Polynomial.C : ℤ →+* A₁) (g i j)) = - Polynomial.map (Polynomial.C : L →+* B₁) - (Polynomial.map f (g i j)) - ext n - simp only [coeff_map, eq_intCast, map_intCast, f₁] + change Matrix.SpecialLinearGroup.map + ((Polynomial.mapRingHom (Polynomial.mapRingHom f)).comp + (Polynomial.mapRingHom Polynomial.C)) g = + Matrix.SpecialLinearGroup.map + ((Polynomial.mapRingHom Polynomial.C).comp (Polynomial.mapRingHom f)) g + rw [Polynomial.mapRingHom_comp, Polynomial.mapRingHom_comp, Polynomial.mapRingHom_comp_C] have hgT : Matrix.SpecialLinearGroup.map (Polynomial.mapRingHom f₁) gT ∈ localGlobalElementarySubgroup (Polynomial B₁) := by @@ -1569,7 +1567,7 @@ private theorem suslin_augmentation_mem_elementary_of_finite_away_powered_increm (fun i _ => Nat.zero_le (exponent i)) (Finset.mem_univ d) have hrange : Set.range (fun d : s => (d : ℤ)) = (s : Set ℤ) := by ext d - simp + simp only [Subtype.range_coe_subtype, SetLike.setOfPred_mem_eq, SetLike.mem_coe] have hcover : Ideal.span (Set.range (fun d : s => (d : ℤ))) = ⊤ := by rw [hrange] exact hspan @@ -1600,7 +1598,7 @@ private theorem suslin_augmentation_mem_elementary_of_finite_away_powered_increm rw [← pow_add, Nat.sub_add_cancel (hle d)] have h := hexponent d a (coefficient d * (d : ℤ) ^ (N - exponent d)) - simpa [c, denominator, d, hpow, mul_assoc] using h + simpa only [c, denominator, d, hpow, mul_assoc] using h let sn : ℕ → ℤ := fun j => if h : j < Fintype.card s then denominator ⟨j, h⟩ else 0 let cn : ℕ → ℤ := fun j => @@ -1922,8 +1920,10 @@ private theorem cornulierColumnRootProduct_apply (v : Index → IntegralPolynomi Matrix.SpecialLinearGroup.transvection (show (2 : Index) ≠ cornulierLast by decide) (v 2) : IntegralSpecialLinearGroup) p q = _ - fin_cases p <;> fin_cases q <;> - simp only [cornulierLast, Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + revert p q + refine matrix_four_entrywise _ _ + ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ <;> + simp only [cornulierLast, Fin.isValue, ConnesRigidity.MennickeIdentity.specialLinear_mul_transvection_apply, Fin.reduceEq, ↓reduceIte, Matrix.SpecialLinearGroup.transvection_coe, Matrix.add_apply, Matrix.one_apply, @@ -1962,8 +1962,10 @@ private theorem cornulierRowRootProduct_apply (v : Index → IntegralPolynomial) Matrix.SpecialLinearGroup.transvection (show cornulierLast ≠ (2 : Index) by decide) (v 2) : IntegralSpecialLinearGroup) p q = _ - fin_cases p <;> fin_cases q <;> - simp only [cornulierLast, Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + revert p q + refine matrix_four_entrywise _ _ + ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ <;> + simp only [cornulierLast, Fin.isValue, ConnesRigidity.MennickeIdentity.specialLinear_mul_transvection_apply, Fin.reduceEq, ↓reduceIte, Matrix.SpecialLinearGroup.transvection_coe, Matrix.add_apply, Matrix.one_apply, @@ -2312,7 +2314,8 @@ private theorem minkowski_prime_three_matrix have hthreeScalar : (3 : ZMod 3) = 0 := ZMod.natCast_self 3 ext i j by_cases hij : i = j <;> - simp [Matrix.ofNat_apply, hij, hthreeScalar] + simp only [Matrix.ofNat_apply, hij, hthreeScalar, ↓reduceIte, Nat.cast_ofNat, + Matrix.zero_apply, Nat.cast_zero] dsimp [T] rw [zsmul_eq_mul, zsmul_eq_mul] simp only [map_add, map_mul, map_intCast, map_one] @@ -2689,22 +2692,20 @@ private theorem carry_add_right (ℓ ℓ₁ ℓ₂ : X) : +/-- Cross-module support for the infinite Connes-rigidity construction. -/ +public +theorem linearMap_ext_on_diagonal {W : Type*} + [AddCommGroup W] [Module F W] {f g : B →ₗ[F] W} + (h : ∀ v : V, f (diagonal v) = g (diagonal v)) : f = g := by + apply LinearMap.ext_on_range (v := diagonal) ?_ h + exact (Submodule.span_range_subtype_eq_top_iff B + (fun v => Submodule.subset_span (Set.mem_range_self v))).mpr rfl + /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem carry_comm (ℓ ℓ' : X) : carry ℓ ℓ' = carry ℓ' ℓ := by - apply LinearMap.ext - rintro ⟨w, hw⟩ - change tensorFunctional ℓ ℓ' w = tensorFunctional ℓ' ℓ w - change w ∈ Submodule.span F (Set.range square) at hw - refine Submodule.span_induction - (p := fun z _ => tensorFunctional ℓ ℓ' z = tensorFunctional ℓ' ℓ z) - ?_ ?_ ?_ ?_ hw - · rintro _ ⟨v, rfl⟩ - simp only [square, tensorFunctional_tmul, mul_comm] - · simp only [map_zero] - · intro u v _ _ hu hv - simp only [map_add, hu, hv] - · intro a v _ hv - simp only [map_smul, hv] + apply linearMap_ext_on_diagonal + intro v + exact mul_comm (ℓ v) (ℓ' v) /-- Cross-module support for the infinite Connes-rigidity construction. -/ @[expose] @@ -4438,33 +4439,6 @@ theorem d_surjective : Function.Surjective d := by intro v exact ⟨diagonal v, d_diagonal v⟩ -/-- Cross-module support for the infinite Connes-rigidity construction. -/ -public -theorem linearMap_ext_on_diagonal {W : Type*} - [AddCommGroup W] [Module F W] {f g : B →ₗ[F] W} - (h : ∀ v : V, f (diagonal v) = g (diagonal v)) : f = g := by - apply LinearMap.ext - intro w - rcases w with ⟨w, hw⟩ - change f ⟨w, hw⟩ = g ⟨w, hw⟩ - change w ∈ Submodule.span F (Set.range square) at hw - induction hw using Submodule.span_induction with - | mem w hw => - rcases hw with ⟨v, rfl⟩ - exact h v - | zero => - change f 0 = g 0 - simp only [map_zero] - | add x y hx hy ihx ihy => - change f (⟨x, hx⟩ + ⟨y, hy⟩) = g (⟨x, hx⟩ + ⟨y, hy⟩) - simpa only [map_add] using congrArg₂ (· + ·) ihx ihy - | smul c x hx ih => - change f (c • (⟨x, hx⟩ : B)) = g (c • (⟨x, hx⟩ : B)) - simpa only [map_smul] using congrArg (c • ·) ih - -end - -section /-- Cross-module support for the infinite Connes-rigidity construction. -/ @[expose] @@ -4820,7 +4794,10 @@ private theorem evalEta_eq_kernelCharacter_linear {n : ℕ} (η : E n) kernelCharacter n η h (Multiplicative.ofAdd z.linear) := by have hdecomp : z = linearSection n z.linear + carryKernelInclusion n z.quadratic := by - apply CarryGroup.ext <;> simp + apply CarryGroup.ext <;> simp only [CarryGroup.add_linear, linearSection_linear, + carryKernelInclusion_linear, add_zero, CarryGroup.add_quadratic, + linearSection_quadratic, carryKernelInclusion_quadratic, zero_add, + shiftedCarry_zero_right] conv_lhs => rw [hdecomp] rw [evalEta_add, evalEta_kernel η h, mul_one] rfl @@ -5681,7 +5658,9 @@ private theorem evaluation_surjective (n : ℕ) : intro η let η' : E n := Multiplicative.toAdd η have hdecomp : z = linearCandidate n φ + carryKernelInclusion n q := by - apply CarryGroup.ext <;> simp [z, l, q, linearCandidate] + apply CarryGroup.ext <;> simp only [z, l, q, linearCandidate, CarryGroup.add_linear, + carryKernelInclusion_linear, add_zero, CarryGroup.add_quadratic, + carryKernelInclusion_quadratic, zero_add, shiftedCarry_zero_right] change evalEta η' z = φ η rw [hdecomp, evalEta_add] have hquad : evalEta η' (carryKernelInclusion n q) = @@ -7466,12 +7445,8 @@ theorem crossedHaarHilbertEquiv_group_conj (crossedHaarHilbertEquiv e).conjStarAlgEquiv (crossedGroupUnitary X k).toContinuousLinearEquiv.toContinuousLinearMap = (crossedGroupUnitary Y k).toContinuousLinearEquiv.toContinuousLinearMap := by - apply ContinuousLinearMap.ext - intro η - obtain ⟨ξ, rfl⟩ := (crossedHaarHilbertEquiv e).surjective η - simpa only [LinearIsometryEquiv.conjStarAlgEquiv_apply_apply, - LinearIsometryEquiv.symm_apply_apply, ContinuousLinearEquiv.coe_coe, - LinearIsometryEquiv.coe_toContinuousLinearEquiv] using crossedHaarHilbertEquiv_group_apply e k ξ + apply conjStarAlgEquiv_eq_of_intertwining + exact crossedHaarHilbertEquiv_group_apply e k end @@ -7740,29 +7715,16 @@ private theorem carryFourier_kEAction_comp (n : ℕ) (k : K) have hmaps : F.comp R = P.comp F := by apply lp.ext_continuousLinearMap (by norm_num) intro η - apply ContinuousLinearMap.ext - intro c + apply ContinuousLinearMap.ext_ring change carryFourierEquiv n - (l2Reindex (carryEAddAction n k).toEquiv (lp.single 2 η c)) = + (l2Reindex (carryEAddAction n k).toEquiv (lp.single 2 η (1 : ℂ))) = Lp.compMeasurePreserving (kCarryAddAut n k⁻¹ : CarryGroup n → CarryGroup n) (paperCarryAddAut_preserves_measure n k⁻¹) - (carryFourierEquiv n (lp.single 2 η c)) - have hsingle : (lp.single 2 η c : GroupL2 (E n)) = - c • (lp.single 2 η (1 : ℂ) : GroupL2 (E n)) := by - simpa only [smul_eq_mul, mul_one] using (lp.single_smul (E := fun _ : E n => ℂ) 2 η c (1 : ℂ)) - rw [hsingle] - simp only [map_smul] - rw [carry_l2Reindex_single, carryFourierEquiv_single, - carryFourierEquiv_single] - change c • carryCharacterL2 n (carryEAddAction n k η) = - (Lp.compMeasurePreservingₗ ℂ - (kCarryAddAut n k⁻¹ : CarryGroup n → CarryGroup n) - (paperCarryAddAut_preserves_measure n k⁻¹)) - (c • carryCharacterL2 n η) - rw [map_smul] - exact congrArg (c • ·) (carryCharacterL2_kEAction n k η) + (carryFourierEquiv n (lp.single 2 η (1 : ℂ))) + rw [carry_l2Reindex_single, carryFourierEquiv_single, carryFourierEquiv_single] + exact carryCharacterL2_kEAction n k η exact DFunLike.congr_fun hmaps ξ /-- Cross-module support for the infinite Connes-rigidity construction. -/ @@ -7967,7 +7929,8 @@ private theorem continuous_sub_unit_multiplier_on_continuous_norm_le unitMultiplier μ u hu hunit ((ContinuousMap.toLp 2 μ ℂ) h) x‖ ≤ ‖h‖ * ‖((ContinuousMap.toLp 2 μ ℂ) q) x - unitFunctionL2 μ u hu hunit x‖ rw [hqmul, humul, hqcoe, hhcoe, hucoe, ← sub_mul, norm_mul] - nlinarith [ContinuousMap.norm_coe_le_norm h x, norm_nonneg (q x - u x)] + exact (mul_le_mul_of_nonneg_left (ContinuousMap.norm_coe_le_norm h x) + (norm_nonneg (q x - u x))).trans_eq (mul_comm _ _) omit [T2Space Ω] [SecondCountableTopology Ω] [μ.WeaklyRegular] in /-- Cross-module support for the infinite Connes-rigidity construction. -/ @@ -8117,20 +8080,11 @@ private theorem commute_continuousMultiplier_of_commute_characters (continuousMultiplier μ) have hspan : Dense (↑(Submodule.span ℂ (Set.range χ)) : Set C(Ω, ℂ)) := Submodule.dense_iff_topologicalClosure_eq_top.mpr hdense - have heq : - (leftMap : C(Ω, ℂ) → (Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ)) = rightMap := by - apply Continuous.ext_on hspan leftMap.continuous rightMap.continuous - intro q hq - refine Submodule.span_induction - (p := fun q _ => leftMap q = rightMap q) ?_ ?_ ?_ ?_ hq - · rintro _ ⟨i, rfl⟩ - exact (hT i).eq - · exact (map_zero leftMap).trans (map_zero rightMap).symm - · intro f g _ _ hf hg - rw [map_add, map_add, hf, hg] - · intro c f _ hf - rw [map_smul, map_smul, hf] - exact congrFun heq q + have heq : leftMap = rightMap := by + apply ContinuousLinearMap.ext_on hspan + rintro _ ⟨i, rfl⟩ + exact (hT i).eq + exact DFunLike.congr_fun heq q /-- Cross-module support for the infinite Connes-rigidity construction. -/ public @@ -8220,14 +8174,24 @@ private theorem norm_realUnit {x : ℝ} (hx : |x| ≤ 1) : /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem realUnit_add_conj (x : ℝ) : realUnit x + starRingEnd ℂ (realUnit x) = 2 * (x : ℂ) := by - apply Complex.ext <;> simp [realUnit]; ring + apply Complex.ext <;> simp only [realUnit, map_add, Complex.conj_ofReal, map_mul, + Complex.conj_I, neg_mul, Complex.add_re, Complex.ofReal_re, + Complex.mul_re, Complex.I_re, zero_mul, Complex.I_im, Complex.ofReal_im, + mul_zero, sub_self, add_zero, Complex.neg_re, neg_zero, + Complex.re_ofNat, Complex.im_ofNat, sub_zero, Complex.add_im, + Complex.mul_im, one_mul, zero_add, Complex.neg_im, add_neg_cancel]; ring /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem complex_four_unit_decomposition {z : ℂ} : z = (realUnit z.re + starRingEnd ℂ (realUnit z.re)) / 2 + Complex.I * (realUnit z.im + starRingEnd ℂ (realUnit z.im)) / 2 := by rw [realUnit_add_conj, realUnit_add_conj] - apply Complex.ext <;> simp + apply Complex.ext <;> simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, + mul_div_cancel_left₀, Complex.add_re, Complex.ofReal_re, + Complex.div_ofNat_re, Complex.mul_re, Complex.I_re, Complex.re_ofNat, + Complex.im_ofNat, Complex.ofReal_im, mul_zero, sub_zero, zero_mul, + Complex.I_im, Complex.mul_im, add_zero, sub_self, zero_div, + Complex.add_im, Complex.div_ofNat_im, one_mul, zero_add] variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} diff --git a/LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean b/LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean index 26c787eaa6..c66d80afec 100644 --- a/LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean +++ b/LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean @@ -7,11 +7,6 @@ Authors: OpenAI, Dean Cureton module import Mathlib.Algebra.Order.Star.Real -import Mathlib.RingTheory.WittVector.IsPoly -import Mathlib.Tactic.ENatToNat -import Mathlib.Tactic.Polynomial.Basic -import Mathlib.Tactic.ReduceModChar -import Std.Tactic.BVDecide.Normalize.Prop public import LeanPool.InfiniteConnesRigidity.SpectralAndPropertyT import LeanPool.InfiniteConnesRigidity.GroupConstruction @@ -1249,6 +1244,18 @@ private theorem semidirectIntrinsicSubquotientEquiv_mk_inclusion rw [← hmk, quotientEquiv.symm_apply_apply] exact multiplicativeTwoTorsionQuotientEquiv_mk hfour x +/-- Conjugation of the abelian normal factor depends only on the quotient coordinate. -/ +private theorem semidirect_conj_inl_commutative {N H : Type*} [CommGroup N] [Group H] + (φ : H →* MulAut N) (g : SemidirectProduct N H φ) (n : N) : + g * SemidirectProduct.inl n * g⁻¹ = SemidirectProduct.inl (φ g.right n) := by + apply SemidirectProduct.ext + · simp only [mul_assoc, SemidirectProduct.mul_left, SemidirectProduct.left_inl, + SemidirectProduct.right_inl, map_one, SemidirectProduct.inv_left, map_inv, + MulAut.inv_apply, MulAut.one_apply, mul_comm, map_mul, MulEquiv.apply_symm_apply, + mul_inv_cancel_left] + · simp only [SemidirectProduct.mul_right, SemidirectProduct.right_inl, mul_one, + SemidirectProduct.inv_right, mul_inv_cancel] + /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem semidirectIntrinsicSubquotientEquiv_conjugation [DistribMulAction K E] @@ -1279,28 +1286,12 @@ private theorem semidirectIntrinsicSubquotientEquiv_conjugation (semidirectTwoTorsionInclusionEquiv φ I hI y) = semidirectTwoTorsionInclusionEquiv φ I hI y' := by apply Subtype.ext - change g * SemidirectProduct.inl - (Multiplicative.ofAdd (Multiplicative.toAdd y).val) * g⁻¹ = - SemidirectProduct.inl (Multiplicative.ofAdd - (Multiplicative.toAdd y').val) change g * SemidirectProduct.inl (Multiplicative.ofAdd (Multiplicative.toAdd y).val) * g⁻¹ = SemidirectProduct.inl - (Multiplicative.ofAdd (g.right • - (Multiplicative.toAdd y).val)) + (Multiplicative.ofAdd (g.right • (Multiplicative.toAdd y).val)) rw [hact] - change g * SemidirectProduct.inl - (Multiplicative.ofAdd (Multiplicative.toAdd y).val) * g⁻¹ = - SemidirectProduct.inl - (φ g.right - (Multiplicative.ofAdd (Multiplicative.toAdd y).val)) - apply SemidirectProduct.ext - · simp only [mul_assoc, SemidirectProduct.mul_left, SemidirectProduct.left_inl, - SemidirectProduct.right_inl, map_one, SemidirectProduct.inv_left, map_inv, - MulAut.inv_apply, MulAut.one_apply, mul_comm, map_mul, MulEquiv.apply_symm_apply, - mul_inv_cancel_left] - · simp only [SemidirectProduct.mul_right, SemidirectProduct.right_inl, mul_one, - SemidirectProduct.inv_right, mul_inv_cancel] + exact semidirect_conj_inl_commutative φ g _ change Multiplicative.toAdd (semidirectIntrinsicSubquotientEquiv φ hfour I D hI hD (QuotientGroup.mk' (intrinsicDenominator I D) @@ -2169,25 +2160,25 @@ private theorem primitiveVector_specialLinear_completion_of_coordinateIdeal (v : obtain ⟨c, hc⟩ := (Ideal.mem_span_range_iff_exists_fun).mp hone let f : V →ₗ[R] R := Fintype.linearCombination R c have hfv : f v = 1 := by - simpa [f, Fintype.linearCombination_apply, smul_eq_mul, mul_comm] using hc + simpa only [f, Fintype.linearCombination_apply, smul_eq_mul, mul_comm] using hc let N : Submodule R V := LinearMap.ker f obtain ⟨n, b⟩ := Submodule.basisOfPid (Pi.basisFun R (Fin 4)) N have hli : ∀ (a : R), ∀ x ∈ N, a • v + x = 0 → a = 0 := by intro a x hx h have hx' : f x = 0 := LinearMap.mem_ker.mp hx have hz := congrArg f h - simpa [map_add, map_smul, hfv, hx'] using hz + simpa only [map_add, map_smul, hfv, hx', smul_eq_mul, mul_one, add_zero, map_zero] using hz have hsp : ∀ z : V, ∃ a : R, z + a • v ∈ N := by intro z refine ⟨-(f z), ?_⟩ apply LinearMap.mem_ker.mpr - simp [map_add, map_smul, hfv] + simp only [map_add, map_smul, hfv, neg_smul, map_neg, smul_eq_mul, mul_one, add_neg_cancel] let bfull : Module.Basis (Fin (n + 1)) R V := Module.Basis.mkFinCons v b hli hsp have hn : n + 1 = 4 := by have hcard := Fintype.card_congr (bfull.indexEquiv (Pi.basisFun R (Fin 4))) - simpa using hcard + simpa only [Nat.reduceEqDiff, Fintype.card_fin] using hcard let bfour : Module.Basis (Fin 4) R V := bfull.reindex (finCongr hn) have hbzero : bfour 0 = v := by have hz : (finCongr hn).symm (0 : Fin 4) = (0 : Fin (n + 1)) := @@ -2207,8 +2198,9 @@ private theorem primitiveVector_specialLinear_completion_of_coordinateIdeal (v : apply funext intro i change A.mulVec e i = v i - simp [A, Matrix.mulVec, dotProduct, e, Module.Basis.toMatrix_apply, - hbzero] + simp only [A, Matrix.mulVec, dotProduct, e, Module.Basis.toMatrix_apply, hbzero, + Pi.basisFun_repr, Fin.isValue, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq', + Finset.mem_univ, ↓reduceIte] /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem primitiveVector_specialLinear_completion (v : V) @@ -2858,7 +2850,8 @@ private theorem invariantDual_boxDetection_bound (boxDetectionSet N) standard hstandard (fun v _ ↦ dualDetectionSet_measurable (polynomialVectorVal v)) (boxDetectionSet_measurable N) hpoint huniform - simpa [standard] using hbound + simpa only [standard, ProbabilityMeasure.measureReal_eq_coe_coeFn, ge_iff_le, + polynomialVectorVal_boundedStandardVector] using hbound /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem dualProbability_detection_gap @@ -3400,6 +3393,7 @@ private theorem groupFactorUnitary_apply F ((l2Reindex (Multiplicative.toAdd : Multiplicative A ≃ A)) (semidirectFubini φ ξ h)) := rfl + /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem groupFactorUnitary_conj_inl (φ : H →* MulAut (Multiplicative A)) @@ -3417,7 +3411,7 @@ private theorem groupFactorUnitary_conj_inl (leftRegularUnitary (Multiplicative.ofAdd a) : GroupL2 (Multiplicative A) →L[ℂ] GroupL2 (Multiplicative A))) := by - apply ContinuousLinearMap.ext + apply conjStarAlgEquiv_eq_of_intertwining intro ξ apply lp.ext funext h @@ -3427,22 +3421,15 @@ private theorem groupFactorUnitary_conj_inl (SemidirectProduct.inl (Multiplicative.ofAdd a) : SemidirectProduct (Multiplicative A) H φ) : GroupL2 (SemidirectProduct (Multiplicative A) H φ) →L[ℂ] - GroupL2 (SemidirectProduct (Multiplicative A) H φ)) - ((groupFactorUnitary φ X F).symm ξ)) h) = - normalFourierCoordinates X F - ((leftRegularUnitary (Multiplicative.ofAdd a) : - GroupL2 (Multiplicative A) →L[ℂ] - GroupL2 (Multiplicative A)) - ((normalFourierCoordinates X F).symm (ξ h))) - congr 1 + GroupL2 (SemidirectProduct (Multiplicative A) H φ)) ξ) h) = + (normalFourierCoordinates X F).conjStarAlgEquiv + (leftRegularUnitary (Multiplicative.ofAdd a)) + (normalFourierCoordinates X F (semidirectFubini φ ξ h)) + rw [LinearIsometryEquiv.conjStarAlgEquiv_apply_apply, + LinearIsometryEquiv.symm_apply_apply] + apply congrArg (normalFourierCoordinates X F) ext b - rw [semidirectFubini_leftRegular_inl_apply] - change (semidirectFubini φ - ((groupFactorUnitary φ X F).symm ξ) h) - ((Multiplicative.ofAdd a)⁻¹ * b) = - ((normalFourierCoordinates X F).symm (ξ h)) - ((Multiplicative.ofAdd a)⁻¹ * b) - congr 1 + exact semidirectFubini_leftRegular_inl_apply φ (Multiplicative.ofAdd a) ξ h b /-- Cross-module support for the infinite Connes-rigidity construction. -/ private def gammaGroupFactorUnitary (n : ℕ) : @@ -3518,16 +3505,6 @@ private theorem splitL2Reindex_single [DecidableEq D] Equiv.symm_apply_eq] rfl -/-- Cross-module support for the infinite Connes-rigidity construction. -/ -private theorem splitFourierEquiv_single_smul [DecidableEq D] - (d : D) (c : ℂ) : - splitFourierEquiv (lp.single 2 d c) = c • splitCharacterL2 d := by - classical - have hsingle : lp.single (E := fun _ : D => ℂ) 2 d c = - c • lp.single (E := fun _ : D => ℂ) 2 d (1 : ℂ) := by - simpa only [smul_eq_mul, mul_one] using (lp.single_smul (E := fun _ : D => ℂ) 2 d c (1 : ℂ)) - rw [hsingle, map_smul, splitFourierEquiv_single] - /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem splitCharacterL2_zero : splitCharacterL2 0 = Lp.const 2 productHaar (1 : ℂ) := by @@ -3563,23 +3540,13 @@ private theorem splitFourierEquiv_kDLinear (k : K) (ξ : GroupL2 D) : have h : left = right := by apply lp.ext_continuousLinearMap (by simp only [ne_eq, ENNReal.ofNat_ne_top, not_false_eq_true]) intro d - apply ContinuousLinearMap.ext - intro c + apply ContinuousLinearMap.ext_ring change splitFourierEquiv - (l2Reindex (kDLinear k).toEquiv (lp.single 2 d c)) = + (l2Reindex (kDLinear k).toEquiv (lp.single 2 d (1 : ℂ))) = crossedActionL2Equiv paperSplitHaarAction k - (splitFourierEquiv (lp.single 2 d c)) - rw [splitL2Reindex_single, splitFourierEquiv_single_smul, - splitFourierEquiv_single_smul] - let hp : MeasurePreserving - (paperSplitPerm k⁻¹ : X × Y → X × Y) productHaar productHaar := - paperSplitHaarAction.action_preserves_measure k⁻¹ - change c • splitCharacterL2 (kDLinear k d) = - (Lp.compMeasurePreservingₗ ℂ (paperSplitPerm k⁻¹) hp) - (c • splitCharacterL2 d) - rw [map_smul] - exact congrArg (fun x : Lp ℂ 2 productHaar => c • x) - (splitCharacterL2_kDLinear k d) + (splitFourierEquiv (lp.single 2 d (1 : ℂ))) + rw [splitL2Reindex_single, splitFourierEquiv_single, splitFourierEquiv_single] + exact splitCharacterL2_kDLinear k d exact DFunLike.congr_fun h ξ end @@ -3615,7 +3582,7 @@ private theorem groupFactorUnitary_conj_inr GroupL2 (SemidirectProduct (Multiplicative A) H φ) →L[ℂ] GroupL2 (SemidirectProduct (Multiplicative A) H φ)) = (crossedGroupUnitary X k).toContinuousLinearEquiv.toContinuousLinearMap := by - apply ContinuousLinearMap.ext + apply conjStarAlgEquiv_eq_of_intertwining intro ξ apply lp.ext funext h @@ -3625,32 +3592,24 @@ private theorem groupFactorUnitary_conj_inr (SemidirectProduct.inr k : SemidirectProduct (Multiplicative A) H φ) : GroupL2 (SemidirectProduct (Multiplicative A) H φ) →L[ℂ] - GroupL2 (SemidirectProduct (Multiplicative A) H φ)) - ((groupFactorUnitary φ X F).symm ξ)) h) = - crossedActionL2Equiv X k (ξ (k⁻¹ * h)) + GroupL2 (SemidirectProduct (Multiplicative A) H φ)) ξ) h) = + crossedActionL2Equiv X k + (normalFourierCoordinates X F (semidirectFubini φ ξ (k⁻¹ * h))) have hnormal : semidirectFubini φ ((leftRegularUnitary (SemidirectProduct.inr k : SemidirectProduct (Multiplicative A) H φ) : GroupL2 (SemidirectProduct (Multiplicative A) H φ) →L[ℂ] - GroupL2 (SemidirectProduct (Multiplicative A) H φ)) - ((groupFactorUnitary φ X F).symm ξ)) h = - l2Reindex (φ k).toEquiv - (semidirectFubini φ ((groupFactorUnitary φ X F).symm ξ) - (k⁻¹ * h)) := by + GroupL2 (SemidirectProduct (Multiplicative A) H φ)) ξ) h = + l2Reindex (φ k).toEquiv (semidirectFubini φ ξ (k⁻¹ * h)) := by ext a rw [semidirectFubini_leftRegular_inr_apply, l2Reindex_apply] - apply congrArg (fun b : Multiplicative A => - (semidirectFubini φ - ((groupFactorUnitary φ X F).symm ξ) (k⁻¹ * h)) b) + apply congrArg (fun b : Multiplicative A => (semidirectFubini φ ξ (k⁻¹ * h)) b) change φ k⁻¹ a = (φ k).symm a rw [map_inv] rfl rw [hnormal, hcov] - congr 1 - exact congrArg (fun z => z (k⁻¹ * h)) - ((groupFactorUnitary φ X F).apply_symm_apply ξ) /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem carryTaggedFourierCovariance (n : ℕ) (k : K) @@ -3711,16 +3670,6 @@ private theorem gammaGroupFactorUnitary_conj_inr (n : ℕ) (k : K) : GroupL2 (Gamma n) →L[ℂ] GroupL2 (Gamma n)) = (crossedGroupUnitary (paperCarryHaarAction n) k).toContinuousLinearEquiv.toContinuousLinearMap := by - change - (groupFactorUnitary (kEAction n) (paperCarryHaarAction n) - (carryFourierEquiv n)).conjStarAlgEquiv - (leftRegularUnitary - (SemidirectProduct.inr k : - SemidirectProduct (Multiplicative (E n)) K (kEAction n)) : - GroupL2 (SemidirectProduct (Multiplicative (E n)) K (kEAction n)) - →L[ℂ] - GroupL2 (SemidirectProduct (Multiplicative (E n)) K (kEAction n))) = - (crossedGroupUnitary (paperCarryHaarAction n) k).toContinuousLinearEquiv.toContinuousLinearMap exact groupFactorUnitary_conj_inr (kEAction n) (paperCarryHaarAction n) (carryFourierEquiv n) (carryTaggedFourierCovariance n) k @@ -3733,13 +3682,8 @@ private theorem lambdaGroupFactorUnitary_conj_inr (k : K) : GroupL2 Lambda →L[ℂ] GroupL2 Lambda) = (crossedGroupUnitary paperSplitHaarAction k).toContinuousLinearEquiv.toContinuousLinearMap := by - change - (groupFactorUnitary kDAction paperSplitHaarAction splitFourierEquiv).conjStarAlgEquiv - (leftRegularUnitary (SemidirectProduct.inr k : Lambda) : - GroupL2 Lambda →L[ℂ] GroupL2 Lambda) = - (crossedGroupUnitary paperSplitHaarAction k).toContinuousLinearEquiv.toContinuousLinearMap - apply groupFactorUnitary_conj_inr - exact splitTaggedFourierCovariance + exact groupFactorUnitary_conj_inr kDAction paperSplitHaarAction splitFourierEquiv + splitTaggedFourierCovariance k /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem gammaGroupFactorUnitary_conj_inl (n : ℕ) (η : E n) : @@ -3749,21 +3693,12 @@ private theorem gammaGroupFactorUnitary_conj_inl (n : ℕ) (η : E n) : GroupL2 (Gamma n) →L[ℂ] GroupL2 (Gamma n)) = crossedMultiplier (paperCarryHaarAction n) (carryCharacterCoefficient n η) := by - calc - _ = crossedFiberwiseOperator (K := K) - ((normalFourierCoordinates (paperCarryHaarAction n) - (carryFourierEquiv n)).conjStarAlgEquiv - (leftRegularUnitary (Multiplicative.ofAdd η) : - GroupL2 (Multiplicative (E n)) →L[ℂ] - GroupL2 (Multiplicative (E n)))) := - groupFactorUnitary_conj_inl (A := E n) (H := K) - (kEAction n) (paperCarryHaarAction n) (carryFourierEquiv n) η - _ = crossedMultiplier (paperCarryHaarAction n) - (carryCharacterCoefficient n η) := by - change crossedFiberwiseOperator (K := K) _ = - crossedFiberwiseOperator (K := K) _ - congr 1 - exact carryFourier_conjugates_normal_generator n η + refine (groupFactorUnitary_conj_inl (A := E n) (H := K) + (kEAction n) (paperCarryHaarAction n) (carryFourierEquiv n) η).trans ?_ + change crossedFiberwiseOperator (K := K) _ = + crossedFiberwiseOperator (K := K) _ + congr 1 + exact carryFourier_conjugates_normal_generator n η /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem split_normalFourierCoordinates_eq : @@ -3781,22 +3716,13 @@ private theorem lambdaGroupFactorUnitary_conj_inl (d : D) : GroupL2 Lambda →L[ℂ] GroupL2 Lambda) = crossedMultiplier paperSplitHaarAction (splitCharacterCoefficient d) := by - calc - _ = crossedFiberwiseOperator (K := K) - ((normalFourierCoordinates paperSplitHaarAction - splitFourierEquiv).conjStarAlgEquiv - (leftRegularUnitary (Multiplicative.ofAdd d) : - GroupL2 (Multiplicative D) →L[ℂ] - GroupL2 (Multiplicative D))) := - groupFactorUnitary_conj_inl (A := D) (H := K) - kDAction paperSplitHaarAction splitFourierEquiv d - _ = crossedMultiplier paperSplitHaarAction - (splitCharacterCoefficient d) := by - change crossedFiberwiseOperator (K := K) _ = - crossedFiberwiseOperator (K := K) _ - congr 1 - rw [split_normalFourierCoordinates_eq] - exact splitFourier_conjugates_normal_generator d + refine (groupFactorUnitary_conj_inl (A := D) (H := K) + kDAction paperSplitHaarAction splitFourierEquiv d).trans ?_ + change crossedFiberwiseOperator (K := K) _ = + crossedFiberwiseOperator (K := K) _ + congr 1 + rw [split_normalFourierCoordinates_eq] + exact splitFourier_conjugates_normal_generator d end @@ -4228,108 +4154,17 @@ private theorem gammaGroupFactorUnitary_vacuum (n : ℕ) : (paperCarryHaarAction n) (carryFourierEquiv n) (@carryFourierEquiv_zero_single n (Classical.decEq (E n))) -open Classical in -/-- Cross-module support for the infinite Connes-rigidity construction. -/ -private theorem lambdaDelta_apply (g : Lambda) : - delta lambdaGroup 1 (show lambdaGroup from g) = - if g = (1 : Lambda) then 1 else 0 := by - classical - rw [delta_eq_single lambdaGroup (1 : lambdaGroup)] - by_cases hg : g = (1 : Lambda) - · subst g - rw [ite_eq_left rfl] - exact lp.single_apply_self (E := fun _ : lambdaGroup => ℂ) - 2 (1 : lambdaGroup) (1 : ℂ) - · rw [ite_eq_right hg] - exact lp.single_apply_ne (E := fun _ : lambdaGroup => ℂ) - 2 (1 : lambdaGroup) (1 : ℂ) hg - -open Classical in -/-- Cross-module support for the infinite Connes-rigidity construction. -/ -private theorem splitVacuum_apply (k : K) : - crossedVacuum paperSplitHaarAction k = - if k = 1 then Lp.const 2 productHaar (1 : ℂ) else 0 := by - classical - by_cases hk : k = (1 : K) - · subst k - rw [ite_eq_left rfl] - change - (@lp.single K (fun _ ↦ Lp ℂ 2 productHaar) _ - (fun a b ↦ Classical.propDecidable (a = b)) - 2 (1 : K) (Lp.const 2 productHaar (1 : ℂ))) 1 = - Lp.const 2 productHaar (1 : ℂ) - exact @lp.single_apply_self K (fun _ ↦ Lp ℂ 2 productHaar) _ - (fun a b ↦ Classical.propDecidable (a = b)) - 2 (1 : K) (Lp.const 2 productHaar (1 : ℂ)) - · rw [ite_eq_right hk] - change - (@lp.single K (fun _ ↦ Lp ℂ 2 productHaar) _ - (fun a b ↦ Classical.propDecidable (a = b)) - 2 (1 : K) (Lp.const 2 productHaar (1 : ℂ))) k = 0 - exact @lp.single_apply_ne K (fun _ ↦ Lp ℂ 2 productHaar) _ - (fun a b ↦ Classical.propDecidable (a = b)) - 2 (1 : K) (Lp.const 2 productHaar (1 : ℂ)) k hk - /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem lambdaGroupFactorUnitary_vacuum : lambdaGroupFactorUnitary (delta lambdaGroup 1) = crossedVacuum paperSplitHaarAction := by - classical - apply lp.ext - funext k - change - splitFourierEquiv - (l2Reindex (Multiplicative.toAdd : Multiplicative D ≃ D) - (semidirectFubini (A := Multiplicative D) (K := K) - kDAction (delta lambdaGroup 1) k)) = - crossedVacuum paperSplitHaarAction k - by_cases hk : k = 1 - · subst k - have hfiber : - l2Reindex (Multiplicative.toAdd : Multiplicative D ≃ D) - (semidirectFubini (A := Multiplicative D) (K := K) - kDAction (delta lambdaGroup 1) 1) = - lp.single 2 (0 : D) (1 : ℂ) := by - ext d - change delta lambdaGroup 1 - (⟨Multiplicative.ofAdd d, 1⟩ : Lambda) = - (lp.single (E := fun _ : D => ℂ) 2 (0 : D) (1 : ℂ)) d - rw [lambdaDelta_apply] - by_cases hd : d = 0 - · subst d - have hpoint : (⟨Multiplicative.ofAdd (0 : D), 1⟩ : Lambda) = 1 := by - apply SemidirectProduct.ext <;> rfl - rw [ite_eq_left hpoint] - exact (lp.single_apply_self (E := fun _ : D => ℂ) - 2 (0 : D) (1 : ℂ)).symm - · have hpoint : - (⟨Multiplicative.ofAdd d, 1⟩ : Lambda) ≠ 1 := by - intro hpoint - apply hd - have hleft := congrArg - (fun g : Lambda => Multiplicative.toAdd g.left) hpoint - simpa only [toAdd_ofAdd, SemidirectProduct.one_left, toAdd_one] using hleft - rw [ite_eq_right hpoint] - exact (lp.single_apply_ne (E := fun _ : D => ℂ) - 2 (0 : D) (1 : ℂ) hd).symm - rw [hfiber, splitFourierEquiv_zero_single] - rw [splitVacuum_apply, ite_eq_left rfl] - · have hfiber : - l2Reindex (Multiplicative.toAdd : Multiplicative D ≃ D) - (semidirectFubini (A := Multiplicative D) (K := K) - kDAction (delta lambdaGroup 1) k) = 0 := by - ext d - change delta lambdaGroup 1 - (⟨Multiplicative.ofAdd d, k⟩ : Lambda) = 0 - rw [lambdaDelta_apply] - have hpoint : - (⟨Multiplicative.ofAdd d, k⟩ : Lambda) ≠ 1 := by - intro hpoint - apply hk - simpa only [SemidirectProduct.one_right] using congrArg SemidirectProduct.right hpoint - rw [ite_eq_right hpoint] - rw [hfiber, map_zero] - rw [splitVacuum_apply, ite_eq_right hk] + change groupFactorUnitary kDAction paperSplitHaarAction splitFourierEquiv + (delta lambdaGroup 1) = crossedVacuum paperSplitHaarAction + rw [@delta_eq_single lambdaGroup + (@instDecidableEqSemidirectProduct (Multiplicative D) K _ _ + kDAction (Classical.decEq _) (Classical.decEq _)) 1] + exact groupFactorUnitary_vacuum kDAction paperSplitHaarAction splitFourierEquiv + (@splitFourierEquiv_zero_single (Classical.decEq D)) end @@ -4919,7 +4754,9 @@ private theorem lambdaFourMulDetectedMass_le_energy apply integral_mono hu (h₁.add h₂) intro χ by_cases hχ₁ : χ ∈ S₁ <;> by_cases hχ₂ : χ ∈ S₂ <;> - simp [hχ₁, hχ₂] + simp only [hχ₁, hχ₂, Set.mem_union, or_self, Set.indicator_of_mem, Pi.add_apply, + le_add_iff_nonneg_right, Nat.ofNat_nonneg, or_false, not_false_eq_true, + Set.indicator_of_notMem, add_zero, Std.le_refl, or_true, zero_add] _ = spectralDetectionEnergy μ (e, 0) + spectralDetectionEnergy μ (0, diagonal e) := by rw [integral_add h₁ h₂, diff --git a/LeanPool/InfiniteConnesRigidity/GroupConstruction.lean b/LeanPool/InfiniteConnesRigidity/GroupConstruction.lean index 86b7d70bcb..d875717e96 100644 --- a/LeanPool/InfiniteConnesRigidity/GroupConstruction.lean +++ b/LeanPool/InfiniteConnesRigidity/GroupConstruction.lean @@ -11,11 +11,6 @@ import Mathlib.Algebra.Order.Star.Real import Mathlib.Algebra.Ring.IsFormallyReal import Mathlib.GroupTheory.FiniteAbelian.Duality import Mathlib.LinearAlgebra.TensorProduct.Pi -import Mathlib.RingTheory.WittVector.IsPoly -import Mathlib.Tactic.ENatToNat -import Mathlib.Tactic.Polynomial.Basic -import Mathlib.Tactic.ReduceModChar -import Std.Tactic.BVDecide.Normalize.Prop public import LeanPool.InfiniteConnesRigidity.SpectralAndPropertyT /-! @@ -1512,7 +1507,7 @@ private theorem exists_affineUniformGeneratorDisplacement_of_no_fixed gromovRescaledAffineAction α (x n) (D (x n) / 2) apply exists_affineUniformGeneratorDisplacement_of_local_sequence γ S hgen · intro n s hs - simpa [γ, D] using + simpa only [γ, D, gromovRescaledAffineAction_apply, map_zero, inv_div, zero_add, sub_zero] using gromov_rescaled_generator_displacement_at_zero_le_two α S (x n) (hpositive (x n)) s hs · intro n z hz @@ -2182,7 +2177,10 @@ private theorem integerRankTwo_basis_decomposition (v : IntegerRankTwo) : v 1 • (Pi.single 1 1) := by funext i fin_cases i <;> - simp + simp only [Fin.zero_eta, Fin.isValue, zsmul_eq_mul, Pi.add_apply, Pi.mul_apply, + Pi.intCast_apply, Int.cast_eq, Pi.single_eq_same, mul_one, ne_eq, zero_ne_one, + not_false_eq_true, Pi.single_eq_of_ne, mul_zero, add_zero, Fin.mk_one, one_ne_zero, + zero_add] /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem integerDual_eq_one_iff_coordinate_values @@ -4071,7 +4069,7 @@ private theorem integerShalomShears_inv_mem classical simp only [integerShalomShears, Finset.mem_insert, Finset.mem_singleton] at hg ⊢ - rcases hg with rfl | rfl | rfl | rfl <;> simp + rcases hg with rfl | rfl | rfl | rfl <;> simp only [inv_inj, true_or, or_true, inv_inv] /-- Cross-module support for the infinite Connes-rigidity construction. -/ @[simp] @@ -4843,7 +4841,11 @@ private theorem polynomialCharacter_monomial z • (Pi.single i ((Polynomial.X : IntegralPolynomial) ^ n) : Fin 2 → IntegralPolynomial) := by ext j - by_cases hji : j = i <;> simp [hji] + by_cases hji : j = i <;> simp only [hji, zsmul_eq_mul, Pi.single_eq_same, + Polynomial.coeff_intCast_mul, Int.cast_eq, Polynomial.coeff_X_pow, + mul_ite, mul_one, mul_zero, Pi.smul_apply, ne_eq, + not_false_eq_true, Pi.single_eq_of_ne, Polynomial.coeff_zero, + smul_zero] rw [hsingle] change χ ((Multiplicative.ofAdd (Pi.single i ((Polynomial.X : IntegralPolynomial) ^ n) : @@ -4868,7 +4870,9 @@ private theorem polynomialCharacter_ext (Pi.single i (p + q) : Fin 2 → IntegralPolynomial) = Pi.single i p + Pi.single i q := by ext j - by_cases hji : j = i <;> simp [hji] + by_cases hji : j = i <;> simp only [hji, Pi.single_eq_same, Polynomial.coeff_add, + Pi.add_apply, ne_eq, not_false_eq_true, Pi.single_eq_of_ne, + Polynomial.coeff_zero, add_zero] rw [hsingle] have hsplit : Multiplicative.ofAdd @@ -4888,7 +4892,9 @@ private theorem polynomialCharacter_ext have hw : w = Pi.single (0 : Fin 2) (w 0) + Pi.single (1 : Fin 2) (w 1) := by ext i - fin_cases i <;> simp + fin_cases i <;> simp only [Fin.zero_eta, Fin.isValue, Pi.add_apply, Pi.single_eq_same, ne_eq, + zero_ne_one, not_false_eq_true, Pi.single_eq_of_ne, add_zero, Fin.mk_one, + one_ne_zero, zero_add] change χ (Multiplicative.ofAdd w) = ψ (Multiplicative.ofAdd w) rw [hw] @@ -5838,7 +5844,9 @@ private theorem shalomConstantVector_single shalomConstantVector (Pi.single i a) = (Pi.single i (Polynomial.C a) : Fin 2 → IntegralPolynomial) := by ext j - by_cases h : i = j <;> simp [shalomConstantVector, h] + by_cases h : i = j <;> simp only [shalomConstantVector, h, eq_intCast, AddMonoidHom.coe_mk, + ZeroHom.coe_mk, Pi.single_eq_same, ne_eq, not_false_eq_true, + Pi.single_eq_of_ne', Int.cast_zero, Polynomial.coeff_zero] /-- Cross-module support for the infinite Connes-rigidity construction. -/ private def shalomConstantSpecialLinear : @@ -6130,51 +6138,7 @@ private theorem shalom_projectionResidual_norm_lt_of_relativePair ‖(π (f g) : W →L[ℂ] W) ξ - ξ‖ < δ) : ‖ξ - (normalFixedSubmodule N₀ (π.comp f)).starProjection ξ‖ < δ / κ := by - let ρ : UnitaryRepresentation G₀ W := π.comp f - let M : Submodule ℂ W := normalFixedSubmodule N₀ ρ - let z : W := ξ - M.starProjection ξ - have hκ : 0 < κ := hpair.1 - change ‖z‖ < δ / κ - by_contra hnot - have hzlower : δ / κ ≤ ‖z‖ := le_of_not_gt hnot - have hz : z ≠ 0 := by - intro hzero - rw [hzero, norm_zero] at hzlower - exact (not_le_of_gt (div_pos hδ hκ)) hzlower - have hzmem : z ∈ Mᗮ := - Submodule.sub_starProjection_mem_orthogonal ξ - let w : Mᗮ := - ⟨((‖z‖ : ℂ)⁻¹) • z, (Mᗮ).smul_mem _ hzmem⟩ - have hwnorm : ‖w‖ = 1 := norm_smul_inv_norm hz - have hwsmall : - ∀ g ∈ F₀, - ‖(normalFixedOrthogonalRepresentation N₀ ρ g : - Mᗮ →L[ℂ] Mᗮ) w - w‖ < κ := by - intro g hg - have hcontract : - ‖(ρ g : W →L[ℂ] W) z - z‖ ≤ - ‖(ρ g : W →L[ℂ] W) ξ - ξ‖ := - normalFixed_orthogonalResidual_displacement_le N₀ ρ g ξ - have hwformula : - ‖(normalFixedOrthogonalRepresentation N₀ ρ g : - Mᗮ →L[ℂ] Mᗮ) w - w‖ = - ‖(ρ g : W →L[ℂ] W) z - z‖ / ‖z‖ := by - change ‖(ρ g : W →L[ℂ] W) - (((‖z‖ : ℂ)⁻¹) • z) - ((‖z‖ : ℂ)⁻¹) • z‖ = _ - rw [map_smul, ← smul_sub, norm_smul, norm_inv, - Complex.norm_real, Real.norm_of_nonneg (norm_nonneg z)] - simp only [div_eq_mul_inv, mul_comm] - rw [hwformula] - apply (div_lt_iff₀ (norm_pos_iff.mpr hz)).2 - have hgsmall : ‖(ρ g : W →L[ℂ] W) ξ - ξ‖ < δ := by - exact hsmall g hg - have hδbound : δ ≤ κ * ‖z‖ := - by simpa only [mul_comm] using (div_le_iff₀ hκ).mp hzlower - exact lt_of_lt_of_le (lt_of_le_of_lt hcontract hgsmall) hδbound - obtain ⟨η, hη, hηfixed⟩ := hpair.2 - Mᗮ inferInstance inferInstance inferInstance - (normalFixedOrthogonalRepresentation N₀ ρ) w hwnorm hwsmall - exact hη (normalFixedOrthogonalRepresentation_no_fixed N₀ ρ η hηfixed) + exact relativeKazhdanPair_orthogonalResidual_norm_lt N₀ hpair hδ W (π.comp f) ξ hsmall /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem shalom_normalizedFixedVector_of_relativePair @@ -6333,7 +6297,8 @@ private theorem shalom_constantCoordinate_fixed_of_constantTranslation_fixed (Multiplicative.ofAdd (Pi.single i (1 : ℤ))), ⟨Multiplicative.ofAdd (Pi.single i (1 : ℤ)), rfl⟩⟩ have hn := hfixed n - simpa [n] using hn + simpa only [n, shalomConstantEmbedding_inl, shalomConstantVector_single, eq_intCast, + Int.cast_one] using hn end @@ -6462,6 +6427,16 @@ section universe u v +/-- Transport centralizer membership before specializing to operators on Hilbert spaces. -/ +private theorem starAlgEquiv_mem_centralizer_image_iff {R A B : Type*} [CommSemiring R] [StarRing R] + [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] + [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] + (e : A ≃⋆ₐ[R] B) (S : Set A) (T : A) : + e T ∈ StarSubalgebra.centralizer R (e '' S) ↔ T ∈ StarSubalgebra.centralizer R S := by + have hinj : Function.Injective (fun x : A ↦ e x) := e.injective + simp only [StarSubalgebra.mem_centralizer_iff, Set.forall_mem_image, + ← map_star, ← map_mul, hinj.eq_iff] + /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem conj_mem_centralizer_image_iff {H K : Type*} @@ -6472,35 +6447,7 @@ private theorem conj_mem_centralizer_image_iff e.conjStarAlgEquiv T ∈ StarSubalgebra.centralizer ℂ (e.conjStarAlgEquiv '' S) ↔ T ∈ StarSubalgebra.centralizer ℂ S := by - rw [StarSubalgebra.mem_centralizer_iff, - StarSubalgebra.mem_centralizer_iff] - constructor - · intro h x hx - have hx' := h (e.conjStarAlgEquiv x) ⟨x, hx, rfl⟩ - constructor - · have heq : - e.conjStarAlgEquiv (x * T) = - e.conjStarAlgEquiv (T * x) := by - rw [map_mul, map_mul] - exact hx'.1 - exact e.conjStarAlgEquiv.injective heq - · have heq : - e.conjStarAlgEquiv (star x * T) = - e.conjStarAlgEquiv (T * star x) := by - rw [map_mul, map_mul] - simpa only [map_star] using hx'.2 - exact e.conjStarAlgEquiv.injective heq - · intro h y hy - obtain ⟨x, hx, rfl⟩ := hy - have hx' := h x hx - constructor - · have heq := congrArg e.conjStarAlgEquiv hx'.1 - rw [map_mul, map_mul] at heq - exact heq - · have heq := congrArg e.conjStarAlgEquiv hx'.2 - rw [map_mul, map_mul] at heq - rw [map_star] at heq - exact heq + exact starAlgEquiv_mem_centralizer_image_iff e.conjStarAlgEquiv S T /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem conj_image_centralizer @@ -6598,27 +6545,15 @@ private theorem crossedHaarHilbertEquiv_multiplier_conj crossedMultiplier Y (Lp.compMeasurePreserving e.toMeasurableEquiv.symm (EquivariantHaarEquiv.symm e).measure_preserving f) := by - apply ContinuousLinearMap.ext - intro η - obtain ⟨ξ, rfl⟩ := (crossedHaarHilbertEquiv e).surjective η + apply conjStarAlgEquiv_eq_of_intertwining + intro ξ apply lp.ext funext k - change - crossedHaarHilbertEquiv e - (crossedMultiplier X f - ((crossedHaarHilbertEquiv e).symm - ((crossedHaarHilbertEquiv e) ξ))) k = - crossedBaseMultiplier Y - (Lp.compMeasurePreserving e.toMeasurableEquiv.symm - (EquivariantHaarEquiv.symm e).measure_preserving f) - (crossedBaseHaarEquiv e (ξ k)) - rw [LinearIsometryEquiv.symm_apply_apply] - change - crossedBaseHaarEquiv e (crossedBaseMultiplier X f (ξ k)) = - crossedBaseMultiplier Y - (Lp.compMeasurePreserving e.toMeasurableEquiv.symm - (EquivariantHaarEquiv.symm e).measure_preserving f) - (crossedBaseHaarEquiv e (ξ k)) + change crossedBaseHaarEquiv e (crossedBaseMultiplier X f (ξ k)) = + crossedBaseMultiplier Y + (Lp.compMeasurePreserving e.toMeasurableEquiv.symm + (EquivariantHaarEquiv.symm e).measure_preserving f) + (crossedBaseHaarEquiv e (ξ k)) exact crossedBaseHaarEquiv_multiplier_apply e f (ξ k) /-- Cross-module support for the infinite Connes-rigidity construction. -/ @@ -7537,8 +7472,10 @@ private theorem upperUnitriangular_factorization (g : Q) have h32 := hu 3 2 (by decide) apply Matrix.SpecialLinearGroup.ext intro i j - fin_cases i <;> fin_cases j <;> - simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + revert i j + refine matrix_four_entrywise _ _ + ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ <;> + simp only [Fin.isValue, ConnesRigidity.MennickeIdentity.specialLinear_mul_transvection_apply, Fin.reduceEq, ↓reduceIte, Matrix.SpecialLinearGroup.transvection_coe, Matrix.add_apply, Matrix.one_apply, @@ -7837,7 +7774,14 @@ private theorem semidirectMap_range_index apply Quotient.sound' rw [QuotientGroup.leftRel_apply] refine ⟨SemidirectProduct.inr z.right, ?_⟩ - apply SemidirectProduct.ext <;> simp [F, j] + apply SemidirectProduct.ext <;> simp only [F, j, SemidirectProduct.map_inr, + MonoidHom.id_apply, SemidirectProduct.left_inr, + SemidirectProduct.mul_left, SemidirectProduct.inv_left, + SemidirectProduct.right_inl, inv_one, map_one, + SemidirectProduct.left_inl, MulAut.one_apply, + SemidirectProduct.inv_right, inv_mul_cancel, + SemidirectProduct.right_inr, SemidirectProduct.mul_right, + one_mul] change F.range.index = f.range.index exact (Nat.card_congr (Equiv.ofBijective quotientMap hbijective)).symm @@ -7942,24 +7886,6 @@ private theorem additiveLeftRegularUnitary_single simp only [leftRegularUnitary_apply, lp.single_apply, Pi.single_apply, inv_mul_eq_iff_eq_mul, ofAdd_add] -/-- Cross-module support for the infinite Connes-rigidity construction. -/ -private theorem fourierUnitary_single_smul - {A : Type u} [DecidableEq A] - {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] - (U : GroupL2 (Multiplicative A) ≃ₗᵢ[ℂ] H) - (χ : A → H) - (hU : ∀ b : A, - U (lp.single 2 (Multiplicative.ofAdd b) 1) = χ b) - (b : A) (c : ℂ) : - U (lp.single 2 (Multiplicative.ofAdd b) c) = c • χ b := by - have hs : lp.single (E := fun _ : Multiplicative A => ℂ) - 2 (Multiplicative.ofAdd b) c = - c • lp.single (E := fun _ : Multiplicative A => ℂ) - 2 (Multiplicative.ofAdd b) (1 : ℂ) := by - simpa only [smul_eq_mul, mul_one] using (lp.single_smul (E := fun _ : Multiplicative A => ℂ) - 2 (Multiplicative.ofAdd b) c (1 : ℂ)) - rw [hs, map_smul, hU] - /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem fourier_conjugates_regular_of_character_basis {A : Type u} [AddCommGroup A] [DecidableEq A] @@ -7983,30 +7909,19 @@ private theorem fourier_conjugates_regular_of_character_basis GroupL2 (Multiplicative A)) = T.comp F := by apply lp.ext_continuousLinearMap (by simp only [ne_eq, ENNReal.ofNat_ne_top, not_false_eq_true]) intro b - apply ContinuousLinearMap.ext - intro c + apply ContinuousLinearMap.ext_ring change U ((leftRegularUnitary (Multiplicative.ofAdd a) : GroupL2 (Multiplicative A) →L[ℂ] GroupL2 (Multiplicative A)) - (lp.single 2 (Multiplicative.ofAdd (Multiplicative.toAdd b)) c)) = + (lp.single 2 (Multiplicative.ofAdd (Multiplicative.toAdd b)) (1 : ℂ))) = T (U (lp.single 2 - (Multiplicative.ofAdd (Multiplicative.toAdd b)) c)) - rw [additiveLeftRegularUnitary_single - a (Multiplicative.toAdd b) c, - fourierUnitary_single_smul U χ hU, - fourierUnitary_single_smul U χ hU, - map_smul, hT] - apply ContinuousLinearMap.ext + (Multiplicative.ofAdd (Multiplicative.toAdd b)) (1 : ℂ))) + rw [additiveLeftRegularUnitary_single a (Multiplicative.toAdd b) (1 : ℂ), + hU, hU, hT] + apply conjStarAlgEquiv_eq_of_intertwining intro ξ - obtain ⟨η, rfl⟩ := U.surjective ξ - change U - ((leftRegularUnitary (Multiplicative.ofAdd a) : - GroupL2 (Multiplicative A) →L[ℂ] - GroupL2 (Multiplicative A)) - (U.symm (U η))) = T (U η) - rw [U.symm_apply_apply] - exact DFunLike.congr_fun hcomp η + exact DFunLike.congr_fun hcomp ξ /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem carryFourier_conjugates_regular_of_character_basis diff --git a/LeanPool/InfiniteConnesRigidity/SpectralAndPropertyT.lean b/LeanPool/InfiniteConnesRigidity/SpectralAndPropertyT.lean index 52aed8891c..814d2c17f8 100644 --- a/LeanPool/InfiniteConnesRigidity/SpectralAndPropertyT.lean +++ b/LeanPool/InfiniteConnesRigidity/SpectralAndPropertyT.lean @@ -12,16 +12,10 @@ public import Mathlib.MeasureTheory.Measure.ProbabilityMeasure public import Mathlib.Order.CompletePartialOrder import Mathlib.Algebra.Ring.IsFormallyReal import Mathlib.RingTheory.PiTensorProduct -import Mathlib.RingTheory.WittVector.IsPoly -import Mathlib.Tactic.ENatToNat -import Mathlib.Tactic.Polynomial.Basic -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) @@ -35,6 +29,16 @@ noncomputable section attribute [local instance low] instAddCommGroupOfIsSimpleAddGroupOfIsNilpotent namespace ConnesRigidity + +/-- Express displacement of a normalized vector without repeated scalar-norm elaboration. -/ +public theorem norm_normalized_displacement {W : Type*} [NormedAddCommGroup W] [NormedSpace ℂ W] + (T : W →L[ℂ] W) (z : W) : + ‖T (((‖z‖ : ℂ)⁻¹) • z) - ((‖z‖ : ℂ)⁻¹) • z‖ = + ‖T z - z‖ / ‖z‖ := by + rw [map_smul, ← smul_sub, norm_smul, norm_inv, Complex.norm_real, + Real.norm_of_nonneg (norm_nonneg z), div_eq_mul_inv, mul_comm] + + section open ConnesRigidity MeasureTheory @@ -146,31 +150,17 @@ private theorem crossedMultiplier_mem_vonNeumannClosure_of_base_commutation (f : crossedCoefficient X) : crossedMultiplier X f ∈ vonNeumannClosure (crossedCharacterGeneratorSet X χ) := by - change - crossedMultiplier X f ∈ StarSubalgebra.centralizer ℂ - (↑(StarSubalgebra.centralizer ℂ - (crossedCharacterGeneratorSet X χ)) : - Set (crossedHilbert X →L[ℂ] crossedHilbert X)) - rw [StarSubalgebra.mem_centralizer_iff] - intro T hT - have hcomm : - ∀ S : crossedHilbert X →L[ℂ] crossedHilbert X, - S ∈ StarSubalgebra.centralizer ℂ - (crossedCharacterGeneratorSet X χ) → - Commute S (crossedMultiplier X f) := by - intro S hS - apply (commute_crossedMultiplier_iff_blocks X S f).2 - intro q k - apply hbase (crossedOperatorBlock X S q k) - intro i - apply crossedOperatorBlock_commute_of_commute_fiberwise X S - (crossedBaseMultiplier X (χ i)) - have hi := (StarSubalgebra.mem_centralizer_iff ℂ).1 hS - (crossedMultiplier X (χ i)) - (Or.inl ⟨i, rfl⟩) - exact hi.1.symm - exact ⟨(hcomm T hT).eq, - (hcomm (star T) (star_mem hT)).eq⟩ + apply mem_vonNeumannClosure_of_commute + intro S hS + apply (commute_crossedMultiplier_iff_blocks X S f).2 + intro q k + apply hbase (crossedOperatorBlock X S q k) + intro i + apply crossedOperatorBlock_commute_of_commute_fiberwise X S + (crossedBaseMultiplier X (χ i)) + have hi := (StarSubalgebra.mem_centralizer_iff ℂ).1 hS + (crossedMultiplier X (χ i)) (Or.inl ⟨i, rfl⟩) + exact hi.1.symm section ContinuousCharacters @@ -335,46 +325,17 @@ private theorem crossed_character_vonNeumannClosure_eq_full_of_multipliers vonNeumannClosure (crossedCharacterGeneratorSet A χ)) : vonNeumannClosure (crossedCharacterGeneratorSet A χ) = (crossedProductModel A).algebra := by - let S : Set (crossedHilbert A →L[ℂ] crossedHilbert A) := - crossedCharacterGeneratorSet A χ - let G : Set (crossedHilbert A →L[ℂ] crossedHilbert A) := - crossedGeneratorSet A - have hsub : S ⊆ G := by - rintro T (⟨i, rfl⟩ | ⟨k, rfl⟩) + change vonNeumannClosure (crossedCharacterGeneratorSet A χ) = + vonNeumannClosure (crossedGeneratorSet A) + apply vonNeumannClosure_eq_of_generators + · rintro T (⟨i, rfl⟩ | ⟨k, rfl⟩) · exact Or.inl ⟨χ i, rfl⟩ · exact Or.inr ⟨k, rfl⟩ - have hcommutants : - StarSubalgebra.centralizer ℂ S = - StarSubalgebra.centralizer ℂ G := by - apply StarSubalgebra.ext - intro T - constructor - · intro hT - rw [StarSubalgebra.mem_centralizer_iff] - intro R hR - rcases hR with ⟨f, rfl⟩ | ⟨k, rfl⟩ - · have hf : crossedMultiplier A f ∈ - vonNeumannClosure S := hχ f - have hforward := - (StarSubalgebra.mem_centralizer_iff ℂ).1 hf T hT - have hstar := - (StarSubalgebra.mem_centralizer_iff ℂ).1 - (star_mem hf) T hT - exact ⟨hforward.1.symm, hstar.1.symm⟩ - · exact (StarSubalgebra.mem_centralizer_iff ℂ).1 hT _ - (Or.inr ⟨k, rfl⟩) - · intro hT - exact StarSubalgebra.centralizer_le ℂ S G hsub hT - apply VonNeumannAlgebra.ext - intro T - change - T ∈ StarSubalgebra.centralizer ℂ - (StarSubalgebra.centralizer ℂ S : - Set (crossedHilbert A →L[ℂ] crossedHilbert A)) ↔ - T ∈ StarSubalgebra.centralizer ℂ - (StarSubalgebra.centralizer ℂ G : - Set (crossedHilbert A →L[ℂ] crossedHilbert A)) - rw [hcommutants] + · rintro T (⟨f, rfl⟩ | ⟨k, rfl⟩) + · exact hχ f + · exact StarAlgebra.adjoin_le_centralizer_centralizer ℂ _ + (StarAlgebra.subset_adjoin ℂ _ (Or.inr ⟨k, rfl⟩)) + end CrossedClosureEquality @@ -1223,10 +1184,7 @@ private theorem quotientProjection_error_lt_of_spectralGap have hwnorm_formula : ‖(π (E.splitting h) : V →L[ℂ] V) w - w‖ = ‖(π (E.splitting h) : V →L[ℂ] V) z - z‖ / ‖z‖ := by - dsimp [w] - rw [map_smul, ← smul_sub, norm_smul, norm_inv, - Complex.norm_real, Real.norm_of_nonneg (norm_nonneg _)] - simp only [div_eq_mul_inv, mul_comm] + exact norm_normalized_displacement (π (E.splitting h) : V →L[ℂ] V) z rw [hwnorm_formula] at hgap have hzpos : 0 < ‖z‖ := norm_pos_iff.mpr hz have hgap' : κ * ‖z‖ ≤ @@ -4088,7 +4046,7 @@ theorem IsMinimizingAffinePair.normalizer_fixed_of_no_linear_invariants intro k have hfixed := affineLinearRepresentation_sub_fixed hmin.fixed_right hy₂ k - simpa [v, hdisp] using hfixed + simpa only [v, hdisp, map_sub] using hfixed have hvzero : v = 0 := hno v (affineLinear_invariant_of_sup_eq_top α K₁ K₂ hgen v hv₁ hv₂) have hleft : α g x₁ = x₁ := by @@ -4405,7 +4363,8 @@ private theorem canonicalKernelVector_inner {I : Type u} simp only [canonicalKernelVector] rw [UniformSpace.Completion.inner_coe, preKernel_inner_single] have hscalar : (scalarOperatorKernel K j i) 1 = K j i := by - simp [scalarOperatorKernel, ContinuousLinearMap.toSpanSingleton_apply] + simp only [scalarOperatorKernel, ContinuousLinearMap.toSpanSingleton_apply, smul_eq_mul, + one_mul] simp only [star_one, mul_one, RCLike.inner_apply, one_mul, hscalar] exact hK.isHermitian.apply i j @@ -4421,8 +4380,8 @@ private theorem preKernel_single_scalar_inner {I : Type u} | add f g hf hg => simp only [inner_add_right, hf, hg] | single j d => rw [preKernel_inner_single, preKernel_inner_single] - simp [scalarOperatorKernel, - ContinuousLinearMap.toSpanSingleton_apply] + simp only [scalarOperatorKernel, ContinuousLinearMap.toSpanSingleton_apply, RCLike.star_def, + smul_eq_mul, RCLike.inner_apply, map_mul, star_mul', one_mul] ring /-- A pre-kernel basis vector is a scalar multiple of its canonical kernel vector. -/ @@ -4436,7 +4395,8 @@ private theorem coe_single_eq_smul_canonicalKernelVector {I : Type u} refine UniformSpace.Completion.denseRange_coe.eq_of_inner_left ℂ fun f ↦ ?_ rw [UniformSpace.Completion.inner_coe, UniformSpace.Completion.inner_coe] - simpa [smul_eq_mul] using preKernel_single_scalar_inner K i z c f + simpa only [smul_eq_mul, Finsupp.smul_single, mul_one, Finsupp.single_mul] using + preKernel_single_scalar_inner K i z c f /-- The index action sends each canonical vector to the corresponding translated vector. -/ private theorem actionKernelUnitaryRepresentation_canonicalKernelVector @@ -5445,8 +5405,9 @@ theorem exists_marked_affine_ultralimit have heq (n : ℕ) : markedAffinePairDisplacement (α n) (x n) (y n) p = markedAffinePairDisplacement (α n) (x n) (y n) p' := by - simp [p, p', markedAffinePairDisplacement, - markedAffineOrbitPoint, hx n k] + simp only [p, p', markedAffinePairDisplacement, markedAffineOrbitPoint, hx n k, + markedOrbitAction_apply, mul_one, ↓reduceIte, map_one, Bool.false_eq_true, + AffineIsometryEquiv.coe_one, id_eq] exact tendsto_nhds_unique (hconv p q) (by simpa only [heq] using hconv p' q) · intro k @@ -5460,8 +5421,9 @@ theorem exists_marked_affine_ultralimit have heq (n : ℕ) : markedAffinePairDisplacement (α n) (x n) (y n) p = markedAffinePairDisplacement (α n) (x n) (y n) p' := by - simp [p, p', markedAffinePairDisplacement, - markedAffineOrbitPoint, hy n k] + simp only [p, p', markedAffinePairDisplacement, markedAffineOrbitPoint, hy n k, + markedOrbitAction_apply, mul_one, Bool.false_eq_true, ↓reduceIte, map_one, + AffineIsometryEquiv.coe_one, id_eq, sub_self] exact tendsto_nhds_unique (hconv p q) (by simpa only [heq] using hconv p' q) · let p : (G × Bool) × (G × Bool) := @@ -5473,8 +5435,9 @@ theorem exists_marked_affine_ultralimit R.realization.vector p⟫_ℂ) := by have h := hconv p p rw [← R.realization.gram p p] at h - simpa [p, markedAffinePairDisplacement, - markedAffineOrbitPoint] using h + simpa only [p, markedAffinePairDisplacement, markedAffineOrbitPoint, + inner_self_eq_norm_sq_to_K, Complex.coe_algebraMap, map_one, ↓reduceIte, + AffineIsometryEquiv.coe_one, id_eq, Bool.false_eq_true] using h rw [markedPairPoint_sub L R hadd] exact norm_eq_of_gram_and_tendsto_norm (Filter.hyperfilter ℕ) @@ -6722,7 +6685,11 @@ private theorem columnShear_mul_castSucc (s : Fin 3 → IntegralPolynomial) Matrix.transvection (2 : Fin 4) 3 (s 2) * g.val.val : Matrix (Fin 4) (Fin 4) IntegralPolynomial)) i.castSucc j = _ fin_cases i <;> - simp [Matrix.transvection, Matrix.mul_apply, Fin.sum_univ_four] + simp only [Matrix.transvection, Matrix.mul_apply, Fin.sum_univ_four, transvection, + Fin.isValue, Fin.zero_eta, Fin.castSucc_zero, Matrix.add_apply, one_apply_eq, Fin.reduceEq, + and_false, not_false_eq_true, single_apply_of_ne, add_zero, one_ne_zero, false_and, one_mul, + ne_eq, zero_ne_one, one_apply_ne, zero_mul, single_apply_same, zero_add, mul_zero, mul_one, + Fin.mk_one, Fin.castSucc_one, Fin.reduceFinMk, Fin.reduceCastSucc] /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem columnShear_mul_last (s : Fin 3 → IntegralPolynomial) @@ -6773,8 +6740,10 @@ private theorem mul_rowShear_castSucc (s : Fin 3 → IntegralPolynomial) Matrix (Fin 4) (Fin 4) IntegralPolynomial)) i j.castSucc = _ simp only [← mul_assoc] fin_cases j <;> - simp [Matrix.mul_transvection_apply_same, - Matrix.mul_transvection_apply_of_ne, mul_comm] + simp only [Matrix.mul_transvection_apply_same, Matrix.mul_transvection_apply_of_ne, mul_comm, + Fin.isValue, Fin.zero_eta, Fin.castSucc_zero, ne_eq, Fin.reduceEq, not_false_eq_true, + mul_transvection_apply_of_ne, zero_ne_one, mul_transvection_apply_same, Fin.mk_one, + Fin.castSucc_one, one_ne_zero, Fin.reduceFinMk, Fin.reduceCastSucc] /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem mul_rowShear_last (s : Fin 3 → IntegralPolynomial) @@ -6849,21 +6818,21 @@ private theorem cornulierBoundedFactorization_of_stableRange cornulierRowShear rcoeff : integralElementaryGroup).val : Matrix (Fin 4) (Fin 4) IntegralPolynomial) 0 3 = 0 rw [mul_rowShear_last] - simpa [lcoeff, hg₂last] using + simpa only [lcoeff, hg₂last, Fin.isValue, Fin.castSucc_zero, mul_one, add_neg_cancel] using (columnShear_mul_castSucc lcoeff g₂ (0 : Fin 3) 3) · change (((cornulierColumnShear lcoeff * g₂) * cornulierRowShear rcoeff : integralElementaryGroup).val : Matrix (Fin 4) (Fin 4) IntegralPolynomial) 1 3 = 0 rw [mul_rowShear_last] - simpa [lcoeff, hg₂last] using + simpa only [lcoeff, hg₂last, Fin.isValue, Fin.castSucc_one, mul_one, add_neg_cancel] using (columnShear_mul_castSucc lcoeff g₂ (1 : Fin 3) 3) · change (((cornulierColumnShear lcoeff * g₂) * cornulierRowShear rcoeff : integralElementaryGroup).val : Matrix (Fin 4) (Fin 4) IntegralPolynomial) 2 3 = 0 rw [mul_rowShear_last] - simpa [lcoeff, hg₂last] using + simpa only [lcoeff, hg₂last, Fin.isValue, Fin.reduceCastSucc, mul_one, add_neg_cancel] using (columnShear_mul_castSucc lcoeff g₂ (2 : Fin 3) 3) · change (((cornulierColumnShear lcoeff * g₂) * @@ -6881,7 +6850,8 @@ private theorem cornulierBoundedFactorization_of_stableRange (cornulierColumnShear lcoeff * g₂) 3 (0 : Fin 3) have hzero := columnShear_mul_last lcoeff g₂ (0 : Fin 4) have hlast := columnShear_mul_last lcoeff g₂ (3 : Fin 4) - simpa [hzero, hlast, rcoeff, hg₂last] using hrow + simpa only [hzero, hlast, rcoeff, hg₂last, Fin.isValue, Fin.castSucc_zero, mul_neg, + one_mul, add_neg_cancel] using hrow · change (((cornulierColumnShear lcoeff * g₂) * cornulierRowShear rcoeff : integralElementaryGroup).val : @@ -6890,7 +6860,8 @@ private theorem cornulierBoundedFactorization_of_stableRange (cornulierColumnShear lcoeff * g₂) 3 (1 : Fin 3) have hzero := columnShear_mul_last lcoeff g₂ (1 : Fin 4) have hlast := columnShear_mul_last lcoeff g₂ (3 : Fin 4) - simpa [hzero, hlast, rcoeff, hg₂last] using hrow + simpa only [hzero, hlast, rcoeff, hg₂last, Fin.isValue, Fin.castSucc_one, mul_neg, + one_mul, add_neg_cancel] using hrow · change (((cornulierColumnShear lcoeff * g₂) * cornulierRowShear rcoeff : integralElementaryGroup).val : @@ -6899,7 +6870,8 @@ private theorem cornulierBoundedFactorization_of_stableRange (cornulierColumnShear lcoeff * g₂) 3 (2 : Fin 3) have hzero := columnShear_mul_last lcoeff g₂ (2 : Fin 4) have hlast := columnShear_mul_last lcoeff g₂ (3 : Fin 4) - simpa [hzero, hlast, rcoeff, hg₂last] using hrow + simpa only [hzero, hlast, rcoeff, hg₂last, Fin.isValue, Fin.reduceCastSucc, mul_neg, + one_mul, add_neg_cancel] using hrow · change (((cornulierColumnShear lcoeff * g₂) * cornulierRowShear rcoeff : integralElementaryGroup).val : @@ -7196,6 +7168,7 @@ theorem HasUniformRelativeKazhdanDisplacement.map rintro ⟨_, ⟨g, hg, rfl⟩⟩ exact hN ⟨g, hg⟩ + /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem uniformRelativeKazhdanDisplacement_of_pair {G : CountableDiscreteGroup.{u}} (N : Subgroup G) [N.Normal] @@ -7233,10 +7206,7 @@ private theorem uniformRelativeKazhdanDisplacement_of_pair ‖(π g : W →L[ℂ] W) z - z‖ / ‖z‖ := by change ‖(π g : W →L[ℂ] W) (((‖z‖ : ℂ)⁻¹) • z) - ((‖z‖ : ℂ)⁻¹) • z‖ = _ - rw [map_smul, ← smul_sub] - rw [norm_smul, norm_inv, Complex.norm_real, - Real.norm_of_nonneg (norm_nonneg z)] - simp only [div_eq_mul_inv, mul_comm] + exact norm_normalized_displacement (π g : W →L[ℂ] W) z rw [hwformula] apply (div_lt_iff₀ (norm_pos_iff.mpr hz)).2 have hsmallg := hsmall g hg @@ -7261,6 +7231,59 @@ private theorem uniformRelativeKazhdanDisplacement_of_pair _ = 2 * ‖z‖ := by rw [Unitary.norm_map]; ring _ < ε := by linarith +/-- A relative Kazhdan pair bounds the component orthogonal to its fixed subspace. -/ +public theorem relativeKazhdanPair_orthogonalResidual_norm_lt + {G : CountableDiscreteGroup.{u}} (N : Subgroup G) [N.Normal] + {F : Finset G} {κ δ : ℝ} + (hpair : IsRelativeKazhdanPair G N F κ) (hδ : 0 < δ) + (W : Type u) [NormedAddCommGroup W] [InnerProductSpace ℂ W] [CompleteSpace W] + (π : UnitaryRepresentation G W) (ξ : W) + (hsmall : ∀ g ∈ F, ‖(π g : W →L[ℂ] W) ξ - ξ‖ < δ) : + ‖ξ - (normalFixedSubmodule N π).starProjection ξ‖ < δ / κ := by + let M : Submodule ℂ W := normalFixedSubmodule N π + let z : W := ξ - M.starProjection ξ + have hκ : 0 < κ := hpair.1 + change ‖z‖ < δ / κ + by_contra hnot + have hzlower : δ / κ ≤ ‖z‖ := le_of_not_gt hnot + have hz : z ≠ 0 := by + intro hzero + rw [hzero, norm_zero] at hzlower + exact (not_le_of_gt (div_pos hδ hκ)) hzlower + have hzmem : z ∈ Mᗮ := + Submodule.sub_starProjection_mem_orthogonal ξ + let w : Mᗮ := + ⟨((‖z‖ : ℂ)⁻¹) • z, (Mᗮ).smul_mem _ hzmem⟩ + have hwnorm : ‖w‖ = 1 := norm_smul_inv_norm hz + have hwsmall : + ∀ g ∈ F, + ‖(normalFixedOrthogonalRepresentation N π g : + Mᗮ →L[ℂ] Mᗮ) w - w‖ < κ := by + intro g hg + have hcontract : + ‖(π g : W →L[ℂ] W) z - z‖ ≤ + ‖(π g : W →L[ℂ] W) ξ - ξ‖ := + normalFixed_orthogonalResidual_displacement_le N π g ξ + have hwformula : + ‖(normalFixedOrthogonalRepresentation N π g : + Mᗮ →L[ℂ] Mᗮ) w - w‖ = + ‖(π g : W →L[ℂ] W) z - z‖ / ‖z‖ := by + change ‖(π g : W →L[ℂ] W) + (((‖z‖ : ℂ)⁻¹) • z) - ((‖z‖ : ℂ)⁻¹) • z‖ = _ + exact norm_normalized_displacement (π g : W →L[ℂ] W) z + rw [hwformula] + apply (div_lt_iff₀ (norm_pos_iff.mpr hz)).2 + have hgsmall : ‖(π g : W →L[ℂ] W) ξ - ξ‖ < δ := by + exact hsmall g hg + have hδbound : δ ≤ κ * ‖z‖ := + by simpa only [mul_comm] using (div_le_iff₀ hκ).mp hzlower + exact lt_of_lt_of_le (lt_of_le_of_lt hcontract hgsmall) hδbound + obtain ⟨η, hη, hηfixed⟩ := hpair.2 + Mᗮ inferInstance inferInstance inferInstance + (normalFixedOrthogonalRepresentation N π) w hwnorm hwsmall + exact hη (normalFixedOrthogonalRepresentation_no_fixed N π η hηfixed) + + /-- Cross-module support for the infinite Connes-rigidity construction. -/ @[expose] public @@ -7824,7 +7847,7 @@ private theorem hasAffineGaussianRealization change representation g (CornulierUltralimit.canonicalKernelVector K (1 : G)) = CornulierUltralimit.canonicalKernelVector K g - simpa [ρ] using + simpa only [ρ, MonoidHom.coe_mk, OneHom.coe_mk, Equiv.coe_mulLeft, mul_one] using CornulierUltralimit.actionKernelUnitaryRepresentation_canonicalKernelVector K ρ hinv g (1 : G) rw [haction] @@ -7835,7 +7858,7 @@ private theorem hasAffineGaussianRealization change 1 ^ 2 - 2 * (Real.exp (-t * ‖α g x - α (1 : G) x‖ ^ 2) : ℂ).re + 1 ^ 2 = 2 * (1 - Real.exp (-(t * ‖α g x - x‖ ^ 2))) - have hxone : α (1 : G) x = x := by simp + have hxone : α (1 : G) x = x := by simp only [map_one, AffineIsometryEquiv.coe_one, id_eq] rw [hxone] simp only [Complex.ofReal_re, one_pow] rw [neg_mul] @@ -8049,7 +8072,8 @@ private theorem rankTwoColumnBlock_add (v w : Fin 2 → A) : rankTwoColumnBlock v + rankTwoColumnBlock w := by ext i j by_cases hj : j = (1 : Fin 2) <;> - simp [rankTwoColumnBlock, hj] + simp only [rankTwoColumnBlock, hj, Fin.isValue, ↓reduceIte, Pi.add_apply, Matrix.add_apply, + add_zero] /-- Cross-module support for the infinite Connes-rigidity construction. -/ @[simp] @@ -8155,11 +8179,20 @@ private theorem rankTwoParabolicSpecialLinear_inl (SemidirectProduct.inl (Multiplicative.ofAdd v) : ElementaryRankTwoSemidirect A) i j = _ rw [Matrix.SpecialLinearGroup.coe_mul] - fin_cases i <;> fin_cases j <;> - simp [rankTwoParabolicMatrix, - rankTwoColumnBlock, Matrix.reindex_apply, Matrix.fromBlocks, - Matrix.SpecialLinearGroup.transvection_coe, Matrix.mul_apply, - Fin.sum_univ_four, Matrix.one_apply, Matrix.single_apply] + revert i j + refine matrix_four_entrywise _ _ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ <;> + simp only [rankTwoParabolicMatrix, rankTwoColumnBlock, Matrix.reindex_apply, + Matrix.fromBlocks, Matrix.SpecialLinearGroup.transvection_coe, Matrix.mul_apply, + Fin.sum_univ_four, Matrix.one_apply, Matrix.single_apply, Nat.reduceAdd, fromBlocks, + SemidirectProduct.right_inl, OneMemClass.coe_one, SpecialLinearGroup.coe_one, + SemidirectProduct.left_inl, toAdd_ofAdd, Fin.isValue, reindex_apply, submatrix_apply, + finTwoPlusTwo_symm_zero, of_apply, Sum.elim_inl, + SpecialLinearGroup.transvection_coe, Matrix.add_apply, single_apply, true_and, Fin.reduceEq, + and_false, add_zero, mul_ite, mul_one, mul_zero, + Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte, finTwoPlusTwo_symm_one, zero_ne_one, + finTwoPlusTwo_symm_two, Sum.elim_inr, finTwoPlusTwo_symm_three, and_true, + one_ne_zero, zero_add, zero_mul, false_and, ite_mul, one_mul, Finset.sum_ite_eq, + Matrix.zero_apply] /-- Cross-module support for the infinite Connes-rigidity construction. -/ @[simp] @@ -8177,16 +8210,20 @@ private theorem rankTwoParabolicSpecialLinear_inr_root (SemidirectProduct.inr (elementaryRankTwoRoot hij a) : ElementaryRankTwoSemidirect A) k l = _ fin_cases i <;> fin_cases j <;> - fin_cases k <;> fin_cases l <;> - 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] + first + | exact (hij rfl).elim + | revert k l + refine matrix_four_entrywise _ _ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ <;> + simp 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, 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 diff --git a/LeanPool/InfiniteConnesRigidity/UniversalLattice.lean b/LeanPool/InfiniteConnesRigidity/UniversalLattice.lean index 41c80d0115..01db0e75d1 100644 --- a/LeanPool/InfiniteConnesRigidity/UniversalLattice.lean +++ b/LeanPool/InfiniteConnesRigidity/UniversalLattice.lean @@ -16,22 +16,10 @@ public import Mathlib.RingTheory.AdjoinRoot public import Mathlib.RingTheory.DiscreteValuationRing.Basic public import Mathlib.RingTheory.KrullDimension.Basic public import Mathlib.RingTheory.Localization.AtPrime.Basic -import Mathlib.Algebra.AffineMonoid.Basic import Mathlib.Algebra.Ring.IsFormallyReal import Mathlib.Data.Finsupp.Encodable import Mathlib.GroupTheory.Complement -import Mathlib.Order.CompletePartialOrder -import Mathlib.RingTheory.Henselian import Mathlib.RingTheory.KrullDimension.Polynomial -import Mathlib.RingTheory.PiTensorProduct -import Mathlib.RingTheory.PicardGroup -import Mathlib.RingTheory.RegularLocalRing.Defs -import Mathlib.RingTheory.SimpleRing.Principal -import Mathlib.RingTheory.WittVector.IsPoly -import Mathlib.Tactic.ENatToNat -import Mathlib.Tactic.Polynomial.Basic -import Mathlib.Tactic.ReduceModChar -import Std.Tactic.BVDecide.Normalize.Prop /-! # Universal-lattice and relative-property-(T) foundations @@ -39,8 +27,51 @@ import Std.Tactic.BVDecide.Normalize.Prop noncomputable section +-- Prefer concrete additive groups to the speculative simple/nilpotent group instance. +attribute [local instance low] instAddCommGroupOfIsSimpleAddGroupOfIsNilpotent + namespace ConnesRigidity +/-- An intertwining identity determines conjugation by an isometric equivalence. -/ +public theorem conjStarAlgEquiv_eq_of_intertwining + {V W : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] + [NormedAddCommGroup W] [InnerProductSpace ℂ W] [CompleteSpace W] + (e : V ≃ₗᵢ[ℂ] W) (T : V →L[ℂ] V) (S : W →L[ℂ] W) + (h : ∀ ξ, e (T ξ) = S (e ξ)) : e.conjStarAlgEquiv T = S := by + apply ContinuousLinearMap.ext + intro ξ + change e (T (e.symm ξ)) = S ξ + rw [h, e.apply_symm_apply] + + +/-- Reuse finite entry elimination across four-by-four matrix proofs. -/ +public theorem matrix_four_entrywise {β : Type*} + (M N : Matrix (Fin 4) (Fin 4) β) + (h00 : M 0 0 = N 0 0) (h01 : M 0 1 = N 0 1) (h02 : M 0 2 = N 0 2) (h03 : M 0 3 = N 0 3) + (h10 : M 1 0 = N 1 0) (h11 : M 1 1 = N 1 1) (h12 : M 1 2 = N 1 2) (h13 : M 1 3 = N 1 3) + (h20 : M 2 0 = N 2 0) (h21 : M 2 1 = N 2 1) (h22 : M 2 2 = N 2 2) (h23 : M 2 3 = N 2 3) + (h30 : M 3 0 = N 3 0) (h31 : M 3 1 = N 3 1) (h32 : M 3 2 = N 3 2) (h33 : M 3 3 = N 3 3) : + ∀ i j, M i j = N i j := by + intro i j + fin_cases i <;> fin_cases j + · exact h00 + · exact h01 + · exact h02 + · exact h03 + · exact h10 + · exact h11 + · exact h12 + · exact h13 + · exact h20 + · exact h21 + · exact h22 + · exact h23 + · exact h30 + · exact h31 + · exact h32 + · exact h33 + + section namespace FeedbackBooleanPolynomial @@ -263,6 +294,49 @@ def vonNeumannClosure rw [StarSubalgebra.coe_centralizer_centralizer] exact Set.centralizer_centralizer_centralizer ((S ∪ star S).centralizer) +section + +variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] + +/-- Membership in a bicommutant from commutation with its commutant. -/ +public +theorem mem_vonNeumannClosure_of_commute + (S : Set (H →L[ℂ] H)) (A : H →L[ℂ] H) + (h : ∀ T ∈ StarSubalgebra.centralizer ℂ S, Commute T A) : + A ∈ vonNeumannClosure S := by + apply (StarSubalgebra.mem_centralizer_iff ℂ).2 + intro T hT + exact ⟨(h T hT).eq, (h (star T) (star_mem hT)).eq⟩ + +/-- Two generator sets have the same bicommutant when each generates the other. -/ +public +theorem vonNeumannClosure_eq_of_generators + (S G : Set (H →L[ℂ] H)) + (hsub : S ⊆ G) (hclosure : G ⊆ vonNeumannClosure S) : + vonNeumannClosure S = vonNeumannClosure G := by + have hcommutants : StarSubalgebra.centralizer ℂ S = StarSubalgebra.centralizer ℂ G := by + apply StarSubalgebra.ext + intro T + constructor + · intro hT + apply (StarSubalgebra.mem_centralizer_iff ℂ).2 + intro R hR + have hf := hclosure hR + have hforward := (StarSubalgebra.mem_centralizer_iff ℂ).1 hf T hT + have hstar := (StarSubalgebra.mem_centralizer_iff ℂ).1 (star_mem hf) T hT + exact ⟨hforward.1.symm, hstar.1.symm⟩ + · intro hT + exact StarSubalgebra.centralizer_le ℂ S G hsub hT + apply VonNeumannAlgebra.ext + intro T + change T ∈ StarSubalgebra.centralizer ℂ + (StarSubalgebra.centralizer ℂ S : Set (H →L[ℂ] H)) ↔ + T ∈ StarSubalgebra.centralizer ℂ + (StarSubalgebra.centralizer ℂ G : Set (H →L[ℂ] H)) + rw [hcommutants] + +end + /-- Cross-module support for the infinite Connes-rigidity construction. -/ @[expose] public @@ -608,12 +682,12 @@ private theorem inducedRepresentation_hasAlmostInvariantUnitVectors let q₀ : G ⧸ S := QuotientGroup.mk 1 have hraw_lower : 1 ≤ ‖raw‖ := by have hcoord := PiLp.norm_apply_le raw q₀ - simpa [raw, q₀, hvnorm] using hcoord + simpa only [raw, q₀, hvnorm, ge_iff_le] using hcoord have hraw_pos : 0 < ‖raw‖ := zero_lt_one.trans_le hraw_lower let a : ℂ := ((‖raw‖⁻¹ : ℝ) : ℂ) let ξ : InducedSpace (H := H) S := a • raw have ha_norm : ‖a‖ = ‖raw‖⁻¹ := by - simp [a] + simp only [a, Complex.ofReal_inv, norm_inv, Complex.norm_real, norm_norm] have ha_le_one : ‖a‖ ≤ 1 := by rw [ha_norm] exact inv_le_one_of_one_le₀ hraw_lower @@ -638,13 +712,14 @@ private theorem inducedRepresentation_hasAlmostInvariantUnitVectors InducedSpace (H := H) S →L[ℂ] InducedSpace (H := H) S) ξ - ξ) q = a • ((π (correction S g (g⁻¹ • q)) : H →L[ℂ] H) v - v) := by - simp [ξ, raw, map_smul, smul_sub] + simp only [ξ, raw, map_smul, smul_sub, PiLp.sub_apply, PiLp.smul_apply, + inducedRepresentation_apply] rw [hformula, norm_smul] calc ‖a‖ * ‖(π (correction S g (g⁻¹ • q)) : H →L[ℂ] H) v - v‖ ≤ 1 * ‖(π (correction S g (g⁻¹ • q)) : H →L[ℂ] H) v - v‖ := mul_le_mul_of_nonneg_right ha_le_one (norm_nonneg _) - _ < δ := by simpa using hclose + _ < δ := by simpa only [one_mul] using hclose calc ‖(inducedRepresentation S π g : InducedSpace (H := H) S →L[ℂ] InducedSpace (H := H) S) ξ - ξ‖ ≤ @@ -656,7 +731,7 @@ private theorem inducedRepresentation_hasAlmostInvariantUnitVectors Finset.sum_lt_sum_of_nonempty Finset.univ_nonempty (fun q _ ↦ hcoordinate q) _ = n * δ := by - simp [n] + simp only [n, Finset.sum_const, Finset.card_univ, nsmul_eq_mul] _ < ε := by dsimp [δ] rw [show n * (ε / (n + 1)) = (n * ε) / (n + 1) by ring] @@ -734,7 +809,8 @@ private theorem inducedInvariant_baseCoset_isInvariant rw [← Subgroup.coe_inv] exact subgroup_smul_baseCoset S t⁻¹ have hcorr : correction S (t : G) q₀ = s := by - simpa [t, r, q₀] using correction_conjugate_at_baseCoset S s + simpa only [t, r, q₀, Subgroup.coe_mul, + InvMemClass.coe_inv] using correction_conjugate_at_baseCoset S s simpa only [inducedRepresentation_apply, htfix, hcorr] using heval end Induced @@ -2204,6 +2280,21 @@ def suslinDifferencePath (a : A) (Matrix.SpecialLinearGroup.map suslinBivariateConstantRingHom (suslinDifferenceDilation a g))⁻¹ +/-- Compose coefficient maps before applying them to a special linear matrix. -/ +private theorem specialLinear_map_comp_apply + {B C : Type*} [CommRing B] [CommRing C] + (f : B →+* C) (g : A →+* B) + (M : Matrix.SpecialLinearGroup Index A) : + Matrix.SpecialLinearGroup.map f (Matrix.SpecialLinearGroup.map g M) = + Matrix.SpecialLinearGroup.map (f.comp g) M := rfl +/-- Evaluating a constant matrix over a polynomial ring returns that matrix. -/ +private theorem specialLinear_eval_constant (x : Polynomial A) + (M : Matrix.SpecialLinearGroup Index (Polynomial A)) : + Matrix.SpecialLinearGroup.map (Polynomial.evalRingHom x) + (Matrix.SpecialLinearGroup.map suslinBivariateConstantRingHom M) = M := by + apply Matrix.SpecialLinearGroup.ext + intro i j + exact Polynomial.eval_C /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem suslinBivariateShift_eval_zero (a : A) : (Polynomial.evalRingHom (0 : Polynomial A)).comp @@ -2224,28 +2315,10 @@ private theorem suslinDifferencePath_eval_zero (a : A) Matrix.SpecialLinearGroup.map (Polynomial.evalRingHom (0 : Polynomial A)) (suslinDifferencePath a g) = 1 := by - rw [suslinDifferencePath, map_mul, map_inv] - have hshift : - Matrix.SpecialLinearGroup.map - (Polynomial.evalRingHom (0 : Polynomial A)) - (Matrix.SpecialLinearGroup.map - (suslinBivariateShiftRingHom a) g) = - suslinDifferenceDilation a g := by - apply Matrix.SpecialLinearGroup.ext - intro i j - exact RingHom.congr_fun (suslinBivariateShift_eval_zero a) (g i j) - have hconstant : - Matrix.SpecialLinearGroup.map - (Polynomial.evalRingHom (0 : Polynomial A)) - (Matrix.SpecialLinearGroup.map - suslinBivariateConstantRingHom - (suslinDifferenceDilation a g)) = - suslinDifferenceDilation a g := by - apply Matrix.SpecialLinearGroup.ext - intro i j - simp only [suslinBivariateConstantRingHom, Matrix.SpecialLinearGroup.map_apply_coe, - RingHom.mapMatrix_apply, coe_evalRingHom, Matrix.map_apply, eval_C] - rw [hshift, hconstant, mul_inv_cancel] + rw [suslinDifferencePath, map_mul, map_inv, + specialLinear_eval_constant, specialLinear_map_comp_apply, + suslinBivariateShift_eval_zero] + exact mul_inv_cancel _ /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem suslinBivariateShift_eval_mul_X (a b : A) : @@ -2270,28 +2343,10 @@ theorem suslinDifferencePath_eval_mul_X (a b : A) (suslinDifferencePath a g) = suslinDifferenceDilation (a + b) g * (suslinDifferenceDilation a g)⁻¹ := by - rw [suslinDifferencePath, map_mul, map_inv] - have hshift : - Matrix.SpecialLinearGroup.map - (Polynomial.evalRingHom (Polynomial.C b * Polynomial.X)) - (Matrix.SpecialLinearGroup.map - (suslinBivariateShiftRingHom a) g) = - suslinDifferenceDilation (a + b) g := by - apply Matrix.SpecialLinearGroup.ext - intro i j - exact RingHom.congr_fun (suslinBivariateShift_eval_mul_X a b) (g i j) - have hconstant : - Matrix.SpecialLinearGroup.map - (Polynomial.evalRingHom (Polynomial.C b * Polynomial.X)) - (Matrix.SpecialLinearGroup.map - suslinBivariateConstantRingHom - (suslinDifferenceDilation a g)) = - suslinDifferenceDilation a g := by - apply Matrix.SpecialLinearGroup.ext - intro i j - simp only [suslinBivariateConstantRingHom, Matrix.SpecialLinearGroup.map_apply_coe, - RingHom.mapMatrix_apply, coe_evalRingHom, Matrix.map_apply, eval_C] - rw [hshift, hconstant] + rw [suslinDifferencePath, map_mul, map_inv, + specialLinear_eval_constant, specialLinear_map_comp_apply, + suslinBivariateShift_eval_mul_X] + rfl /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem suslinDifferenceDilationRingHom_baseChange @@ -2316,10 +2371,12 @@ theorem suslinDifferenceDilation_baseChange (suslinDifferenceDilation a g) = suslinDifferenceDilation (f a) (Matrix.SpecialLinearGroup.map (Polynomial.mapRingHom f) g) := by - apply Matrix.SpecialLinearGroup.ext - intro i j - exact RingHom.congr_fun - (suslinDifferenceDilationRingHom_baseChange f a) (g i j) + change Matrix.SpecialLinearGroup.map (Polynomial.mapRingHom f) + (Matrix.SpecialLinearGroup.map (suslinDifferenceDilationRingHom a) g) = + Matrix.SpecialLinearGroup.map (suslinDifferenceDilationRingHom (f a)) + (Matrix.SpecialLinearGroup.map (Polynomial.mapRingHom f) g) + rw [specialLinear_map_comp_apply, specialLinear_map_comp_apply, + suslinDifferenceDilationRingHom_baseChange] /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem suslinBivariateShiftRingHom_baseChange @@ -2877,7 +2934,8 @@ private theorem suslin_polynomial_conjugate_opposite_integral_mem_eventual (Polynomial.C (d : A)) = (Polynomial.mapRingHom (algebraMap A B)) c' := by have hcomp := congrArg (fun z : Polynomial B => z.comp σ) hc - simpa [a', c', σ, τ, Polynomial.mul_comp, Polynomial.map_comp] + simpa only [a', c', σ, τ, Polynomial.mul_comp, Polynomial.map_comp, coe_mapRingHom, map_C, + map_comp, Polynomial.map_mul, map_X, mul_comp, C_comp] using hcomp obtain ⟨k, hki, hkj⟩ := Fin.exists_ne_and_ne_of_two_lt i j (by decide : 2 < 4) @@ -2900,8 +2958,8 @@ private theorem suslin_polynomial_conjugate_opposite_integral_mem_eventual congr 2 apply congrArg (Matrix.SpecialLinearGroup.transvection hij.symm) dsimp [r, τ, D] - simp [Polynomial.map_comp, Polynomial.mul_comp, - Polynomial.C_mul, mul_assoc] + simp only [Polynomial.map_comp, Polynomial.mul_comp, mul_assoc, map_C, + Polynomial.map_mul, map_X, map_comp, map_mul, mul_comp, X_comp] /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem suslin_polynomial_conjugate_opposite_mem_eventual @@ -2988,7 +3046,8 @@ private theorem quotient_uniformizer_isUnit_of_relation _ = ρ f := (congrArg ρ hf).symm _ = 0 := hfzero refine isUnit_iff_exists_inv'.mpr ⟨-(ρ q), ?_⟩ - linear_combination -hrelation + rw [neg_mul, mul_comm, neg_eq_iff_eq_neg] + exact eq_neg_of_add_eq_zero_right hrelation /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem quotient_nonzero_coefficient_isUnit @@ -4238,9 +4297,14 @@ private theorem firstRowClear_mul_apply Matrix.transvection (0 : Fin 4) 2 (-(g 0 2)) * Matrix.transvection (0 : Fin 4) 3 (-(g 0 3)))) i j = _ simp only [← mul_assoc] - fin_cases i <;> fin_cases j <;> - simp [Matrix.mul_transvection_apply_same, - Matrix.mul_transvection_apply_of_ne, h0, h1, h2, h3] + revert i j + refine matrix_four_entrywise _ _ + ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ <;> + simp only [Matrix.mul_transvection_apply_same, Matrix.mul_transvection_apply_of_ne, h0, h1, + h2, h3, Fin.isValue, ne_eq, Fin.reduceEq, not_false_eq_true, + mul_transvection_apply_of_ne, zero_ne_one, ↓reduceIte, + mul_transvection_apply_same, mul_one, add_neg_cancel, one_ne_zero, + mul_zero, add_zero] /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem lowerRight_det_eq_one @@ -4280,7 +4344,9 @@ private theorem firstColumn_block_decomposition change (if i = 0 then if j = 0 then 1 else 0 else g i j) = lowerBlockMatrix (g.val.submatrix Fin.succ Fin.succ) i j cases i using Fin.cases <;> cases j using Fin.cases <;> - simp [Matrix.submatrix, hcolumn] + simp only [Matrix.submatrix, hcolumn, Fin.isValue, ↓reduceIte, submatrix, + lowerBlockMatrix_zero_zero, Fin.succ_ne_zero, lowerBlockMatrix_zero_succ, + lowerBlockMatrix_succ_zero, lowerBlockMatrix_succ_succ, of_apply] /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem firstColumn_mem_elementary_iff_block @@ -4355,7 +4421,11 @@ private theorem lowerBlockSpecialLinear_one : apply Matrix.SpecialLinearGroup.ext intro i j cases i using Fin.cases <;> cases j using Fin.cases <;> - simp [lowerBlockSpecialLinear, Matrix.one_apply, eq_comm] + simp only [↓reduceIte, lowerBlockSpecialLinear, Matrix.one_apply, eq_comm, + SpecialLinearGroup.coe_one, + Fin.isValue, lowerBlockMatrix_zero_zero, lowerBlockMatrix_zero_succ, + Nat.reduceAdd, Fin.succ_ne_zero, + lowerBlockMatrix_succ_zero, lowerBlockMatrix_succ_succ, Fin.succ_inj] /-- Cross-module support for the infinite Connes-rigidity construction. -/ @[simp] @@ -4370,8 +4440,10 @@ private theorem lowerBlockSpecialLinear_mul (lowerBlockMatrix (b : Matrix (Fin 3) (Fin 3) R) * lowerBlockMatrix (c : Matrix (Fin 3) (Fin 3) R)) i j cases i using Fin.cases <;> cases j using Fin.cases <;> - simp [Matrix.mul_apply, - Fin.sum_univ_succ, lowerBlockMatrix] + simp only [Matrix.mul_apply, Fin.sum_univ_succ, lowerBlockMatrix, Fin.isValue, Fin.cases_zero, + SpecialLinearGroup.coe_mul, Fin.succ_zero_eq_one, Finset.univ_unique, Fin.default_eq_zero, + Finset.sum_singleton, Fin.succ_one_eq_two, mul_one, Fin.cases_succ, mul_zero, + Finset.sum_const_zero, add_zero, zero_mul, zero_add] /-- Cross-module support for the infinite Connes-rigidity construction. -/ private def lowerBlockHom : @@ -4391,9 +4463,13 @@ private theorem lowerBlockHom_transvection (i j : Fin 3) (h : i ≠ j) (r : R) : apply Matrix.SpecialLinearGroup.ext intro p q cases p using Fin.cases <;> cases q using Fin.cases <;> - simp [lowerBlockHom, lowerBlockSpecialLinear, + simp only [add_zero, ↓reduceIte, lowerBlockHom, lowerBlockSpecialLinear, Matrix.SpecialLinearGroup.transvection_coe, - Matrix.single_apply, Matrix.one_apply, eq_comm] + Matrix.single_apply, Matrix.one_apply, eq_comm, MonoidHom.coe_mk, OneHom.coe_mk, + SpecialLinearGroup.transvection_coe, Fin.isValue, lowerBlockMatrix_zero_zero, Nat.reduceAdd, + Matrix.add_apply, Fin.succ_ne_zero, and_self, + lowerBlockMatrix_zero_succ, Fin.succ_inj, + false_and, lowerBlockMatrix_succ_zero, and_false, lowerBlockMatrix_succ_succ, single_apply] @@ -4532,7 +4608,12 @@ theorem stabilizedTwoSpecialLinear_one : apply Matrix.SpecialLinearGroup.ext intro i j cases i using Fin.lastCases <;> cases j using Fin.lastCases <;> - simp [Matrix.one_apply, eq_comm] + simp only [↓reduceIte, Matrix.one_apply, eq_comm, Fin.reduceLast, + stabilizedTwoSpecialLinear_two_two, + SpecialLinearGroup.coe_one, stabilizedTwoSpecialLinear_two_castSucc, + Fin.isValue, finTwo_castSucc_ne_two, + stabilizedTwoSpecialLinear_castSucc_two, Nat.reduceAdd, + stabilizedTwoSpecialLinear_castSucc_castSucc, Fin.castSucc_inj] /-- Cross-module support for the infinite Connes-rigidity construction. -/ @[simp] @@ -4544,7 +4625,12 @@ theorem stabilizedTwoSpecialLinear_mul apply Matrix.SpecialLinearGroup.ext intro i j cases i using Fin.lastCases <;> cases j using Fin.lastCases <;> - simp [Matrix.mul_apply, Fin.sum_univ_castSucc] + simp only [Matrix.mul_apply, Fin.sum_univ_castSucc, Fin.reduceLast, + stabilizedTwoSpecialLinear_two_two, SpecialLinearGroup.coe_mul, Fin.isValue, + stabilizedTwoSpecialLinear_two_castSucc, stabilizedTwoSpecialLinear_castSucc_two, mul_zero, + Finset.sum_const_zero, mul_one, zero_add, stabilizedTwoSpecialLinear_castSucc_castSucc, + zero_mul, add_zero, Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton, + Fin.castSucc_zero] /-- Cross-module support for the infinite Connes-rigidity construction. -/ @[expose] @@ -4600,8 +4686,14 @@ private theorem stabilizedTwoHom_transvection apply Matrix.SpecialLinearGroup.ext intro p q cases p using Fin.lastCases <;> cases q using Fin.lastCases <;> - simp [Matrix.SpecialLinearGroup.transvection_coe, - Matrix.single_apply, Matrix.one_apply, eq_comm] + simp only [add_zero, ↓reduceIte, Matrix.SpecialLinearGroup.transvection_coe, + Matrix.single_apply, + Matrix.one_apply, + eq_comm, Fin.reduceLast, stabilizedTwoHom_two_two, Nat.reduceAdd, + SpecialLinearGroup.transvection_coe, Fin.isValue, Matrix.add_apply, + finTwo_castSucc_ne_two, and_self, + stabilizedTwoHom_two_castSucc, Fin.castSucc_inj, false_and, + stabilizedTwoHom_castSucc_two, and_false, stabilizedTwoHom_castSucc_castSucc, single_apply] /-- Cross-module support for the infinite Connes-rigidity construction. -/ @[expose] @@ -5844,6 +5936,65 @@ private def mennickeWord Matrix.SpecialLinearGroup.transvection (show (2 : Fin 3) ≠ 1 by decide) (-(ap * d)) +/-- Check the nine entries without repeating finite case elimination in every matrix step. -/ +private theorem matrix_three_entrywise {β : Type*} + (M N : Matrix (Fin 3) (Fin 3) β) + (h00 : M 0 0 = N 0 0) (h01 : M 0 1 = N 0 1) (h02 : M 0 2 = N 0 2) + (h10 : M 1 0 = N 1 0) (h11 : M 1 1 = N 1 1) (h12 : M 1 2 = N 1 2) + (h20 : M 2 0 = N 2 0) (h21 : M 2 1 = N 2 1) (h22 : M 2 2 = N 2 2) : + ∀ i j, M i j = N i j := by + intro i j + fin_cases i <;> fin_cases j + · exact h00 + · exact h01 + · exact h02 + · exact h10 + · exact h11 + · exact h12 + · exact h20 + · exact h21 + · exact h22 + +/-- Compute a three-dimensional column shear as one matrix equality. -/ +private theorem specialLinear_mul_transvection_three {R : Type*} [CommRing R] + (g : Matrix.SpecialLinearGroup (Fin 3) R) {i j : Fin 3} + (h : i ≠ j) (r : R) : + ((g * Matrix.SpecialLinearGroup.transvection h r : + Matrix.SpecialLinearGroup (Fin 3) R) : Matrix (Fin 3) (Fin 3) R) = + !![if 0 = j then g 0 j + r * g 0 i else g 0 0, + if 1 = j then g 0 j + r * g 0 i else g 0 1, + if 2 = j then g 0 j + r * g 0 i else g 0 2; + if 0 = j then g 1 j + r * g 1 i else g 1 0, + if 1 = j then g 1 j + r * g 1 i else g 1 1, + if 2 = j then g 1 j + r * g 1 i else g 1 2; + if 0 = j then g 2 j + r * g 2 i else g 2 0, + if 1 = j then g 2 j + r * g 2 i else g 2 1, + if 2 = j then g 2 j + r * g 2 i else g 2 2] := by + simpa only [specialLinear_mul_transvection_apply] using + Matrix.eta_fin_three + ((g * Matrix.SpecialLinearGroup.transvection h r : + Matrix.SpecialLinearGroup (Fin 3) R) : Matrix (Fin 3) (Fin 3) R) + +/-- Multiply the first two-by-two Mennicke block in one matrix step. -/ +private theorem mennicke_first_block_product (a ap b c d : R) + (hdet : a * ap * d - b * c = 1) : + (!![1, 0, 0; -c * d, a * d, -1; 0, 1, 0] : Matrix (Fin 3) (Fin 3) R) * + !![a, b, 0; c, ap * d, 0; 0, 0, 1] = + !![a, b, 0; 0, d, -1; c, ap * d, 0] := by + have hleft : -(c * d * a) + a * d * c = 0 := by ring + have hcenter : -(c * d * b) + a * d * (ap * d) = d := by + linear_combination d * hdet + simp only [Matrix.mul_fin_three, one_mul, mul_one, zero_mul, + mul_zero, zero_add, add_zero, neg_mul, hleft, hcenter] + +/-- Multiply the second two-by-two Mennicke block in one matrix step. -/ +private theorem mennicke_second_block_product (a ap b c d : R) : + (!![a, 0, b; 0, 1, d; c, 0, ap * d] : Matrix (Fin 3) (Fin 3) R) * + !![ap, b, 0; c, a * d, 0; 0, 0, 1] = + !![a * ap, a * b, b; c, a * d, d; ap * c, b * c, ap * d] := by + simp only [Matrix.mul_fin_three, one_mul, mul_one, zero_mul, + mul_zero, zero_add, add_zero, mul_comm c ap, mul_comm c b] + /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem parkWoodburn_mennicke_identity (a ap b c d : R) (hdet : a * ap * d - b * c = 1) : @@ -5854,124 +6005,103 @@ private theorem parkWoodburn_mennicke_identity (c * (ap * d) * (a * d) - d * (c + ap * c * (a * d))) 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 only [Fin.isValue, Fin.zero_eta, SpecialLinearGroup.transvection_coe, + revert i j + refine matrix_three_entrywise _ _ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ <;> + simp only [Fin.isValue, 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, + cons_val_fin_one, ne_eq, zero_ne_one, one_apply_ne, and_self, + cons_val_one, 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 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] + have hw2 : (w2 : Matrix (Fin 3) (Fin 3) R) = + !![1, 0, 0; -c * d, 1, a * d - 1; 0, 0, 1] := by + simpa only [w2, Fin.isValue, Fin.reduceEq, ↓reduceIte, hw1, neg_mul, of_apply, + cons_val', cons_val_zero, cons_val_fin_one, cons_val_one, + cons_val, mul_zero, add_zero, mul_one, zero_add] using + specialLinear_mul_transvection_three w1 + (show (1 : Fin 3) ≠ 2 by decide) (a * d - 1) 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 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] + have hw3 : (w3 : Matrix (Fin 3) (Fin 3) R) = + !![1, 0, 0; -c * d, a * d, a * d - 1; 0, 1, 1] := by + simpa only [w3, Fin.isValue, zero_ne_one, ↓reduceIte, hw2, neg_mul, of_apply, + cons_val', cons_val_zero, cons_val_fin_one, cons_val_one, cons_val, mul_zero, + add_zero, Fin.reduceEq, one_mul, add_sub_cancel, mul_one, zero_add] using + specialLinear_mul_transvection_three w2 + (show (2 : Fin 3) ≠ 1 by decide) 1 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 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 + have hw4 : (w4 : Matrix (Fin 3) (Fin 3) R) = + !![1, 0, 0; -c * d, a * d, -1; 0, 1, 0] := by + have hcancel : a * d - 1 + -(a * d) = (-1 : R) := by ring + simpa only [w4, Fin.isValue, Fin.reduceEq, ↓reduceIte, hw3, neg_mul, of_apply, + cons_val', cons_val_zero, cons_val_fin_one, cons_val_one, cons_val, + mul_zero, add_zero, one_mul, mul_one, add_neg_cancel, neg_zero, hcancel] using + specialLinear_mul_transvection_three w3 + (show (1 : Fin 3) ≠ 2 by decide) (-1) 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 - ring - have hmiddleCenter : -(c * d * b) + a * d * (ap * d) = d := by - linear_combination d * hdet - have hw5 (i j : Fin 3) : - w5 i j = !![a, b, 0; 0, d, -1; c, ap * d, 0] i j := by - dsimp only [w5] - rw [Matrix.SpecialLinearGroup.coe_mul] - fin_cases i <;> fin_cases j <;> - 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] + have hw5 : (w5 : Matrix (Fin 3) (Fin 3) R) = + !![a, b, 0; 0, d, -1; c, ap * d, 0] := by + change (w4 : Matrix (Fin 3) (Fin 3) R) * !![a, b, 0; c, ap * d, 0; 0, 0, 1] = _ + rw [hw4] + exact mennicke_first_block_product a ap b c d hdet 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 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 + have hw6 : (w6 : Matrix (Fin 3) (Fin 3) R) = + !![a, b, b; 0, d, d - 1; c, ap * d, ap * d] := by + simpa only [w6, Fin.isValue, Fin.reduceEq, ↓reduceIte, hw5, of_apply, cons_val', + cons_val_zero, cons_val_fin_one, cons_val_one, cons_val, + one_mul, zero_add, neg_add_eq_sub] using + specialLinear_mul_transvection_three w5 + (show (1 : Fin 3) ≠ 2 by decide) 1 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 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] + have hw7 : (w7 : Matrix (Fin 3) (Fin 3) R) = + !![a, 0, b; 0, 1, d - 1; c, 0, ap * d] := by + simpa only [w7, Fin.isValue, zero_ne_one, ↓reduceIte, hw6, of_apply, cons_val', + cons_val_zero, cons_val_fin_one, cons_val_one, cons_val, neg_mul, one_mul, + add_neg_cancel, Fin.reduceEq, neg_sub, add_sub_cancel] using + specialLinear_mul_transvection_three w6 + (show (2 : Fin 3) ≠ 1 by decide) (-1) 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 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] + have hw8 : (w8 : Matrix (Fin 3) (Fin 3) R) = + !![a, 0, b; 0, 1, d; c, 0, ap * d] := by + simpa only [w8, Fin.isValue, Fin.reduceEq, ↓reduceIte, hw7, of_apply, cons_val', + cons_val_zero, cons_val_fin_one, cons_val_one, cons_val, + mul_zero, add_zero, mul_one, sub_add_cancel] using + specialLinear_mul_transvection_three w7 + (show (1 : Fin 3) ≠ 2 by decide) 1 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 = - !![a * ap, a * b, b; c, a * d, d; ap * c, b * c, ap * d] i j := by - dsimp only [w9] - rw [Matrix.SpecialLinearGroup.coe_mul] - fin_cases i <;> fin_cases j <;> - 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 + have hw9 : (w9 : Matrix (Fin 3) (Fin 3) R) = + !![a * ap, a * b, b; c, a * d, d; ap * c, b * c, ap * d] := by + change (w8 : Matrix (Fin 3) (Fin 3) R) * !![ap, b, 0; c, a * d, 0; 0, 0, 1] = _ + rw [hw8] + exact mennicke_second_block_product a ap b c d let w10 := w9 * Matrix.SpecialLinearGroup.transvection (show (1 : Fin 3) ≠ 2 by decide) (-1) - have hw10 (i j : Fin 3) : w10 i j = + have hw10 : (w10 : Matrix (Fin 3) (Fin 3) R) = !![a * ap, a * b, b - a * b; c, a * d, d - a * d; - 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 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 + ap * c, b * c, ap * d - b * c] := by + simpa only [w10, Fin.isValue, Fin.reduceEq, ↓reduceIte, hw9, of_apply, cons_val', + cons_val_zero, cons_val_fin_one, cons_val_one, cons_val, + neg_mul, one_mul, ← sub_eq_add_neg] using + specialLinear_mul_transvection_three w9 + (show (1 : Fin 3) ≠ 2 by decide) (-1) let w11 := w10 * Matrix.SpecialLinearGroup.transvection (show (2 : Fin 3) ≠ 1 by decide) 1 - have hw11 (i j : Fin 3) : w11 i j = + have hw11 : (w11 : Matrix (Fin 3) (Fin 3) R) = !![a * ap, b, b - a * b; c, d, d - a * d; - 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 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] + ap * c, ap * d, ap * d - b * c] := by + simpa only [w11, Fin.isValue, zero_ne_one, ↓reduceIte, hw10, of_apply, cons_val', + cons_val_zero, cons_val_fin_one, cons_val_one, cons_val, one_mul, + add_sub_cancel, Fin.reduceEq] using + specialLinear_mul_transvection_three w10 + (show (2 : Fin 3) ≠ 1 by decide) 1 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 @@ -5980,38 +6110,35 @@ private theorem parkWoodburn_mennicke_identity ring have hbottomRight : ap * d - b * c + (a - 1) * (ap * d) = 1 := by linear_combination hdet - have hw12 (i j : Fin 3) : - w12 i j = !![a * ap, b, 0; c, d, 0; ap * c, ap * d, 1] i j := by - dsimp only [w12] - rw [specialLinear_mul_transvection_apply] - fin_cases i <;> fin_cases j <;> - 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] + have hw12 : (w12 : Matrix (Fin 3) (Fin 3) R) = + !![a * ap, b, 0; c, d, 0; ap * c, ap * d, 1] := by + simpa only [w12, Fin.isValue, Fin.reduceEq, ↓reduceIte, hw11, of_apply, cons_val', + cons_val_zero, cons_val_fin_one, cons_val_one, cons_val, + htopRight, hmiddleRight, hbottomRight] using + specialLinear_mul_transvection_three w11 + (show (1 : Fin 3) ≠ 2 by decide) (a - 1) 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 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] + have hw13 : (w13 : Matrix (Fin 3) (Fin 3) R) = + !![a * ap, b, 0; c, d, 0; 0, ap * d, 1] := by + simpa only [w13, Fin.isValue, ↓reduceIte, hw12, of_apply, cons_val', cons_val_zero, + cons_val_fin_one, neg_mul, cons_val, mul_zero, add_zero, one_ne_zero, + cons_val_one, Fin.reduceEq, mul_one, add_neg_cancel] using + specialLinear_mul_transvection_three w12 + (show (2 : Fin 3) ≠ 0 by decide) (-ap * c) 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 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] + have hw14 : (w14 : Matrix (Fin 3) (Fin 3) R) = + !![a * ap, b, 0; c, d, 0; 0, 0, 1] := by + simpa only [w14, Fin.isValue, zero_ne_one, ↓reduceIte, hw13, of_apply, cons_val', + cons_val_zero, cons_val_fin_one, cons_val_one, cons_val, mul_zero, add_zero, + Fin.reduceEq, mul_one, add_neg_cancel] using + specialLinear_mul_transvection_three w13 + (show (2 : Fin 3) ≠ 1 by decide) (-(ap * d)) change mennickeBlock (a * ap) b c d hdet = w14 apply Matrix.SpecialLinearGroup.ext intro i j - exact (hw14 i j).symm + exact congrFun (congrFun hw14.symm i) j /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem mennickeWord_mem @@ -6085,8 +6212,9 @@ private theorem mennickeBlock_rotation_conjugate Matrix.SpecialLinearGroup.transvection_inv] apply Matrix.SpecialLinearGroup.ext intro i j - fin_cases i <;> fin_cases j <;> - simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, ← mul_assoc, + revert i j + refine MennickeIdentity.matrix_three_entrywise _ _ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ <;> + simp only [Fin.isValue, ← mul_assoc, specialLinear_mul_transvection_apply, Fin.reduceEq, ↓reduceIte] <;> simp only [mul_assoc] <;> simp only [specialLinear_transvection_mul_apply, Fin.isValue, Fin.reduceEq, ↓reduceIte] <;> @@ -6310,7 +6438,7 @@ private theorem natDegree_sub_shiftedLeadingCancellationQuotient_mul_lt g.natDegree := by let r : A[X] := g - shiftedLeadingCancellationQuotient f g c * f by_cases hr : r = 0 - · simpa [r, hr] using hgpos + · simpa only [r, hr, natDegree_zero, gt_iff_lt] using hgpos · apply (Polynomial.natDegree_lt_iff_degree_lt hr).mpr rw [← Polynomial.degree_eq_natDegree hg] exact degree_sub_shiftedLeadingCancellationQuotient_mul_lt @@ -6457,8 +6585,9 @@ private theorem unitEntry_diagonalUnitPair_apply if i = j then 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.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + revert i j + refine MennickeIdentity.matrix_three_entrywise _ _ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ <;> + simp only [unitEntry_diagonalUnitPair, Fin.isValue, 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, @@ -6515,12 +6644,17 @@ private theorem stabilizedTwoByTwo_mem_elementaryThree_of_topLeft_isUnit have hb : b = l * d * u := by apply Matrix.SpecialLinearGroup.ext intro i j - fin_cases i <;> fin_cases j <;> - simp [l, d, u, unitEntry_diagonalUnitPair_apply, - Matrix.SpecialLinearGroup.transvection_coe, - Matrix.mul_apply, Fin.sum_univ_succ, - Matrix.single_apply, Matrix.one_apply, - hrow, hcolumn, a, ← hzeroOne, ← honeZero, ← honeOne] + revert i j + refine MennickeIdentity.matrix_three_entrywise _ _ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ <;> + simp only [l, d, u, unitEntry_diagonalUnitPair_apply, + Matrix.SpecialLinearGroup.transvection_coe, Matrix.mul_apply, Fin.sum_univ_succ, + Matrix.single_apply, Matrix.one_apply, hrow, hcolumn, a, ← hzeroOne, ← honeZero, ← + honeOne, Fin.isValue, SpecialLinearGroup.coe_mul, SpecialLinearGroup.transvection_coe, + Matrix.add_apply, one_ne_zero, false_and, add_zero, + IsUnit.unit_spec, mul_ite, ite_mul, one_mul, zero_mul, mul_one, mul_zero, + Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte, and_false, single_apply, and_true, + zero_ne_one, zero_add, Fin.succ_ne_zero, Fin.succ_zero_eq_one, Finset.univ_unique, + Fin.default_eq_zero, Finset.sum_singleton, Fin.succ_one_eq_two, Fin.reduceEq, true_and] rw [hb] exact (StabilizedBlockReduction.elementaryThreeSubgroup R).mul_mem ((StabilizedBlockReduction.elementaryThreeSubgroup R).mul_mem hl hd) hu' @@ -6534,9 +6668,13 @@ private theorem mennickeBlock_mem_of_isUnit_topLeft apply stabilizedTwoByTwo_mem_elementaryThree_of_topLeft_isUnit (MennickeIdentity.mennickeBlock a b c d hdet) · intro j - fin_cases j <;> simp [MennickeIdentity.mennickeBlock] + fin_cases j <;> simp only [MennickeIdentity.mennickeBlock, Fin.isValue, Fin.zero_eta, + of_apply, cons_val', cons_val_zero, cons_val_fin_one, cons_val, + cons_val_one, Fin.reduceEq, ↓reduceIte, Fin.mk_one, Fin.reduceFinMk] · intro i - fin_cases i <;> simp [MennickeIdentity.mennickeBlock] + fin_cases i <;> simp only [MennickeIdentity.mennickeBlock, Fin.zero_eta, Fin.isValue, + of_apply, cons_val', cons_val, cons_val_fin_one, cons_val_zero, + Fin.reduceEq, ↓reduceIte, Fin.mk_one, cons_val_one, Fin.reduceFinMk] · exact ha /-- Cross-module support for the infinite Connes-rigidity construction. -/ @@ -6631,8 +6769,9 @@ private theorem mennickeBlock_X_constant_shear_mul mennickeBlock a g p X hdet := by apply Matrix.SpecialLinearGroup.ext intro i j - fin_cases i <;> fin_cases j <;> - simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + revert i j + refine MennickeIdentity.matrix_three_entrywise _ _ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ <;> + simp only [Fin.isValue, 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] <;> @@ -6688,7 +6827,7 @@ private theorem mennickeBlock_mem_of_isUnit_bottomRight have hconjugate := mennickeBlock_rotation_conjugate d b c a hswapped have hmem := E.mul_mem (E.mul_mem hJ hunit) (E.inv_mem hJ) - simpa [J, hconjugate] using hmem + simpa only [J, hconjugate] using hmem /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem mennickeBlock_mem_of_bottomRight_X_pow @@ -6908,11 +7047,12 @@ private theorem suslin_local_stabilizedTwo_unit_offdiag_normalization refine ⟨b * j, (stabilizedTwoHom j)⁻¹, (elementaryThreeSubgroup (Polynomial A)).inv_mem hj, ?_, ?_, ?_⟩ - · simp [map_mul] - · simpa [j] using hdiag.1 - · simpa [j] using hdiag.2.neg + · simp only [map_mul, mul_inv_cancel_right] + · simpa only [j, Fin.isValue, suslin_mul_signedSwap_zero_one] using hdiag.1 + · simpa only [j, Fin.isValue, suslin_mul_signedSwap_one_zero, coeff_neg, + IsUnit.neg_iff] using hdiag.2.neg · exact ⟨b, 1, (elementaryThreeSubgroup (Polynomial A)).one_mem, - by simp, hoff.1, hoff.2⟩ + by simp only [mul_one], hoff.1, hoff.2⟩ end @@ -7032,8 +7172,9 @@ private theorem suslin_uniformizer_column_shear dsimp apply Matrix.SpecialLinearGroup.ext intro i j - fin_cases i <;> fin_cases j <;> - simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + revert i j + refine MennickeIdentity.matrix_three_entrywise _ _ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ <;> + 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, Matrix.cons_val] <;> @@ -7448,8 +7589,9 @@ private theorem mennickeBlock_rowSecond_sub_mul mennickeBlock a b c d hdet := by apply Matrix.SpecialLinearGroup.ext intro i j - fin_cases i <;> fin_cases j <;> - simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + revert i j + refine MennickeIdentity.matrix_three_entrywise _ _ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ <;> + simp only [Fin.isValue, 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] <;> @@ -7465,8 +7607,9 @@ private theorem mennickeBlock_columnFirst_sub_mul (show (1 : Fin 3) ≠ 0 by decide) (-q) := by apply Matrix.SpecialLinearGroup.ext intro i j - fin_cases i <;> fin_cases j <;> - simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + revert i j + refine MennickeIdentity.matrix_three_entrywise _ _ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ <;> + 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, Matrix.cons_val] <;> @@ -7703,11 +7846,17 @@ private theorem mennickeBlock_secondColumnSub_mem_iff 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.single_apply, Matrix.one_apply] <;> ring + revert i j + refine MennickeIdentity.matrix_three_entrywise _ _ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ <;> + simp only [mennickeBlock, Matrix.SpecialLinearGroup.transvection_coe, Matrix.mul_apply, + Fin.sum_univ_succ, Matrix.single_apply, Matrix.one_apply, Fin.isValue, + SpecialLinearGroup.transvection_coe, of_apply, cons_val', cons_val_fin_one, cons_val_zero, + Matrix.add_apply, one_ne_zero, and_false, add_zero, + mul_ite, mul_one, mul_zero, Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte, single_apply, + and_true, zero_ne_one, zero_add, mul_neg, cons_val_succ, Fin.succ_zero_eq_one, + Finset.univ_unique, Fin.default_eq_zero, zero_mul, Finset.sum_const_zero, cons_val_one, + Fin.reduceEq, cons_val, neg_zero, one_mul, Finset.sum_singleton, + Fin.succ_one_eq_two] <;> ring rw [← hmul] exact (E.mul_mem_cancel_right hroot).symm @@ -7920,8 +8069,9 @@ private theorem mennickeBlock_mul_columnSubtract (mennickeBlock_columnSubtract_det f g p q t hdet) := by apply Matrix.SpecialLinearGroup.ext intro i j - fin_cases i <;> fin_cases j <;> - simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + revert i j + refine MennickeIdentity.matrix_three_entrywise _ _ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ <;> + 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, Matrix.cons_val] <;> @@ -7946,7 +8096,7 @@ private theorem mennickeBlock_columnSubtract_mem_iff exact E.mul_mem h hz · intro h have h' := E.mul_mem h (E.inv_mem hz) - simpa [z, mul_assoc] using h' + simpa only [z, mul_assoc, Fin.isValue, mul_inv_cancel, mul_one] using h' /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem mennickeBlock_shifted_det @@ -7979,7 +8129,10 @@ private theorem mennickeBlock_shifted_mem_iff (mennickeBlock_shifted_det f g p q f₁ t s hdet hshift) := by apply Matrix.SpecialLinearGroup.ext intro i j - fin_cases i <;> fin_cases j <;> simp [mennickeBlock, hfirst] + revert i j + refine MennickeIdentity.matrix_three_entrywise _ _ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ <;> + simp only [mennickeBlock, hfirst, Fin.isValue, of_apply, cons_val', cons_val_zero, + cons_val_fin_one, cons_val_one, cons_val] rw [hblock] at h exact h @@ -8027,7 +8180,8 @@ private theorem stabilizedTwoHom_eq_mennickeBlock exact hdet) := by apply Matrix.SpecialLinearGroup.ext intro i j - fin_cases i <;> fin_cases j + revert i j + refine MennickeIdentity.matrix_three_entrywise _ _ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ · exact stabilizedTwoHom_castSucc_castSucc b 0 0 · exact stabilizedTwoHom_castSucc_castSucc b 0 1 · exact stabilizedTwoHom_castSucc_two b 0 @@ -8151,8 +8305,10 @@ private theorem valuation_mennicke_outer_induction hdetfactor := by apply Matrix.SpecialLinearGroup.ext intro j k - fin_cases j <;> fin_cases k <;> - simp [MennickeIdentity.mennickeBlock, hshape] + revert j k + refine MennickeIdentity.matrix_three_entrywise _ _ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ <;> + simp only [MennickeIdentity.mennickeBlock, hshape, mennickeBlock, Fin.isValue, + of_apply, cons_val', cons_val_zero, cons_val_fin_one, cons_val_one, cons_val] rw [hblock] exact hfactored intro f g p q hdet hg₀ @@ -8389,9 +8545,12 @@ private theorem lastRowClear_mul_apply (Matrix.transvection (2 : Fin 3) 0 (-(g 2 0)) * Matrix.transvection (2 : Fin 3) 1 (-(g 2 1)))) i j = _ simp only [← mul_assoc] - fin_cases i <;> fin_cases j <;> - simp [Matrix.mul_transvection_apply_same, - Matrix.mul_transvection_apply_of_ne, h0, h1, h2] + revert i j + refine MennickeIdentity.matrix_three_entrywise _ _ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ <;> + simp only [Matrix.mul_transvection_apply_same, Matrix.mul_transvection_apply_of_ne, h0, h1, + h2, Fin.isValue, ne_eq, zero_ne_one, not_false_eq_true, mul_transvection_apply_of_ne, + mul_transvection_apply_same, Fin.reduceEq, ↓reduceIte, mul_zero, add_zero, one_ne_zero, + mul_one, add_neg_cancel] /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem upperLeft_det_eq_one @@ -8425,8 +8584,12 @@ private theorem lastColumn_block_decomposition intro i j rw [lastRowClear_mul_apply g hcolumn] cases i using Fin.lastCases <;> cases j using Fin.lastCases <;> - simp [stabilizedTwoHom, stabilizedTwoSpecialLinear, stabilizedTwoMatrix, - upperLeftSpecialLinear, Matrix.submatrix, hcolumn] + simp only [stabilizedTwoHom, stabilizedTwoSpecialLinear, stabilizedTwoMatrix, + upperLeftSpecialLinear, Matrix.submatrix, hcolumn, Fin.reduceLast, Fin.isValue, ↓reduceIte, + submatrix, MonoidHom.coe_mk, OneHom.coe_mk, Nat.reduceAdd, reindex_apply, of_apply, + finTwoPlusOne_symm_two, fromBlocks_apply₂₂, one_apply_eq, finTwo_castSucc_ne_two, + finSumFinEquiv_symm_apply_castSucc, fromBlocks_apply₂₁, Matrix.zero_apply, + fromBlocks_apply₁₂, fromBlocks_apply₁₁] /-- Cross-module support for the infinite Connes-rigidity construction. -/ public @@ -8923,9 +9086,9 @@ private theorem normalizeSigns_mem (g : IGroup) : normalizeSigns g ∈ elementar unfold normalizeSigns apply elementary.mul_mem · apply elementary.mul_mem - · split_ifs <;> simp [signFlip_mem] - · split_ifs <;> simp [signFlip_mem] - · split_ifs <;> simp [signFlip_mem] + · split_ifs <;> simp only [signFlip_mem, Fin.isValue, one_mem] + · split_ifs <;> simp only [signFlip_mem, Fin.isValue, one_mem] + · split_ifs <;> simp only [signFlip_mem, Fin.isValue, one_mem] /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem normalizeSigns_preserves_upper (g : IGroup) @@ -8938,18 +9101,19 @@ private theorem normalizeSigns_preserves_upper (g : IGroup) dsimp [f₁] split_ifs · exact signFlip_preserves_upper 0 1 _ g hg - · simpa using hg + · simpa only [SpecialLinearGroup.coe_one, one_mul] using hg have h₂ : ∀ a b : Index, b < a → (f₂ * (f₁ * g)) a b = 0 := by dsimp [f₂] split_ifs · exact signFlip_preserves_upper 0 2 _ (f₁ * g) h₁ - · simpa using h₁ + · simpa only [SpecialLinearGroup.coe_one, one_mul, SpecialLinearGroup.coe_mul] using h₁ have h₃ : ∀ a b : Index, b < a → (f₃ * (f₂ * (f₁ * g))) a b = 0 := by dsimp [f₃] split_ifs · exact signFlip_preserves_upper 0 3 _ (f₂ * (f₁ * g)) h₂ - · simpa using h₂ - simpa [normalizeSigns, f₁, f₂, f₃, mul_assoc] using h₃ + · simpa only [SpecialLinearGroup.coe_one, one_mul, SpecialLinearGroup.coe_mul] using h₂ + simpa only [normalizeSigns, f₁, f₂, f₃, mul_assoc, Fin.isValue, Int.reduceNeg, mul_ite, ite_mul, + one_mul, mul_one] using h₃ /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem normalizeSigns_diag_one (g : IGroup) @@ -8976,19 +9140,22 @@ private theorem normalizeSigns_diag_one (g : IGroup) simp only [mul_assoc] rcases h1 with h1 | h1 <;> rcases h2 with h2 | h2 <;> rcases h3 with h3 | h3 <;> - simp [h1, h2, h3, signFlip_mul_apply] + simp only [h1, h2, h3, signFlip_mul_apply, Fin.isValue, Int.reduceNeg, reduceCtorEq, + ↓reduceIte, one_mul, one_ne_zero, Fin.reduceEq, or_self, or_true, neg_neg] have hdiag2 : (normalizeSigns g * g) (2 : Index) 2 = 1 := by unfold normalizeSigns simp only [mul_assoc] rcases h1 with h1 | h1 <;> rcases h2 with h2 | h2 <;> rcases h3 with h3 | h3 <;> - simp [h1, h2, h3, signFlip_mul_apply] + simp only [h1, h2, h3, signFlip_mul_apply, Fin.isValue, Int.reduceNeg, reduceCtorEq, + ↓reduceIte, one_mul, Fin.reduceEq, or_self, or_true, neg_neg] have hdiag3 : (normalizeSigns g * g) (3 : Index) 3 = 1 := by unfold normalizeSigns simp only [mul_assoc] rcases h1 with h1 | h1 <;> rcases h2 with h2 | h2 <;> rcases h3 with h3 | h3 <;> - simp [h1, h2, h3, signFlip_mul_apply] + simp only [h1, h2, h3, signFlip_mul_apply, Fin.isValue, Int.reduceNeg, reduceCtorEq, + ↓reduceIte, one_mul, Fin.reduceEq, or_true, neg_neg, or_self] norm_num [Fin.prod_univ_succ] at hprod change (normalizeSigns g * g) 0 0 * ((normalizeSigns g * g) 1 1 * @@ -9001,17 +9168,20 @@ private theorem normalizeSigns_diag_one (g : IGroup) simp only [mul_assoc] rcases h1 with h1 | h1 <;> rcases h2 with h2 | h2 <;> rcases h3 with h3 | h3 <;> - simp [h1, h2, h3, signFlip_mul_apply] + simp only [h1, h2, h3, signFlip_mul_apply, Fin.isValue, Int.reduceNeg, reduceCtorEq, + ↓reduceIte, one_mul, Fin.mk_one, one_ne_zero, Fin.reduceEq, or_self, or_true, neg_neg] · unfold normalizeSigns simp only [mul_assoc] rcases h1 with h1 | h1 <;> rcases h2 with h2 | h2 <;> rcases h3 with h3 | h3 <;> - simp [h1, h2, h3, signFlip_mul_apply] + simp only [h1, h2, h3, signFlip_mul_apply, Fin.isValue, Int.reduceNeg, reduceCtorEq, + ↓reduceIte, one_mul, Fin.reduceFinMk, Fin.reduceEq, or_self, or_true, neg_neg] · unfold normalizeSigns simp only [mul_assoc] rcases h1 with h1 | h1 <;> rcases h2 with h2 | h2 <;> rcases h3 with h3 | h3 <;> - simp [h1, h2, h3, signFlip_mul_apply] + simp only [h1, h2, h3, signFlip_mul_apply, Fin.isValue, Int.reduceNeg, reduceCtorEq, + ↓reduceIte, one_mul, Fin.reduceFinMk, Fin.reduceEq, or_true, neg_neg, or_self] /-- Cross-module support for the infinite Connes-rigidity construction. -/ public @@ -9043,8 +9213,10 @@ theorem upperUnitriangular_factorization (g : IGroup) have h32 := hu 3 2 (by decide) apply Matrix.SpecialLinearGroup.ext intro i j - fin_cases i <;> fin_cases j <;> - simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, + revert i j + refine matrix_four_entrywise _ _ + ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ <;> + simp only [Fin.isValue, 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,