Merge remote-tracking branch 'upstream/master' into bump/v4.31.0

Author: mathlib4-bot

Mathlib.lean

@@ -4338,6 +4338,7 @@ public import Mathlib.Dynamics.Ergodic.Function
 public import Mathlib.Dynamics.Ergodic.MeasurePreserving
 public import Mathlib.Dynamics.Ergodic.RadonNikodym
 public import Mathlib.Dynamics.FixedPoints.Basic
+public import Mathlib.Dynamics.FixedPoints.Defs
 public import Mathlib.Dynamics.FixedPoints.Prufer
 public import Mathlib.Dynamics.FixedPoints.Topology
 public import Mathlib.Dynamics.Flow

Mathlib/Algebra/Lie/Graded.lean

@@ -12,9 +12,7 @@ public import Mathlib.Algebra.Lie.Derivation.Basic
 # Graded Lie algebras
 
 This file defines typeclasses `SetLike.GradedBracket` and `GradedLieAlgebra`, for working with Lie
-algebras that are graded by a collection `ℒ` of submodules. The additivity of degree with respect to
-the bracket product is encoded by an addition condition so we can avoid the usual difficulties of
-adding elements of `A (i + j)` to elements of `A (j + i)`.
+algebras that are graded by a collection `ℒ` of submodules.
 
 ## Main definitions
 
@@ -25,6 +23,12 @@ adding elements of `A (i + j)` to elements of `A (j + i)`.
 * `LieDerivation.ofGrading`: A Lie derivation on a graded Lie algebra, that scalar-multiplies graded
   pieces by an additive map applied to degree.
 
+## Implementation notes
+
+For now we only implement internally-graded Lie algebras; supporting the externally-graded case
+would be achieved by generalizing the `LieRing (⨁ i, ℒ i)` instance to take a family of types,
+and defining a new `GradedMonoid.GBracket` class to provide the data piecewise.
+
 -/
 
 @[expose] public section
@@ -38,7 +42,7 @@ section SetLike
 /-- A class that ensures a bracket product preserves an additive grading. -/
 class SetLike.GradedBracket [SetLike σ L] [Bracket L L] [Add ι] (ℒ : ι → σ) : Prop where
   /-- Bracket is homogeneous -/
-  bracket_mem : ∀ ⦃i j k⦄ {gi gj}, i + j = k → gi ∈ ℒ i → gj ∈ ℒ j → ⁅gi, gj⁆ ∈ ℒ k
+  bracket_mem : ∀ ⦃i j⦄ {gi gj}, gi ∈ ℒ i → gj ∈ ℒ j → ⁅gi, gj⁆ ∈ ℒ (i + j)
 
 variable [DecidableEq ι] [AddCommMonoid ι] [CommRing R] [LieRing L] [LieAlgebra R L]
   (ℒ : ι → Submodule R L)
@@ -125,7 +129,7 @@ def ofGradingSum (φ : ι →+ R) : LieDerivation R (⨁ i, ℒ i) (⨁ i, ℒ i
             add_lie, smul_add, add_sub, ← sub_sub]
           congr 1
           have : (decompose ℒ).symm ⁅of (fun i ↦ ℒ i) i a, of (fun i ↦ ℒ i) k b⁆ ∈ ℒ (i + k) := by
