From 7f9bfd340328a967fcdc37d2a16dedb4bd323f61 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 7 Aug 2024 10:57:09 +0000 Subject: [PATCH] chore: backports for leanprover/lean4#4814 (part 25) (#15537) --- Mathlib/Algebra/Lie/Submodule.lean | 88 ++++++----- .../EllipticCurve/Jacobian.lean | 6 +- .../InnerProductSpace/Orientation.lean | 4 +- .../Normed/Algebra/TrivSqZeroExt.lean | 8 +- .../Normed/Algebra/UnitizationL1.lean | 4 +- Mathlib/Analysis/Normed/Lp/PiLp.lean | 4 +- Mathlib/Analysis/NormedSpace/DualNumber.lean | 2 +- .../Combinatorics/Additive/Corner/Roth.lean | 6 +- Mathlib/FieldTheory/Perfect.lean | 7 +- .../Geometry/Manifold/InteriorBoundary.lean | 2 +- .../QuadraticForm/TensorProduct.lean | 8 +- Mathlib/LinearAlgebra/Trace.lean | 10 +- Mathlib/MeasureTheory/Constructions/Pi.lean | 11 +- .../Constructions/Prod/Basic.lean | 6 +- Mathlib/MeasureTheory/Group/Measure.lean | 3 + .../Measure/HasOuterApproxClosed.lean | 4 +- Mathlib/RingTheory/Kaehler/Basic.lean | 13 +- Mathlib/RingTheory/Unramified/Finite.lean | 53 +++---- Mathlib/RingTheory/WittVector/Basic.lean | 16 +- Mathlib/RingTheory/WittVector/InitTail.lean | 10 +- .../RingTheory/WittVector/Teichmuller.lean | 4 +- .../RingTheory/WittVector/Verschiebung.lean | 9 +- .../MetricSpace/GromovHausdorffRealized.lean | 143 ++++++++++-------- 23 files changed, 246 insertions(+), 175 deletions(-) diff --git a/Mathlib/Algebra/Lie/Submodule.lean b/Mathlib/Algebra/Lie/Submodule.lean index 3bc21e9da307d..08978bd95d8ba 100644 --- a/Mathlib/Algebra/Lie/Submodule.lean +++ b/Mathlib/Algebra/Lie/Submodule.lean @@ -36,8 +36,8 @@ universe u v w w₁ w₂ section LieSubmodule variable (R : Type u) (L : Type v) (M : Type w) -variable [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] -variable [LieRingModule L M] [LieModule R L M] +variable [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] +variable [LieRingModule L M] /-- A Lie submodule of a Lie module is a submodule that is closed under the Lie bracket. This is a sufficient condition for the subset itself to form a Lie module. -/ @@ -169,10 +169,6 @@ instance {S : Type*} [Semiring S] [SMul S R] [SMul Sᵐᵒᵖ R] [Module S M] [M [IsScalarTower S R M] [IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M] : IsCentralScalar S N := N.toSubmodule.isCentralScalar -instance instLieModule : LieModule R L N where - lie_smul := by intro t x y; apply SetCoe.ext; apply lie_smul - smul_lie := by intro t x y; apply SetCoe.ext; apply smul_lie - @[simp, norm_cast] theorem coe_zero : ((0 : N) : M) = (0 : M) := rfl @@ -197,12 +193,19 @@ theorem coe_smul (t : R) (m : N) : (↑(t • m) : M) = t • (m : M) := theorem coe_bracket (x : L) (m : N) : (↑⁅x, m⁆ : M) = ⁅x, ↑m⁆ := rfl +variable [LieAlgebra R L] [LieModule R L M] + +instance instLieModule : LieModule R L N where + lie_smul := by intro t x y; apply SetCoe.ext; apply lie_smul + smul_lie := by intro t x y; apply SetCoe.ext; apply smul_lie + instance [Subsingleton M] : Unique (LieSubmodule R L M) := ⟨⟨0⟩, fun _ ↦ (coe_toSubmodule_eq_iff _ _).mp (Subsingleton.elim _ _)⟩ end LieSubmodule section LieIdeal +variable [LieAlgebra R L] [LieModule R L M] /-- An ideal of a Lie algebra is a Lie submodule of the Lie algebra as a Lie module over itself. -/ abbrev LieIdeal := @@ -265,6 +268,7 @@ theorem Submodule.exists_lieSubmodule_coe_eq_iff (p : Submodule R M) : namespace LieSubalgebra variable {L} +variable [LieAlgebra R L] variable (K : LieSubalgebra R L) /-- Given a Lie subalgebra `K ⊆ L`, if we view `L` as a `K`-module by restriction, it contains @@ -301,9 +305,9 @@ end LieSubmodule namespace LieSubmodule variable {R : Type u} {L : Type v} {M : Type w} -variable [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] -variable [LieRingModule L M] [LieModule R L M] -variable (N N' : LieSubmodule R L M) (I J : LieIdeal R L) +variable [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] +variable [LieRingModule L M] +variable (N N' : LieSubmodule R L M) section LatticeStructure @@ -741,9 +745,9 @@ end LieSubmodule section LieSubmoduleMapAndComap variable {R : Type u} {L : Type v} {L' : Type w₂} {M : Type w} {M' : Type w₁} -variable [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] -variable [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] -variable [AddCommGroup M'] [Module R M'] [LieRingModule L M'] [LieModule R L M'] +variable [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] +variable [AddCommGroup M] [Module R M] [LieRingModule L M] +variable [AddCommGroup M'] [Module R M'] [LieRingModule L M'] namespace LieSubmodule @@ -884,6 +888,7 @@ Submodules. -/ end LieSubmodule namespace LieIdeal +variable [LieAlgebra R L] [LieModule R L M] [LieModule R L M'] variable (f : L →ₗ⁅R⁆ L') (I I₂ : LieIdeal R L) (J : LieIdeal R L') @@ -988,7 +993,7 @@ instance subsingleton_of_bot : Subsingleton (LieIdeal R (⊥ : LieIdeal R L)) := end LieIdeal namespace LieHom - +variable [LieAlgebra R L] [LieModule R L M] [LieModule R L M'] variable (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L) (J : LieIdeal R L') /-- The kernel of a morphism of Lie algebras, as an ideal in the domain. -/ @@ -1090,7 +1095,7 @@ theorem isIdealMorphism_of_surjective (h : Function.Surjective f) : f.IsIdealMor end LieHom namespace LieIdeal - +variable [LieAlgebra R L] [LieModule R L M] [LieModule R L M'] variable {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} {J : LieIdeal R L'} @[simp] @@ -1223,9 +1228,9 @@ end LieSubmoduleMapAndComap namespace LieModuleHom variable {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} -variable [CommRing R] [LieRing L] [LieAlgebra R L] -variable [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] -variable [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] +variable [CommRing R] [LieRing L] +variable [AddCommGroup M] [Module R M] [LieRingModule L M] +variable [AddCommGroup N] [Module R N] [LieRingModule L N] variable (f : M →ₗ⁅R,L⁆ N) /-- The kernel of a morphism of Lie algebras, as an ideal in the domain. -/ @@ -1299,8 +1304,8 @@ end LieModuleHom namespace LieSubmodule variable {R : Type u} {L : Type v} {M : Type w} -variable [CommRing R] [LieRing L] [LieAlgebra R L] -variable [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] +variable [CommRing R] [LieRing L] +variable [AddCommGroup M] [Module R M] [LieRingModule L M] variable (N : LieSubmodule R L M) @[simp] @@ -1339,8 +1344,30 @@ end LieSubmodule section TopEquiv -variable {R : Type u} {L : Type v} -variable [CommRing R] [LieRing L] [LieAlgebra R L] +variable (R : Type u) (L : Type v) +variable [CommRing R] [LieRing L] + +variable (M : Type*) [AddCommGroup M] [Module R M] [LieRingModule L M] + +/-- The natural equivalence between the 'top' Lie submodule and the enclosing Lie module. -/ +def LieModuleEquiv.ofTop : (⊤ : LieSubmodule R L M) ≃ₗ⁅R,L⁆ M := + { LinearEquiv.ofTop ⊤ rfl with + map_lie' := rfl } + +variable {R L} + +-- This lemma has always been bad, but leanprover/lean4#2644 made `simp` start noticing +@[simp, nolint simpNF] lemma LieModuleEquiv.ofTop_apply (x : (⊤ : LieSubmodule R L M)) : + LieModuleEquiv.ofTop R L M x = x := + rfl + +@[simp] lemma LieModuleEquiv.range_coe {M' : Type*} + [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (e : M ≃ₗ⁅R,L⁆ M') : + LieModuleHom.range (e : M →ₗ⁅R,L⁆ M') = ⊤ := by + rw [LieModuleHom.range_eq_top] + exact e.surjective + +variable [LieAlgebra R L] [LieModule R L M] /-- The natural equivalence between the 'top' Lie subalgebra and the enclosing Lie algebra. @@ -1366,23 +1393,4 @@ def LieIdeal.topEquiv : (⊤ : LieIdeal R L) ≃ₗ⁅R⁆ L := theorem LieIdeal.topEquiv_apply (x : (⊤ : LieIdeal R L)) : LieIdeal.topEquiv x = x := rfl -variable (R L) -variable (M : Type*) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] - -/-- The natural equivalence between the 'top' Lie submodule and the enclosing Lie module. -/ -def LieModuleEquiv.ofTop : (⊤ : LieSubmodule R L M) ≃ₗ⁅R,L⁆ M := - { LinearEquiv.ofTop ⊤ rfl with - map_lie' := rfl } - --- This lemma has always been bad, but leanprover/lean4#2644 made `simp` start noticing -@[simp, nolint simpNF] lemma LieModuleEquiv.ofTop_apply (x : (⊤ : LieSubmodule R L M)) : - LieModuleEquiv.ofTop R L M x = x := - rfl - -@[simp] lemma LieModuleEquiv.range_coe {M' : Type*} - [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (e : M ≃ₗ⁅R,L⁆ M') : - LieModuleHom.range (e : M →ₗ⁅R,L⁆ M') = ⊤ := by - rw [LieModuleHom.range_eq_top] - exact e.surjective - end TopEquiv diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean index 2154fb228839b..38abc3bb0ed03 100644 --- a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean +++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean @@ -112,7 +112,7 @@ local macro "pderiv_simp" : tactic => pderiv_X_of_ne (by decide : z ≠ x), pderiv_X_of_ne (by decide : x ≠ z), pderiv_X_of_ne (by decide : z ≠ y), pderiv_X_of_ne (by decide : y ≠ z)]) -variable {R : Type u} [CommRing R] {W' : Jacobian R} {F : Type v} [Field F] {W : Jacobian F} +variable {R : Type u} {W' : Jacobian R} {F : Type v} [Field F] {W : Jacobian F} section Jacobian @@ -127,6 +127,8 @@ lemma fin3_def_ext (X Y Z : R) : ![X, Y, Z] x = X ∧ ![X, Y, Z] y = Y ∧ ![X, lemma comp_fin3 {S} (f : R → S) (X Y Z : R) : f ∘ ![X, Y, Z] = ![f X, f Y, f Z] := (FinVec.map_eq _ _).symm +variable [CommRing R] + /-- The scalar multiplication on a point representative. -/ scoped instance instSMulPoint : SMul R <| Fin 3 → R := ⟨fun u P => ![u ^ 2 * P x, u ^ 3 * P y, u * P z]⟩ @@ -224,6 +226,8 @@ lemma Y_eq_iff {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0) : end Jacobian +variable [CommRing R] + section Equation /-! ### Weierstrass equations -/ diff --git a/Mathlib/Analysis/InnerProductSpace/Orientation.lean b/Mathlib/Analysis/InnerProductSpace/Orientation.lean index 4dcb286356c0b..60b27da658fe3 100644 --- a/Mathlib/Analysis/InnerProductSpace/Orientation.lean +++ b/Mathlib/Analysis/InnerProductSpace/Orientation.lean @@ -44,7 +44,7 @@ open scoped RealInnerProductSpace namespace OrthonormalBasis -variable {ι : Type*} [Fintype ι] [DecidableEq ι] [ne : Nonempty ι] (e f : OrthonormalBasis ι ℝ E) +variable {ι : Type*} [Fintype ι] [DecidableEq ι] (e f : OrthonormalBasis ι ℝ E) (x : Orientation ℝ E ι) /-- The change-of-basis matrix between two orthonormal bases with the same orientation has @@ -90,6 +90,8 @@ theorem det_eq_neg_det_of_opposite_orientation (h : e.toBasis.orientation ≠ f. simp [e.det_to_matrix_orthonormalBasis_of_opposite_orientation f h, neg_one_smul ℝ (M := E [⋀^ι]→ₗ[ℝ] ℝ)] +variable [Nonempty ι] + section AdjustToOrientation /-- `OrthonormalBasis.adjustToOrientation`, applied to an orthonormal basis, preserves the diff --git a/Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean b/Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean index 3f1aa98ec5d75..5a779b0580765 100644 --- a/Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean +++ b/Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean @@ -192,9 +192,8 @@ noncomputable section Seminormed section Ring variable [SeminormedCommRing S] [SeminormedRing R] [SeminormedAddCommGroup M] -variable [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] -variable [BoundedSMul S R] [BoundedSMul S M] [BoundedSMul R M] [BoundedSMul Rᵐᵒᵖ M] -variable [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] +variable [Algebra S R] [Module S M] +variable [BoundedSMul S R] [BoundedSMul S M] instance instL1SeminormedAddCommGroup : SeminormedAddCommGroup (tsze R M) := inferInstanceAs <| SeminormedAddCommGroup (WithLp 1 <| R × M) @@ -217,6 +216,9 @@ theorem nnnorm_def (x : tsze R M) : ‖x‖₊ = ‖fst x‖₊ + ‖snd x‖₊ @[simp] theorem nnnorm_inl (r : R) : ‖(inl r : tsze R M)‖₊ = ‖r‖₊ := by simp [nnnorm_def] @[simp] theorem nnnorm_inr (m : M) : ‖(inr m : tsze R M)‖₊ = ‖m‖₊ := by simp [nnnorm_def] +variable [Module R M] [BoundedSMul R M] [Module Rᵐᵒᵖ M] [BoundedSMul Rᵐᵒᵖ M] + [SMulCommClass R Rᵐᵒᵖ M] + instance instL1SeminormedRing : SeminormedRing (tsze R M) where norm_mul | ⟨r₁, m₁⟩, ⟨r₂, m₂⟩ => by diff --git a/Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean b/Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean index f92a28cdee905..4a0ab143ce2a1 100644 --- a/Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean +++ b/Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean @@ -24,7 +24,7 @@ non-unital Banach algebra is compact, which can be established by passing to the -/ variable (𝕜 A : Type*) [NormedField 𝕜] [NonUnitalNormedRing A] -variable [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] +variable [NormedSpace 𝕜 A] namespace WithLp @@ -79,6 +79,8 @@ lemma unitization_isometry_inr : ((WithLp.linearEquiv 1 𝕜 (Unitization 𝕜 A)).symm.comp <| Unitization.inrHom 𝕜 A) unitization_norm_inr +variable [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] + instance instUnitizationRing : Ring (WithLp 1 (Unitization 𝕜 A)) := inferInstanceAs (Ring (Unitization 𝕜 A)) diff --git a/Mathlib/Analysis/Normed/Lp/PiLp.lean b/Mathlib/Analysis/Normed/Lp/PiLp.lean index 5ceff479c7c2d..dda1bee40dc60 100644 --- a/Mathlib/Analysis/Normed/Lp/PiLp.lean +++ b/Mathlib/Analysis/Normed/Lp/PiLp.lean @@ -92,7 +92,7 @@ section for Pi types will not trigger. -/ variable {𝕜 p α} variable [SeminormedRing 𝕜] [∀ i, SeminormedAddCommGroup (β i)] -variable [∀ i, Module 𝕜 (β i)] [∀ i, BoundedSMul 𝕜 (β i)] (c : 𝕜) +variable [∀ i, Module 𝕜 (β i)] (c : 𝕜) variable (x y : PiLp p β) (i : ι) #adaptation_note @@ -744,7 +744,7 @@ variable {ι : Type*} {κ : ι → Type*} (p : ℝ≥0∞) [Fact (1 ≤ p)] variable (𝕜) in /-- `LinearEquiv.piCurry` for `PiLp`, as an isometry. -/ -def _root_.LinearIsometryEquiv.piLpCurry : +def _root_.LinearIsometryEquiv.piLpCurry : PiLp p (fun i : Sigma _ => α i.1 i.2) ≃ₗᵢ[𝕜] PiLp p (fun i => PiLp p (α i)) where toLinearEquiv := WithLp.linearEquiv _ _ _ diff --git a/Mathlib/Analysis/NormedSpace/DualNumber.lean b/Mathlib/Analysis/NormedSpace/DualNumber.lean index 4058d986db870..f81134aac4e9d 100644 --- a/Mathlib/Analysis/NormedSpace/DualNumber.lean +++ b/Mathlib/Analysis/NormedSpace/DualNumber.lean @@ -25,7 +25,7 @@ open TrivSqZeroExt variable (𝕜 : Type*) {R : Type*} variable [Field 𝕜] [CharZero 𝕜] [CommRing R] [Algebra 𝕜 R] -variable [UniformSpace R] [TopologicalRing R] [CompleteSpace R] [T2Space R] +variable [UniformSpace R] [TopologicalRing R] [T2Space R] @[simp] theorem exp_eps : exp 𝕜 (eps : DualNumber R) = 1 + eps := diff --git a/Mathlib/Combinatorics/Additive/Corner/Roth.lean b/Mathlib/Combinatorics/Additive/Corner/Roth.lean index 9abc01be4aa41..cc3a7145d5a4d 100644 --- a/Mathlib/Combinatorics/Additive/Corner/Roth.lean +++ b/Mathlib/Combinatorics/Additive/Corner/Roth.lean @@ -23,7 +23,7 @@ open Finset SimpleGraph TripartiteFromTriangles open Function hiding graph open Fintype (card) -variable {G : Type*} [AddCommGroup G] [Fintype G] {A B : Finset (G × G)} +variable {G : Type*} [AddCommGroup G] {A B : Finset (G × G)} {a b c d x y : G} {n : ℕ} {ε : ℝ} namespace Corners @@ -55,7 +55,7 @@ private lemma noAccidental (hs : IsCornerFree (A : Set (G × G))) : simp only [mk_mem_triangleIndices] at ha hb hc exact .inl $ hs ⟨hc.1, hb.1, ha.1, hb.2.symm.trans ha.2⟩ -private lemma farFromTriangleFree_graph [DecidableEq G] (hε : ε * card G ^ 2 ≤ A.card) : +private lemma farFromTriangleFree_graph [Fintype G] [DecidableEq G] (hε : ε * card G ^ 2 ≤ A.card) : (graph <| triangleIndices A).FarFromTriangleFree (ε / 9) := by refine farFromTriangleFree _ ?_ simp_rw [card_triangleIndices, mul_comm_div, Nat.cast_pow, Nat.cast_add] @@ -64,6 +64,8 @@ private lemma farFromTriangleFree_graph [DecidableEq G] (hε : ε * card G ^ 2 end Corners +variable [Fintype G] + open Corners diff --git a/Mathlib/FieldTheory/Perfect.lean b/Mathlib/FieldTheory/Perfect.lean index cf6c499537bf9..f0725115ada01 100644 --- a/Mathlib/FieldTheory/Perfect.lean +++ b/Mathlib/FieldTheory/Perfect.lean @@ -290,6 +290,7 @@ theorem roots_expand_image_frobenius_subset [DecidableEq R] : convert ← roots_expand_pow_image_iterateFrobenius_subset p 1 f apply pow_one +section PerfectRing variable {p n f} variable [PerfectRing R p] @@ -342,7 +343,9 @@ theorem roots_expand_image_frobenius [DecidableEq R] : rw [Finset.image_toFinset, roots_expand_map_frobenius, (roots f).toFinset_nsmul _ (expChar_pos R p).ne'] -variable (p n f) [DecidableEq R] +end PerfectRing + +variable [DecidableEq R] /-- If `f` is a polynomial over an integral domain `R` of characteristic `p`, then there is a map from the set of roots of `Polynomial.expand R p f` to the set of roots of `f`. @@ -367,6 +370,8 @@ noncomputable def rootsExpandPowToRoots : @[simp] theorem rootsExpandPowToRoots_apply (x) : (rootsExpandPowToRoots p n f x : R) = x ^ p ^ n := rfl +variable [PerfectRing R p] + /-- If `f` is a polynomial over a perfect integral domain `R` of characteristic `p`, then there is a bijection from the set of roots of `Polynomial.expand R p f` to the set of roots of `f`. It's given by `x ↦ x ^ p`, see `rootsExpandEquivRoots_apply`. -/ diff --git a/Mathlib/Geometry/Manifold/InteriorBoundary.lean b/Mathlib/Geometry/Manifold/InteriorBoundary.lean index aafb361508ac5..1bfcd8ec40979 100644 --- a/Mathlib/Geometry/Manifold/InteriorBoundary.lean +++ b/Mathlib/Geometry/Manifold/InteriorBoundary.lean @@ -159,7 +159,7 @@ variable {I} {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H'] {N : Type*} [TopologicalSpace N] [ChartedSpace H' N] - (J : ModelWithCorners 𝕜 E' H') [SmoothManifoldWithCorners J N] {x : M} {y : N} + (J : ModelWithCorners 𝕜 E' H') {x : M} {y : N} /-- The interior of `M × N` is the product of the interiors of `M` and `N`. -/ lemma ModelWithCorners.interior_prod : diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 54a0bb985a977..f4bca4eca0457 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -31,9 +31,11 @@ section CommRing variable [CommRing R] [CommRing A] variable [AddCommGroup M₁] [AddCommGroup M₂] variable [Algebra R A] [Module R M₁] [Module A M₁] -variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [IsScalarTower R A M₁] -variable [Module R M₂] [Invertible (2 : R)] +variable [SMulCommClass R A M₁] [IsScalarTower R A M₁] +variable [Module R M₂] +section InvertibleTwo +variable [Invertible (2 : R)] variable (R A) in /-- The tensor product of two quadratic forms injects into quadratic forms on tensor products. @@ -106,6 +108,8 @@ theorem polarBilin_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂) : ← LinearMap.map_smul, smul_tmul', ← two_nsmul_associated R, coe_associatedHom, associated_sq, smul_comm, ← smul_assoc, two_smul, invOf_two_add_invOf_two, one_smul] +end InvertibleTwo + /-- If two quadratic forms from `A ⊗[R] M₂` agree on elements of the form `1 ⊗ m`, they are equal. In other words, if a base change exists for a quadratic form, it is unique. diff --git a/Mathlib/LinearAlgebra/Trace.lean b/Mathlib/LinearAlgebra/Trace.lean index b9d42ad6884fe..9bbcd7e816372 100644 --- a/Mathlib/LinearAlgebra/Trace.lean +++ b/Mathlib/LinearAlgebra/Trace.lean @@ -145,9 +145,9 @@ theorem trace_eq_contract_of_basis' [Fintype ι] [DecidableEq ι] (b : Basis ι LinearMap.trace R M = contractLeft R M ∘ₗ (dualTensorHomEquivOfBasis b).symm.toLinearMap := by simp [LinearEquiv.eq_comp_toLinearMap_symm, trace_eq_contract_of_basis b] +section variable (R M) variable [Module.Free R M] [Module.Finite R M] [Module.Free R N] [Module.Finite R N] - [Module.Free R P] [Module.Finite R P] /-- When `M` is finite free, the trace of a linear map correspond to the contraction pairing under the isomorphism `End(M) ≃ M* ⊗ M`-/ @@ -257,10 +257,16 @@ theorem trace_comp_comm' (f : M →ₗ[R] N) (g : N →ₗ[R] M) : simp only [llcomp_apply', compr₂_apply, flip_apply] at h exact h +end + +variable {N P} + +variable [Module.Free R N] [Module.Finite R N] [Module.Free R P] [Module.Finite R P] in lemma trace_comp_cycle (f : M →ₗ[R] N) (g : N →ₗ[R] P) (h : P →ₗ[R] M) : trace R P (g ∘ₗ f ∘ₗ h) = trace R N (f ∘ₗ h ∘ₗ g) := by rw [trace_comp_comm', comp_assoc] +variable [Module.Free R M] [Module.Finite R M] [Module.Free R P] [Module.Finite R P] in lemma trace_comp_cycle' (f : M →ₗ[R] N) (g : N →ₗ[R] P) (h : P →ₗ[R] M) : trace R P ((g ∘ₗ f) ∘ₗ h) = trace R M ((h ∘ₗ g) ∘ₗ f) := by rw [trace_comp_comm', ← comp_assoc] @@ -286,6 +292,7 @@ theorem IsProj.trace {p : Submodule R M} {f : M →ₗ[R] M} (h : IsProj p f) [M trace R M f = (finrank R p : R) := by rw [h.eq_conj_prodMap, trace_conj', trace_prodMap', trace_id, map_zero, add_zero] +variable [Module.Free R M] [Module.Finite R M] in lemma isNilpotent_trace_of_isNilpotent {f : M →ₗ[R] M} (hf : IsNilpotent f) : IsNilpotent (trace R M f) := by let b : Basis _ R M := Module.Free.chooseBasis R M @@ -293,6 +300,7 @@ lemma isNilpotent_trace_of_isNilpotent {f : M →ₗ[R] M} (hf : IsNilpotent f) apply Matrix.isNilpotent_trace_of_isNilpotent simpa +variable [Module.Free R M] [Module.Finite R M] in lemma trace_comp_eq_mul_of_commute_of_isNilpotent [IsReduced R] {f g : Module.End R M} (μ : R) (h_comm : Commute f g) (hg : IsNilpotent (g - algebraMap R _ μ)) : trace R M (f ∘ₗ g) = μ * trace R M f := by diff --git a/Mathlib/MeasureTheory/Constructions/Pi.lean b/Mathlib/MeasureTheory/Constructions/Pi.lean index 71b2a4b053c3d..3482a2535938d 100644 --- a/Mathlib/MeasureTheory/Constructions/Pi.lean +++ b/Mathlib/MeasureTheory/Constructions/Pi.lean @@ -867,7 +867,8 @@ theorem volume_preserving_pi_empty {ι : Type u} (α : ι → Type v) [Fintype MeasurePreserving (MeasurableEquiv.ofUniqueOfUnique (∀ i, α i) Unit) volume volume := measurePreserving_pi_empty fun _ => volume -theorem measurePreserving_piFinsetUnion [DecidableEq ι] {s t : Finset ι} (h : Disjoint s t) +theorem measurePreserving_piFinsetUnion {ι : Type*} {α : ι → Type*} + {_ : ∀ i, MeasurableSpace (α i)} [DecidableEq ι] {s t : Finset ι} (h : Disjoint s t) (μ : ∀ i, Measure (α i)) [∀ i, SigmaFinite (μ i)] : MeasurePreserving (MeasurableEquiv.piFinsetUnion α h) ((Measure.pi fun i : s ↦ μ i).prod (Measure.pi fun i : t ↦ μ i)) @@ -876,13 +877,15 @@ theorem measurePreserving_piFinsetUnion [DecidableEq ι] {s t : Finset ι} (h : measurePreserving_piCongrLeft (fun i : ↥(s ∪ t) ↦ μ i) e |>.comp <| measurePreserving_sumPiEquivProdPi_symm fun b ↦ μ (e b) -theorem volume_preserving_piFinsetUnion (α : ι → Type*) [DecidableEq ι] {s t : Finset ι} +theorem volume_preserving_piFinsetUnion {ι : Type*} [DecidableEq ι] (α : ι → Type*) {s t : Finset ι} (h : Disjoint s t) [∀ i, MeasureSpace (α i)] [∀ i, SigmaFinite (volume : Measure (α i))] : MeasurePreserving (MeasurableEquiv.piFinsetUnion α h) volume volume := measurePreserving_piFinsetUnion h (fun _ ↦ volume) -theorem measurePreserving_pi {β : ι → Type*} [∀ i, MeasurableSpace (β i)] - (ν : (i : ι) → Measure (β i)) {f : (i : ι) → (α i) → (β i)} [∀ i, SigmaFinite (ν i)] +theorem measurePreserving_pi {ι : Type*} [Fintype ι] {α : ι → Type v} {β : ι → Type*} + [∀ i, MeasureSpace (α i)] [∀ i, MeasurableSpace (β i)] + (μ : (i : ι) → Measure (α i)) (ν : (i : ι) → Measure (β i)) + {f : (i : ι) → (α i) → (β i)} [∀ i, SigmaFinite (ν i)] (hf : ∀ i, MeasurePreserving (f i) (μ i) (ν i)) : MeasurePreserving (fun a i ↦ f i (a i)) (Measure.pi μ) (Measure.pi ν) where measurable := diff --git a/Mathlib/MeasureTheory/Constructions/Prod/Basic.lean b/Mathlib/MeasureTheory/Constructions/Prod/Basic.lean index dd948e06b1dfd..ebf5efd059fd2 100644 --- a/Mathlib/MeasureTheory/Constructions/Prod/Basic.lean +++ b/Mathlib/MeasureTheory/Constructions/Prod/Basic.lean @@ -466,12 +466,12 @@ theorem ae_ae_of_ae_prod {p : α × β → Prop} (h : ∀ᵐ z ∂μ.prod ν, p ∀ᵐ x ∂μ, ∀ᵐ y ∂ν, p (x, y) := measure_ae_null_of_prod_null h -theorem ae_ae_eq_curry_of_prod {f g : α × β → γ} (h : f =ᵐ[μ.prod ν] g) : +theorem ae_ae_eq_curry_of_prod {γ : Type*} {f g : α × β → γ} (h : f =ᵐ[μ.prod ν] g) : ∀ᵐ x ∂μ, curry f x =ᵐ[ν] curry g x := ae_ae_of_ae_prod h -theorem ae_ae_eq_of_ae_eq_uncurry {f g : α → β → γ} (h : uncurry f =ᵐ[μ.prod ν] uncurry g) : - ∀ᵐ x ∂μ, f x =ᵐ[ν] g x := +theorem ae_ae_eq_of_ae_eq_uncurry {γ : Type*} {f g : α → β → γ} + (h : uncurry f =ᵐ[μ.prod ν] uncurry g) : ∀ᵐ x ∂μ, f x =ᵐ[ν] g x := ae_ae_eq_curry_of_prod h theorem ae_prod_mem_iff_ae_ae_mem {s : Set (α × β)} (hs : MeasurableSet s) : diff --git a/Mathlib/MeasureTheory/Group/Measure.lean b/Mathlib/MeasureTheory/Group/Measure.lean index c45cc18acbfdf..8172325ce37ac 100644 --- a/Mathlib/MeasureTheory/Group/Measure.lean +++ b/Mathlib/MeasureTheory/Group/Measure.lean @@ -523,6 +523,7 @@ lemma tendsto_measure_smul_diff_isCompact_isClosed [LocallyCompactSpace G] ENNReal.nhds_zero_basis.tendsto_right_iff.mpr <| fun _ h ↦ eventually_nhds_one_measure_smul_diff_lt hk h'k h.ne' +section IsMulLeftInvariant variable [IsMulLeftInvariant μ] /-- If a left-invariant measure gives positive mass to a compact set, then it gives positive mass to @@ -682,6 +683,8 @@ lemma _root_.IsCompact.measure_closure_eq_of_group {k : Set G} (hk : IsCompact k μ (closure k) = μ k := hk.measure_closure μ +end IsMulLeftInvariant + @[to_additive] lemma innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group [h : InnerRegularCompactLTTop μ] : InnerRegularWRT μ (fun s ↦ IsCompact s ∧ IsClosed s) (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞) := by diff --git a/Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean b/Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean index 38a0aab6c0316..b3d825fc3b697 100644 --- a/Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean +++ b/Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean @@ -72,7 +72,7 @@ This formulation assumes: * boundedness holds almost everywhere. -/ theorem measure_of_cont_bdd_of_tendsto_filter_indicator {ι : Type*} {L : Filter ι} - [L.IsCountablyGenerated] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (μ : Measure Ω) + [L.IsCountablyGenerated] (μ : Measure Ω) [IsFiniteMeasure μ] {c : ℝ≥0} {E : Set Ω} (E_mble : MeasurableSet E) (fs : ι → Ω →ᵇ ℝ≥0) (fs_bdd : ∀ᶠ i in L, ∀ᵐ ω : Ω ∂μ, fs i ω ≤ c) (fs_lim : ∀ᵐ ω ∂μ, Tendsto (fun i ↦ fs i ω) L (𝓝 (indicator E (fun _ ↦ (1 : ℝ≥0)) ω))) : @@ -90,7 +90,7 @@ measure of the set. A similar result with more general assumptions is `MeasureTheory.measure_of_cont_bdd_of_tendsto_filter_indicator`. -/ -theorem measure_of_cont_bdd_of_tendsto_indicator [OpensMeasurableSpace Ω] +theorem measure_of_cont_bdd_of_tendsto_indicator (μ : Measure Ω) [IsFiniteMeasure μ] {c : ℝ≥0} {E : Set Ω} (E_mble : MeasurableSet E) (fs : ℕ → Ω →ᵇ ℝ≥0) (fs_bdd : ∀ n ω, fs n ω ≤ c) (fs_lim : Tendsto (fun n ω ↦ fs n ω) atTop (𝓝 (indicator E fun _ ↦ (1 : ℝ≥0)))) : diff --git a/Mathlib/RingTheory/Kaehler/Basic.lean b/Mathlib/RingTheory/Kaehler/Basic.lean index f896a50f46ebc..d5a828b146a26 100644 --- a/Mathlib/RingTheory/Kaehler/Basic.lean +++ b/Mathlib/RingTheory/Kaehler/Basic.lean @@ -617,9 +617,8 @@ A --→ B R --→ S ``` -/ -variable (A B : Type*) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] -variable [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] -variable [SMulCommClass S A B] +variable (A B : Type*) [CommRing A] [CommRing B] [Algebra R A] +variable [Algebra A B] [Algebra S B] unsuppress_compilation in -- The map `(A →₀ A) →ₗ[A] (B →₀ B)` @@ -639,7 +638,8 @@ The kernel of the presentation `⊕ₓ B dx ↠ Ω_{B/S}` is spanned by the imag kernel of `⊕ₓ A dx ↠ Ω_{A/R}` and all `ds` with `s : S`. See `kerTotal_map'` for the special case where `R = S`. -/ -theorem KaehlerDifferential.kerTotal_map (h : Function.Surjective (algebraMap A B)) : +theorem KaehlerDifferential.kerTotal_map [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B] + (h : Function.Surjective (algebraMap A B)) : (KaehlerDifferential.kerTotal R A).map finsupp_map ⊔ Submodule.span A (Set.range fun x : S => .single (algebraMap S B x) (1 : B)) = (KaehlerDifferential.kerTotal S B).restrictScalars _ := by @@ -665,7 +665,8 @@ This is a special case of `kerTotal_map` where `R = S`. The kernel of the presentation `⊕ₓ B dx ↠ Ω_{B/R}` is spanned by the image of the kernel of `⊕ₓ A dx ↠ Ω_{A/R}` and all `da` with `a : A`. -/ -theorem KaehlerDifferential.kerTotal_map' (h : Function.Surjective (algebraMap A B)) : +theorem KaehlerDifferential.kerTotal_map' [Algebra R B] + [IsScalarTower R A B] (h : Function.Surjective (algebraMap A B)) : (KaehlerDifferential.kerTotal R A ⊔ Submodule.span A (Set.range fun x ↦ .single (algebraMap R A x) 1)).map finsupp_map = (KaehlerDifferential.kerTotal R B).restrictScalars _ := by @@ -674,6 +675,8 @@ theorem KaehlerDifferential.kerTotal_map' (h : Function.Surjective (algebraMap A refine congr_arg Set.range ?_ ext; simp [IsScalarTower.algebraMap_eq R A B] +variable [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B] [SMulCommClass S A B] + /-- The map `Ω[A⁄R] →ₗ[A] Ω[B⁄S]` given a square ``` A --→ B diff --git a/Mathlib/RingTheory/Unramified/Finite.lean b/Mathlib/RingTheory/Unramified/Finite.lean index b754c35bf4fee..0afad0fed8c13 100644 --- a/Mathlib/RingTheory/Unramified/Finite.lean +++ b/Mathlib/RingTheory/Unramified/Finite.lean @@ -80,32 +80,6 @@ theorem iff_exists_tensorProduct [EssFiniteType R S] : use 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1 linear_combination ht₁ s -variable [FormallyUnramified R S] [EssFiniteType R S] - -variable (R S) in -/-- -A finite-type `R`-algebra `S` is (formally) unramified iff there exists a `t : S ⊗[R] S` satisfying -1. `t` annihilates every `1 ⊗ s - s ⊗ 1`. -2. the image of `t` is `1` under the map `S ⊗[R] S → S`. -See `Algebra.FormallyUnramified.iff_exists_tensorProduct`. -This is the choice of such a `t`. --/ -noncomputable -def elem : S ⊗[R] S := - (iff_exists_tensorProduct.mp inferInstance).choose - -lemma one_tmul_sub_tmul_one_mul_elem - (s : S) : (1 ⊗ₜ s - s ⊗ₜ 1) * elem R S = 0 := - (iff_exists_tensorProduct.mp inferInstance).choose_spec.1 s - -lemma one_tmul_mul_elem - (s : S) : (1 ⊗ₜ s) * elem R S = (s ⊗ₜ 1) * elem R S := by - rw [← sub_eq_zero, ← sub_mul, one_tmul_sub_tmul_one_mul_elem] - -lemma lmul_elem [EssFiniteType R S] [FormallyUnramified R S] : - TensorProduct.lmul' R (elem R S) = 1 := - (iff_exists_tensorProduct.mp inferInstance).choose_spec.2 - lemma finite_of_free_aux (I) [DecidableEq I] (b : Basis I R S) (f : I →₀ S) (x : S) (a : I → I →₀ R) (ha : a = fun i ↦ b.repr (b i * x)) : (1 ⊗ₜ[R] x * Finsupp.sum f fun i y ↦ y ⊗ₜ[R] b i) = @@ -145,6 +119,33 @@ lemma finite_of_free_aux (I) [DecidableEq I] (b : Basis I R S) simp (config := {contextual := true}) · exact fun _ _ ↦ rfl +variable [FormallyUnramified R S] [EssFiniteType R S] + +variable (R S) in +/-- +A finite-type `R`-algebra `S` is (formally) unramified iff there exists a `t : S ⊗[R] S` satisfying +1. `t` annihilates every `1 ⊗ s - s ⊗ 1`. +2. the image of `t` is `1` under the map `S ⊗[R] S → S`. +See `Algebra.FormallyUnramified.iff_exists_tensorProduct`. +This is the choice of such a `t`. +-/ +noncomputable +def elem : S ⊗[R] S := + (iff_exists_tensorProduct.mp inferInstance).choose + +lemma one_tmul_sub_tmul_one_mul_elem + (s : S) : (1 ⊗ₜ s - s ⊗ₜ 1) * elem R S = 0 := + (iff_exists_tensorProduct.mp inferInstance).choose_spec.1 s + +lemma one_tmul_mul_elem + (s : S) : (1 ⊗ₜ s) * elem R S = (s ⊗ₜ 1) * elem R S := by + rw [← sub_eq_zero, ← sub_mul, one_tmul_sub_tmul_one_mul_elem] + +lemma lmul_elem : + TensorProduct.lmul' R (elem R S) = 1 := + (iff_exists_tensorProduct.mp inferInstance).choose_spec.2 + + variable (R S) /-- An unramified free algebra is finitely generated. Iversen I.2.8 -/ diff --git a/Mathlib/RingTheory/WittVector/Basic.lean b/Mathlib/RingTheory/WittVector/Basic.lean index 7d09dc5c960fb..5630d6a00254e 100644 --- a/Mathlib/RingTheory/WittVector/Basic.lean +++ b/Mathlib/RingTheory/WittVector/Basic.lean @@ -49,7 +49,7 @@ noncomputable section open MvPolynomial Function -variable {p : ℕ} {R S T : Type*} [hp : Fact p.Prime] [CommRing R] [CommRing S] [CommRing T] +variable {p : ℕ} {R S T : Type*} [CommRing R] [CommRing S] [CommRing T] variable {α : Type*} {β : Type*} local notation "𝕎" => WittVector p @@ -76,9 +76,6 @@ theorem surjective (f : α → β) (hf : Surjective f) : Surjective (mapFun f : ⟨mk _ fun n => Classical.choose <| hf <| x.coeff n, by ext n; simp only [mapFun, coeff_mk, comp_apply, Classical.choose_spec (hf (x.coeff n))]⟩ --- Porting note: using `(x y : 𝕎 R)` instead of `(x y : WittVector p R)` produced sorries. -variable (f : R →+* S) (x y : WittVector p R) - /-- Auxiliary tactic for showing that `mapFun` respects the ring operations. -/ -- porting note: a very crude port. macro "map_fun_tac" : tactic => `(tactic| ( @@ -92,6 +89,10 @@ macro "map_fun_tac" : tactic => `(tactic| ( ext ⟨i, k⟩ <;> fin_cases i <;> rfl)) +variable [Fact p.Prime] +-- Porting note: using `(x y : 𝕎 R)` instead of `(x y : WittVector p R)` produced sorries. +variable (f : R →+* S) (x y : WittVector p R) + -- and until `pow`. -- We do not tag these lemmas as `@[simp]` because they will be bundled in `map` later on. theorem zero : mapFun f (0 : 𝕎 R) = 0 := by map_fun_tac @@ -158,8 +159,6 @@ end Tactic section GhostFun -variable (x y : WittVector p R) - -- The following lemmas are not `@[simp]` because they will be bundled in `ghostMap` later on. @[local simp] @@ -167,6 +166,9 @@ theorem matrix_vecEmpty_coeff {R} (i j) : @coeff p R (Matrix.vecEmpty i) j = (Matrix.vecEmpty i : ℕ → R) j := by rcases i with ⟨_ | _ | _ | _ | i_val, ⟨⟩⟩ +variable [Fact p.Prime] +variable (x y : WittVector p R) + private theorem ghostFun_zero : ghostFun (0 : 𝕎 R) = 0 := by ghost_fun_tac 0, ![] @@ -232,6 +234,8 @@ private def ghostEquiv' [Invertible (p : R)] : 𝕎 R ≃ (ℕ → R) where apply_fun aeval x at this simpa only [aeval_bind₁, aeval_X, ghostFun, aeval_wittPolynomial] +variable [Fact p.Prime] + @[local instance] private def comm_ring_aux₁ : CommRing (𝕎 (MvPolynomial R ℚ)) := (ghostEquiv' p (MvPolynomial R ℚ)).injective.commRing ghostFun ghostFun_zero ghostFun_one diff --git a/Mathlib/RingTheory/WittVector/InitTail.lean b/Mathlib/RingTheory/WittVector/InitTail.lean index 63541a917319d..c2c6e3cc9a3a5 100644 --- a/Mathlib/RingTheory/WittVector/InitTail.lean +++ b/Mathlib/RingTheory/WittVector/InitTail.lean @@ -34,7 +34,7 @@ and shows how that polynomial interacts with `MvPolynomial.bind₁`. -/ -variable {p : ℕ} [hp : Fact p.Prime] (n : ℕ) {R : Type*} [CommRing R] +variable {p : ℕ} (n : ℕ) {R : Type*} [CommRing R] -- type as `\bbW` local notation "𝕎" => WittVector p @@ -79,6 +79,8 @@ instance select_isPoly {P : ℕ → Prop} : IsPoly p fun _ _ x => select P x := funext i apply coeff_select +variable [hp : Fact p.Prime] + theorem select_add_select_not : ∀ x : 𝕎 R, select P x + select (fun i => ¬P i) x = x := by -- Porting note: TC search was insufficient to find this instance, even though all required -- instances exist. See zulip: [https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/WittVector.20saga/near/370073526] @@ -127,6 +129,8 @@ theorem coeff_add_of_disjoint (x y : 𝕎 R) (h : ∀ n, x.coeff n = 0 ∨ y.coe end Select +variable [Fact p.Prime] + /-- `WittVector.init n x` is the Witt vector of which the first `n` coefficients are those from `x` and all other coefficients are `0`. See `WittVector.tail` for the complementary part. @@ -186,6 +190,9 @@ theorem init_init (x : 𝕎 R) (n : ℕ) : init n (init n x) = init n x := by simp only [WittVector.init, WittVector.select, WittVector.coeff_mk] by_cases hi : i < n <;> simp [hi] +section +variable [Fact p.Prime] + theorem init_add (x y : 𝕎 R) (n : ℕ) : init n (x + y) = init n (init n x + init n y) := by init_ring using wittAdd_vars @@ -207,6 +214,7 @@ theorem init_zsmul (m : ℤ) (x : 𝕎 R) (n : ℕ) : init n (m • x) = init n theorem init_pow (m : ℕ) (x : 𝕎 R) (n : ℕ) : init n (x ^ m) = init n (init n x ^ m) := by init_ring using fun p [Fact (Nat.Prime p)] n => wittPow_vars p m n +end section variable (p) diff --git a/Mathlib/RingTheory/WittVector/Teichmuller.lean b/Mathlib/RingTheory/WittVector/Teichmuller.lean index a68a5e0c2f286..d90c9006aefba 100644 --- a/Mathlib/RingTheory/WittVector/Teichmuller.lean +++ b/Mathlib/RingTheory/WittVector/Teichmuller.lean @@ -70,14 +70,14 @@ private theorem map_teichmullerFun (f : R →+* S) (r : R) : · rfl · exact f.map_zero -private theorem teichmuller_mul_aux₁ (x y : MvPolynomial R ℚ) : +private theorem teichmuller_mul_aux₁ {R : Type*} (x y : MvPolynomial R ℚ) : teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y := by apply (ghostMap.bijective_of_invertible p (MvPolynomial R ℚ)).1 rw [RingHom.map_mul] ext1 n simp only [Pi.mul_apply, ghostMap_apply, ghostComponent_teichmullerFun, mul_pow] -private theorem teichmuller_mul_aux₂ (x y : MvPolynomial R ℤ) : +private theorem teichmuller_mul_aux₂ {R : Type*} (x y : MvPolynomial R ℤ) : teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y := by refine map_injective (MvPolynomial.map (Int.castRingHom ℚ)) (MvPolynomial.map_injective _ Int.cast_injective) ?_ diff --git a/Mathlib/RingTheory/WittVector/Verschiebung.lean b/Mathlib/RingTheory/WittVector/Verschiebung.lean index def9919ecd7a2..17a60efd46d57 100644 --- a/Mathlib/RingTheory/WittVector/Verschiebung.lean +++ b/Mathlib/RingTheory/WittVector/Verschiebung.lean @@ -21,7 +21,7 @@ namespace WittVector open MvPolynomial -variable {p : ℕ} {R S : Type*} [hp : Fact p.Prime] [CommRing R] [CommRing S] +variable {p : ℕ} {R S : Type*} [CommRing R] [CommRing S] local notation "𝕎" => WittVector p -- type as `\bbW` @@ -49,13 +49,13 @@ theorem verschiebungFun_coeff_succ (x : 𝕎 R) (n : ℕ) : rfl @[ghost_simps] -theorem ghostComponent_zero_verschiebungFun (x : 𝕎 R) : +theorem ghostComponent_zero_verschiebungFun [hp : Fact p.Prime] (x : 𝕎 R) : ghostComponent 0 (verschiebungFun x) = 0 := by rw [ghostComponent_apply, aeval_wittPolynomial, Finset.range_one, Finset.sum_singleton, verschiebungFun_coeff_zero, pow_zero, pow_zero, pow_one, one_mul] @[ghost_simps] -theorem ghostComponent_verschiebungFun (x : 𝕎 R) (n : ℕ) : +theorem ghostComponent_verschiebungFun [hp : Fact p.Prime] (x : 𝕎 R) (n : ℕ) : ghostComponent (n + 1) (verschiebungFun x) = p * ghostComponent n x := by simp only [ghostComponent_apply, aeval_wittPolynomial] rw [Finset.sum_range_succ', verschiebungFun_coeff, if_pos rfl, @@ -96,6 +96,7 @@ example (p : ℕ) (f : ⦃R : Type _⦄ → [CommRing R] → WittVector p R → inferInstance variable {p} +variable [hp : Fact p.Prime] /-- `verschiebung x` shifts the coefficients of `x` up by one, by inserting 0 as the 0th coefficient. @@ -116,7 +117,7 @@ noncomputable def verschiebung : 𝕎 R →+ 𝕎 R where /-- `WittVector.verschiebung` is a polynomial function. -/ @[is_poly] -theorem verschiebung_isPoly : IsPoly p fun R _Rcr => @verschiebung p R hp _Rcr := +theorem verschiebung_isPoly : IsPoly p fun _ _ => verschiebung (p := p) := verschiebungFun_isPoly p /-- verschiebung is a natural transformation -/ diff --git a/Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean b/Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean index daa03f9b799fb..e4fb9f1ae0d5b 100644 --- a/Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean +++ b/Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean @@ -193,32 +193,6 @@ private theorem candidates_lipschitz (fA : f ∈ candidates X Y) : rw [dist_comm] exact candidates_lipschitz_aux fA -/-- candidates give rise to elements of `BoundedContinuousFunction`s -/ -def candidatesBOfCandidates (f : ProdSpaceFun X Y) (fA : f ∈ candidates X Y) : Cb X Y := - BoundedContinuousFunction.mkOfCompact ⟨f, (candidates_lipschitz fA).continuous⟩ - -theorem candidatesBOfCandidates_mem (f : ProdSpaceFun X Y) (fA : f ∈ candidates X Y) : - candidatesBOfCandidates f fA ∈ candidatesB X Y := - fA - -/-- The distance on `X ⊕ Y` is a candidate -/ -private theorem dist_mem_candidates : - (fun p : (X ⊕ Y) × (X ⊕ Y) => dist p.1 p.2) ∈ candidates X Y := by - simp_rw [candidates, Set.mem_setOf_eq, dist_comm, dist_triangle, dist_self, maxVar_bound, - forall_const, and_true] - exact ⟨fun x y => rfl, fun x y => rfl⟩ - -/-- The distance on `X ⊕ Y` as a candidate -/ -def candidatesBDist (X : Type u) (Y : Type v) [MetricSpace X] [CompactSpace X] [Nonempty X] - [MetricSpace Y] [CompactSpace Y] [Nonempty Y] : Cb X Y := - candidatesBOfCandidates _ dist_mem_candidates - -theorem candidatesBDist_mem_candidatesB : candidatesBDist X Y ∈ candidatesB X Y := - candidatesBOfCandidates_mem _ _ - -private theorem candidatesB_nonempty : (candidatesB X Y).Nonempty := - ⟨_, candidatesBDist_mem_candidatesB⟩ - /-- To apply Arzela-Ascoli, we need to check that the set of candidates is closed and equicontinuous. Equicontinuity follows from the Lipschitz control, we check closedness. -/ private theorem closed_candidatesB : IsClosed (candidatesB X Y) := by @@ -249,20 +223,6 @@ private theorem closed_candidatesB : IsClosed (candidatesB X Y) := by |apply isClosed_iInter _ |apply I1 _ _|apply I2 _ _|apply I3 _ _|apply I4 _ _ _|apply I5 _|apply I6 _ _|intro x -/-- Compactness of candidates (in `BoundedContinuousFunction`s) follows. -/ -private theorem isCompact_candidatesB : IsCompact (candidatesB X Y) := by - refine arzela_ascoli₂ - (Icc 0 (maxVar X Y) : Set ℝ) isCompact_Icc (candidatesB X Y) closed_candidatesB ?_ ?_ - · rintro f ⟨x1, x2⟩ hf - simp only [Set.mem_Icc] - exact ⟨candidates_nonneg hf, candidates_le_maxVar hf⟩ - · refine equicontinuous_of_continuity_modulus (fun t => 2 * maxVar X Y * t) ?_ _ ?_ - · have : Tendsto (fun t : ℝ => 2 * (maxVar X Y : ℝ) * t) (𝓝 0) (𝓝 (2 * maxVar X Y * 0)) := - tendsto_const_nhds.mul tendsto_id - simpa using this - · rintro x y ⟨f, hf⟩ - exact (candidates_lipschitz hf).dist_le_mul _ _ - /-- We will then choose the candidate minimizing the Hausdorff distance. Except that we are not in a metric space setting, so we need to define our custom version of Hausdorff distance, called `HD`, and prove its basic properties. -/ @@ -279,7 +239,7 @@ theorem HD_below_aux1 {f : Cb X Y} (C : ℝ) {x : X} : let ⟨cf, hcf⟩ := f.isBounded_range.bddBelow ⟨cf + C, forall_mem_range.2 fun _ => add_le_add_right ((fun x => hcf (mem_range_self x)) _) _⟩ -private theorem HD_bound_aux1 (f : Cb X Y) (C : ℝ) : +private theorem HD_bound_aux1 [Nonempty Y] (f : Cb X Y) (C : ℝ) : BddAbove (range fun x : X => ⨅ y, f (inl x, inr y) + C) := by obtain ⟨Cf, hCf⟩ := f.isBounded_range.bddAbove refine ⟨Cf + C, forall_mem_range.2 fun x => ?_⟩ @@ -292,7 +252,7 @@ theorem HD_below_aux2 {f : Cb X Y} (C : ℝ) {y : Y} : let ⟨cf, hcf⟩ := f.isBounded_range.bddBelow ⟨cf + C, forall_mem_range.2 fun _ => add_le_add_right ((fun x => hcf (mem_range_self x)) _) _⟩ -private theorem HD_bound_aux2 (f : Cb X Y) (C : ℝ) : +private theorem HD_bound_aux2 [Nonempty X] (f : Cb X Y) (C : ℝ) : BddAbove (range fun y : Y => ⨅ x, f (inl x, inr y) + C) := by obtain ⟨Cf, hCf⟩ := f.isBounded_range.bddAbove refine ⟨Cf + C, forall_mem_range.2 fun y => ?_⟩ @@ -300,29 +260,8 @@ private theorem HD_bound_aux2 (f : Cb X Y) (C : ℝ) : ⨅ x, f (inl x, inr y) + C ≤ f (inl default, inr y) + C := ciInf_le (HD_below_aux2 C) default _ ≤ Cf + C := add_le_add ((fun x => hCf (mem_range_self x)) _) le_rfl -/-- Explicit bound on `HD (dist)`. This means that when looking for minimizers it will -be sufficient to look for functions with `HD(f)` bounded by this bound. -/ -theorem HD_candidatesBDist_le : - HD (candidatesBDist X Y) ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := by - refine max_le (ciSup_le fun x => ?_) (ciSup_le fun y => ?_) - · have A : ⨅ y, candidatesBDist X Y (inl x, inr y) ≤ candidatesBDist X Y (inl x, inr default) := - ciInf_le (by simpa using HD_below_aux1 0) default - have B : dist (inl x) (inr default) ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := - calc - dist (inl x) (inr (default : Y)) = dist x (default : X) + 1 + dist default default := rfl - _ ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := by - gcongr <;> - exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _) - exact le_trans A B - · have A : ⨅ x, candidatesBDist X Y (inl x, inr y) ≤ candidatesBDist X Y (inl default, inr y) := - ciInf_le (by simpa using HD_below_aux2 0) default - have B : dist (inl default) (inr y) ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := - calc - dist (inl (default : X)) (inr y) = dist default default + 1 + dist default y := rfl - _ ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := by - gcongr <;> - exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _) - exact le_trans A B +section Nonempty +variable [Nonempty X] [Nonempty Y] /- To check that `HD` is continuous, we check that it is Lipschitz. As `HD` is a max, we prove separately inequalities controlling the two terms (relying too heavily on copy-paste...) -/ @@ -382,7 +321,8 @@ private theorem HD_lipschitz_aux2 (f g : Cb X Y) : -- deduce the result from the above two steps simpa [E2, E1] -private theorem HD_lipschitz_aux3 (f g : Cb X Y) : HD f ≤ HD g + dist f g := +private theorem HD_lipschitz_aux3 (f g : Cb X Y) : + HD f ≤ HD g + dist f g := max_le (le_trans (HD_lipschitz_aux1 f g) (add_le_add_right (le_max_left _ _) _)) (le_trans (HD_lipschitz_aux2 f g) (add_le_add_right (le_max_right _ _) _)) @@ -390,6 +330,77 @@ private theorem HD_lipschitz_aux3 (f g : Cb X Y) : HD f ≤ HD g + dist f g := private theorem HD_continuous : Continuous (HD : Cb X Y → ℝ) := LipschitzWith.continuous (LipschitzWith.of_le_add HD_lipschitz_aux3) +end Nonempty + +variable [CompactSpace X] [CompactSpace Y] + +/-- Compactness of candidates (in `BoundedContinuousFunction`s) follows. -/ +private theorem isCompact_candidatesB : IsCompact (candidatesB X Y) := by + refine arzela_ascoli₂ + (Icc 0 (maxVar X Y) : Set ℝ) isCompact_Icc (candidatesB X Y) closed_candidatesB ?_ ?_ + · rintro f ⟨x1, x2⟩ hf + simp only [Set.mem_Icc] + exact ⟨candidates_nonneg hf, candidates_le_maxVar hf⟩ + · refine equicontinuous_of_continuity_modulus (fun t => 2 * maxVar X Y * t) ?_ _ ?_ + · have : Tendsto (fun t : ℝ => 2 * (maxVar X Y : ℝ) * t) (𝓝 0) (𝓝 (2 * maxVar X Y * 0)) := + tendsto_const_nhds.mul tendsto_id + simpa using this + · rintro x y ⟨f, hf⟩ + exact (candidates_lipschitz hf).dist_le_mul _ _ + +/-- candidates give rise to elements of `BoundedContinuousFunction`s -/ +def candidatesBOfCandidates (f : ProdSpaceFun X Y) (fA : f ∈ candidates X Y) : Cb X Y := + BoundedContinuousFunction.mkOfCompact ⟨f, (candidates_lipschitz fA).continuous⟩ + +theorem candidatesBOfCandidates_mem (f : ProdSpaceFun X Y) (fA : f ∈ candidates X Y) : + candidatesBOfCandidates f fA ∈ candidatesB X Y := + fA + +variable [Nonempty X] [Nonempty Y] + +/-- The distance on `X ⊕ Y` is a candidate -/ +private theorem dist_mem_candidates : + (fun p : (X ⊕ Y) × (X ⊕ Y) => dist p.1 p.2) ∈ candidates X Y := by + simp_rw [candidates, Set.mem_setOf_eq, dist_comm, dist_triangle, dist_self, maxVar_bound, + forall_const, and_true] + exact ⟨fun x y => rfl, fun x y => rfl⟩ + +/-- The distance on `X ⊕ Y` as a candidate -/ +def candidatesBDist (X : Type u) (Y : Type v) [MetricSpace X] [CompactSpace X] [Nonempty X] + [MetricSpace Y] [CompactSpace Y] [Nonempty Y] : Cb X Y := + candidatesBOfCandidates _ dist_mem_candidates + +theorem candidatesBDist_mem_candidatesB : + candidatesBDist X Y ∈ candidatesB X Y := + candidatesBOfCandidates_mem _ _ + +private theorem candidatesB_nonempty : (candidatesB X Y).Nonempty := + ⟨_, candidatesBDist_mem_candidatesB⟩ + +/-- Explicit bound on `HD (dist)`. This means that when looking for minimizers it will +be sufficient to look for functions with `HD(f)` bounded by this bound. -/ +theorem HD_candidatesBDist_le : + HD (candidatesBDist X Y) ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := by + refine max_le (ciSup_le fun x => ?_) (ciSup_le fun y => ?_) + · have A : ⨅ y, candidatesBDist X Y (inl x, inr y) ≤ candidatesBDist X Y (inl x, inr default) := + ciInf_le (by simpa using HD_below_aux1 0) default + have B : dist (inl x) (inr default) ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := + calc + dist (inl x) (inr (default : Y)) = dist x (default : X) + 1 + dist default default := rfl + _ ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := by + gcongr <;> + exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _) + exact le_trans A B + · have A : ⨅ x, candidatesBDist X Y (inl x, inr y) ≤ candidatesBDist X Y (inl default, inr y) := + ciInf_le (by simpa using HD_below_aux2 0) default + have B : dist (inl default) (inr y) ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := + calc + dist (inl (default : X)) (inr y) = dist default default + 1 + dist default y := rfl + _ ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := by + gcongr <;> + exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _) + exact le_trans A B + end Constructions section Consequences