-            simp [SetLike.GradedBracket.bracket_mem rfl (Submodule.coe_mem a) (Submodule.coe_mem b)]
+            simp [SetLike.GradedBracket.bracket_mem (Submodule.coe_mem a) (Submodule.coe_mem b)]
           rw [hM _ _ this, hM k (of (ℒ ·) k b) (by simp), ← lie_skew (of (ℒ ·) k b),
             add_sub_right_comm, add_right_cancel_iff, add_comm i k, map_add, add_smul,
             DirectSum.add_apply, Submodule.coe_add, sub_eq_add_neg, lie_smul, add_left_cancel_iff,

Mathlib/Algebra/Module/Torsion/PrimaryComponent.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Module.Torsion.Basic
 public import Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
+public import Mathlib.RingTheory.DedekindDomain.Factorization
 
 /-!
 # I-Primary Components of modules
@@ -15,7 +16,7 @@ Let `A` be a commutative ring and `I`, an ideal of `A`.
 Given an `A`-Module `M` it's `I`-primary component is defined as
   $$M(I) := \bigcup_{i : \mathbb{N}} \text{torsionBySet A  M }  I ^ i.$$
 
-For `P : HeightOneSpectrum A`, the main result of this file (TODO) is that
+For `P : HeightOneSpectrum A`, the main result of this file is that
   $$M \cong \bigoplus_{P} M(P).$$
 
 ## Main definitions
@@ -28,6 +29,8 @@ For `P : HeightOneSpectrum A`, the main result of this file (TODO) is that
 
 variable {A M M₁ M₂ : Type*} [CommRing A]
 
+open IsDedekindDomain Submodule Module HeightOneSpectrum Set Function
+
 namespace Ideal
 
 variable (I : Ideal A)
@@ -127,6 +130,64 @@ theorem primaryComponent_sup (N₁ N₂ : Submodule A M) (hD : Disjoint N₁ N
       aesop
     · use y, hymem, z, hzmem
 
+section IsDedekindDomain
+
+variable [IsDedekindDomain A]
+
+open scoped nonZeroDivisors
+
+theorem iSup_primaryComponent_eq_top (h : IsTorsion A M) :
+    ⨆ P : HeightOneSpectrum A, primaryComponent M (P : Ideal A) = ⊤ := by
+  rw [eq_top_iff']
+  intro x
+  obtain ⟨⟨a : A, ha : a ∈ A⁰⟩, hmem : a • x = 0⟩ := h (x := x)
+  replace hmem : x ∈ torsionBySet A M (span {a}) := by
+    simp_all [← torsionBySet_eq_torsionBySet_span {a}]
+  have ha0 : span {a} ≠ ⊥ := by simpa using nonZeroDivisors.ne_zero ha
+  rw [← iInf_maxPowDividing_eq ha0] at hmem
+  let : Fintype (mulSupport fun v : HeightOneSpectrum A => v.maxPowDividing (span {a})) :=
+    Finite.fintype (hasFiniteMulSupport ha0)
+  let S := (mulSupport fun v : HeightOneSpectrum A => v.maxPowDividing (span {a})).toFinset
+  have : (⨅ i : HeightOneSpectrum A, i.maxPowDividing (span {a})) =
+      (⨅ i ∈ S, i.maxPowDividing (span {a})) := by
+    ext x
+    constructor
+    · aesop
+    · simp only [mem_iInf]
+      intro h i
+      by_cases htop : i.maxPowDividing (span {a}) = ⊤ <;> simp_all [S]
+  have hPairwise : (S : Set (HeightOneSpectrum _)).Pairwise
+      fun i j ↦ i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤ :=
+    fun r hr s hs hrs ↦ (isCoprime_pow_of_ne _ _ hrs _ _).sup_eq
+  rw [this, ← iSup_torsionBySet_ideal_eq_torsionBySet_iInf hPairwise] at hmem
+  revert x
+  rw [← SetLike.le_def]
+  refine iSup_mono (fun P x hxmem ↦ ?_)
+  by_cases hPS : P ∈ S
+  · simp_all only [mem_nonZeroDivisors_iff_ne_zero, ne_eq, mem_toFinset, mem_mulSupport,
+      one_eq_top, primaryComponent_mem, mem_torsionBySet_iff, SetLike.coe_sort_coe,
+      Subtype.forall, iSup_pos, S]
+    exact ⟨(Associates.mk P.asIdeal).count (Associates.mk (span {a})).factors, fun _ b ↦ hxmem _ b⟩
+  · simp_all
+
+variable (A M) in
+theorem iSupIndep_primaryComponent :
+    iSupIndep fun P : HeightOneSpectrum A => primaryComponent M (P : Ideal A) := by
+  rw [iSupIndep_iff_finset_sum_eq_zero_imp_eq_zero]
+  intro s p hmem hsum
+  simp only [primaryComponent_mem] at hmem
+  choose! f hmem using hmem
+  let m := s.sup f
+  have hSupIndep : iSupIndep fun i : HeightOneSpectrum A ↦ torsionBySet A M ↑(i.asIdeal ^ m) := by
+    rw [iSupIndep_iff_supIndep]
+    exact fun _ ↦ supIndep_torsionBySet_ideal
+      fun _ _ _ _ hPQ ↦ (isCoprime_pow_of_ne _ _ hPQ _ _).sup_eq
+  rw [iSupIndep_iff_finset_sum_eq_zero_imp_eq_zero] at hSupIndep
+  apply hSupIndep _ _ ?_ hsum
+  exact fun P hP ↦ torsionBySet_le_torsionBySet_pow _ _ (Finset.le_sup hP) _ (hmem P hP)
+
+end IsDedekindDomain
+
 end AddCommGroup
 
 end CommRing

Mathlib/Dynamics/FixedPoints/Basic.lean

@@ -7,16 +7,12 @@ module
 
 public import Mathlib.Algebra.Group.End
 public import Mathlib.Data.Set.Function
+public import Mathlib.Dynamics.FixedPoints.Defs
 
 /-!
 # Fixed points of a self-map
 
-In this file we define
-
-* the predicate `IsFixedPt f x := f x = x`;
-* the set `fixedPoints f` of fixed points of a self-map `f`.
-
-We also prove some simple lemmas about `IsFixedPt` and `∘`, `iterate`, and `Semiconj`.
+We prove some simple lemmas about `IsFixedPt` and `∘`, `iterate`, and `Semiconj`.
 
 ## Tags
 
@@ -25,34 +21,18 @@ fixed point
 
 @[expose] public section
 
-
 open Equiv
 
 universe u v
 
-variable {α : Type u} {β : Type v} {f fa g : α → α} {x : α} {fb : β → β} {e : Perm α}
+variable {α β : Type*} {f fa g : α → α} {x : α} {fb : β → β} {e : Perm α}
 
 namespace Function
 
 open Function (Commute)
 
-/-- Every point is a fixed point of `id`. -/
-theorem isFixedPt_id (x : α) : IsFixedPt id x :=
-  (rfl :)
-
-/-- A function fixes every point iff it is the identity. -/
-@[simp] theorem forall_isFixedPt_iff : (∀ x, IsFixedPt f x) ↔ f = id :=
-  ⟨funext, fun h ↦ h ▸ isFixedPt_id⟩
-
 namespace IsFixedPt
 
-instance decidable [h : DecidableEq α] {f : α → α} {x : α} : Decidable (IsFixedPt f x) :=
-  h (f x) x
-
-/-- If `x` is a fixed point of `f`, then `f x = x`. This is useful, e.g., for `rw` or `simp`. -/
-protected theorem eq (hf : IsFixedPt f x) : f x = x :=
-  hf
-
 /-- If `x` is a fixed point of `f` and `g`, then it is a fixed point of `f ∘ g`. -/
 protected theorem comp (hf : IsFixedPt f x) (hg : IsFixedPt g x) : IsFixedPt (f ∘ g) x :=
   calc
@@ -114,27 +94,6 @@ theorem Injective.isFixedPt_apply_iff (hf : Injective f) {x : α} :
     IsFixedPt f (f x) ↔ IsFixedPt f x :=
   ⟨fun h => hf h.eq, IsFixedPt.apply⟩
 
-/-- The set of fixed points of a map `f : α → α`. -/
-def fixedPoints (f : α → α) : Set α :=
-  { x : α | IsFixedPt f x }
-
-instance fixedPoints.decidable [DecidableEq α] (f : α → α) (x : α) :
-    Decidable (x ∈ fixedPoints f) :=
-  IsFixedPt.decidable
-
-@[simp]
-theorem mem_fixedPoints : x ∈ fixedPoints f ↔ IsFixedPt f x :=
-  Iff.rfl
-
-theorem mem_fixedPoints_iff {α : Type*} {f : α → α} {x : α} : x ∈ fixedPoints f ↔ f x = x := by
-  rfl
-
-@[simp]
-theorem fixedPoints_id : fixedPoints (@id α) = Set.univ :=
-  Set.ext fun _ => by simpa using isFixedPt_id _
-
-theorem fixedPoints_subset_range : fixedPoints f ⊆ Set.range f := fun x hx => ⟨x, hx⟩
-
 /-- If `g` semiconjugates `fa` to `fb`, then it sends fixed points of `fa` to fixed points
 of `fb`. -/
 theorem Semiconj.mapsTo_fixedPoints {g : α → β} (h : Semiconj g fa fb) :

Mathlib/Dynamics/FixedPoints/Defs.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2020 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+module
+
+public import Mathlib.Data.Set.Operations
+
+/-!
+# Fixed points of a self-map
+
+In this file we define the set `Function.fixedPoints` of fixed points of a function `f : α → α`.
+The related predicate `IsFixedPt` is defined in `Mathlib.Logic.Function.Defs`.
+
+## Tags
+
+fixed point
+-/
+
+@[expose] public section
+
+namespace Function
+
+variable {α : Type*} {x : α} {f : α → α}
+
+/-- The set of fixed points of a map `f : α → α`. -/
+def fixedPoints (f : α → α) : Set α :=
+  { x : α | IsFixedPt f x }
+
+instance fixedPoints.decidable [DecidableEq α] (f : α → α) (x : α) :
+    Decidable (x ∈ fixedPoints f) :=
+  IsFixedPt.decidable
+
+@[simp]
+theorem mem_fixedPoints : x ∈ fixedPoints f ↔ IsFixedPt f x :=
+  .rfl
+
+theorem mem_fixedPoints_iff {α : Type*} {f : α → α} {x : α} : x ∈ fixedPoints f ↔ f x = x :=
+  .rfl
+
+@[simp]
+theorem fixedPoints_id : fixedPoints (@id α) = Set.univ :=
+  Set.ext fun _ => by simpa using isFixedPt_id _
+
+theorem fixedPoints_subset_range : fixedPoints f ⊆ Set.range f := fun x hx => ⟨x, hx⟩
+
+end Function

Mathlib/LinearAlgebra/TensorProduct/Pi.lean

@@ -43,16 +43,14 @@ section
 
 variable {ι} (M : ι → Type*) [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
 
-set_option backward.privateInPublic true in
-private def piRightHomBil : N →ₗ[S] (∀ i, M i) →ₗ[R] ∀ i, N ⊗[R] M i where
+/-- (Implementation): Bilinear map for defining `TensorProduct.piRightHom`. -/
+def piRightHomBil : N →ₗ[S] (∀ i, M i) →ₗ[R] ∀ i, N ⊗[R] M i where
   toFun n := LinearMap.pi (fun i ↦ mk R N (M i) n ∘ₗ LinearMap.proj i)
   map_add' _ _ := by
     ext
     simp
   map_smul' _ _ := rfl
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- For any `R`-module `N`, index type `ι` and family of `R`-modules `Mᵢ`, there is a natural
 linear map `N ⊗[R] (∀ i, M i) →ₗ ∀ i, N ⊗[R] M i`. This map is an isomorphism if `ι` is finite. -/
 def piRightHom : N ⊗[R] (∀ i, M i) →ₗ[S] ∀ i, N ⊗[R] M i :=
@@ -65,8 +63,7 @@ lemma piRightHom_tmul (x : N) (f : ∀ i, M i) :
 
 variable [Fintype ι] [DecidableEq ι]
 
-set_option backward.privateInPublic true in
-private
+/-- (Implementation): Inverse for `TensorProduct.piRight`. -/
 def piRightInv : (∀ i, N ⊗[R] M i) →ₗ[S] N ⊗[R] ∀ i, M i :=
   LinearMap.lsum S (fun i ↦ N ⊗[R] M i) S <| fun i ↦
     AlgebraTensorModule.map LinearMap.id (single R M i)
@@ -90,8 +87,6 @@ private lemma piRightInv_single (x : N) (i : ι) (m : M i) :
   rw [this]
   simp
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- Tensor product commutes with finite products on the right. -/
 def piRight : N ⊗[R] (∀ i, M i) ≃ₗ[S] ∀ i, N ⊗[R] M i :=
   LinearEquiv.ofLinear
@@ -122,8 +117,8 @@ TODO: generalize to `S`-linear. -/
 
 end
 
-set_option backward.privateInPublic true in
-private def piScalarRightHomBil : N →ₗ[S] (ι → R) →ₗ[R] (ι → N) where
+/-- (Implementation): Bilinear map for defining `TensorProduct.piScalarRightHom`. -/
+def piScalarRightHomBil : N →ₗ[S] (ι → R) →ₗ[R] (ι → N) where
   toFun n := LinearMap.compLeft (toSpanSingleton R N n) ι
   map_add' x y := by
     ext i j
@@ -135,8 +130,6 @@ private def piScalarRightHomBil : N →ₗ[S] (ι → R) →ₗ[R] (ι → N) wh
     rw [← IsScalarTower.smul_assoc, _root_.Algebra.smul_def, mul_comm, mul_smul]
     simp
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- For any `R`-module `N` and index type `ι`, there is a natural
 linear map `N ⊗[R] (ι → R) →ₗ (ι → N)`. This map is an isomorphism if `ι` is finite. -/
 def piScalarRightHom : N ⊗[R] (ι → R) →ₗ[S] (ι → N) :=
@@ -150,8 +143,7 @@ lemma piScalarRightHom_tmul (x : N) (f : ι → R) :
 
 variable [Fintype ι] [DecidableEq ι]
 
-set_option backward.privateInPublic true in
-private
+/-- (Implementation): Inverse for `TensorProduct.piScalarRight`. -/
 def piScalarRightInv : (ι → N) →ₗ[S] N ⊗[R] (ι → R) :=
   LinearMap.lsum S (fun _ ↦ N) S <| fun i ↦ {
     toFun := fun n ↦ n ⊗ₜ Pi.single i 1
@@ -164,8 +156,6 @@ private lemma piScalarRightInv_single (x : N) (i : ι) :
     piScalarRightInv R S N ι (Pi.single i x) = x ⊗ₜ Pi.single i 1 := by
   simp [piScalarRightInv, Pi.single_apply, TensorProduct.ite_tmul]
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- For any `R`-module `N` and finite index type `ι`, `N ⊗[R] (ι → R)` is canonically
 isomorphic to `ι → N`. -/
 def piScalarRight : N ⊗[R] (ι → R) ≃ₗ[S] (ι → N) :=

Mathlib/Logic/Equiv/Defs.lean

@@ -818,6 +818,8 @@ noncomputable def ofBijective (f : α → β) (hf : Bijective f) : α ≃ β whe
   left_inv := leftInverse_surjInv hf
   right_inv := rightInverse_surjInv _
 
+@[simp] lemma coe_ofBijective (f : α → β) (hf : Bijective f) : ⇑(ofBijective f hf) = f := rfl
+
 lemma ofBijective_apply_symm_apply (f : α → β) (hf : Bijective f) (x : β) :
     f ((ofBijective f hf).symm x) = x :=
   (ofBijective f hf).apply_symm_apply x

Mathlib/Logic/Function/Defs.lean

@@ -75,10 +75,25 @@ variable {α : Type u₁} {β : Type u₂}
 /-- A point `x` is a fixed point of `f : α → α` if `f x = x`. -/
 def IsFixedPt (f : α → α) (x : α) := f x = x
 
+/-- If `x` is a fixed point of `f`, then `f x = x`. This is useful, e.g., for `rw` or `simp`. -/
+protected theorem IsFixedPt.eq {f : α → α} {x : α} (hf : IsFixedPt f x) : f x = x :=
+  hf
+
+instance IsFixedPt.decidable [h : DecidableEq α] {f : α → α} {x : α} : Decidable (IsFixedPt f x) :=
+  h (f x) x
+
 @[nontriviality]
 theorem IsFixedPt.of_subsingleton [Subsingleton α] (f : α → α) (x : α) : IsFixedPt f x :=
   Subsingleton.elim _ _
 
+/-- Every point is a fixed point of `id`. -/
+theorem isFixedPt_id (x : α) : IsFixedPt id x :=
+  rfl
+
+/-- A function fixes every point iff it is the identity. -/
+@[simp] theorem forall_isFixedPt_iff {f : α → α} : (∀ x, IsFixedPt f x) ↔ f = id :=
+  ⟨funext, fun h ↦ h ▸ isFixedPt_id⟩
+
 end Function
 
 namespace Pi