Merge master into nightly-testing

Author: mathlib-nightly-testing[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/AlgebraicGeometry/Gluing.lean

@@ -77,6 +77,7 @@ namespace Scheme
   limits library easier.)
 4. An open immersion `f i j : V i j ⟶ U i` for each `i j : ι`.
 5. A transition map `t i j : V i j ⟶ V j i` for each `i j : ι`.
+
 such that
 6. `f i i` is an isomorphism.
 7. `t i i` is the identity.
@@ -500,6 +501,7 @@ For such a diagram, we can glue them directly since the gluing conditions are al
 The intended usage is to provide the following instances:
 - `∀ {i j} (f : i ⟶ j), IsOpenImmersion (F.map f)`
 - `(F ⋙ forget).IsLocallyDirected`
+
 and to directly use the `colimit` API.
 Also see `AlgebraicGeometry.Scheme.IsLocallyDirected.openCover` for the open cover of the `colimit`.
 

Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

@@ -473,6 +473,7 @@ schemes, it is equivalent to `Q : AffineTargetMorphismProperty`.
 To make the proofs easier, we state it instead as
 1. `Q` is local at the target
 2. `P f` if and only if `∀ U, Q (f ∣_ U)` ranging over all affine opens of the target of `f`.
+
 See `HasAffineProperty.iff`.
 -/
 class HasAffineProperty (P : MorphismProperty Scheme)

Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

@@ -250,7 +250,7 @@ and for `f : Spec B ⟶ Spec A`, it is equivalent to the ring hom property `Q`.
 To make the proofs easier, we state it instead as
 1. `Q` is local (See `RingHom.PropertyIsLocal`)
 2. `P f` if and only if `Q` holds for every `Γ(Y, U) ⟶ Γ(X, V)` for all affine `U`, `V`.
-See `HasRingHomProperty.iff_appLE`.
+  See `HasRingHomProperty.iff_appLE`.
 -/
 class HasRingHomProperty (P : MorphismProperty Scheme.{u})
     (Q : outParam (∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop)) : Prop where

Mathlib/Analysis/InnerProductSpace/Orthonormal.lean

@@ -95,6 +95,11 @@ theorem orthonormal_iff_ite [DecidableEq ι] {v : ι → E} :
     · intro i j hij
       simpa [hij] using h i j
 
+@[simp]
+theorem orthonormal_subsingleton_iff [Subsingleton ι] {v : ι → E} :
+    Orthonormal 𝕜 v ↔ ∀ i, ‖v i‖ = 1 := by
+  simp [orthonormal_iff_ite, ← map_pow, pow_eq_one_iff_of_nonneg]
+
 /-- `if ... then ... else` characterization of a set of vectors being orthonormal.  (Inner product
 equals Kronecker delta.) -/
 theorem orthonormal_subtype_iff_ite [DecidableEq E] {s : Set E} :

Mathlib/Analysis/InnerProductSpace/PiL2.lean

@@ -51,6 +51,9 @@ the last section, various properties of matrices are explored.
 - `stdOrthonormalBasis`: provides an arbitrarily-chosen `OrthonormalBasis` of a given
   finite-dimensional inner product space
 
+- `orthonormalBasisSingleton`: an orthonormal basis formed by a single unit vector in a
+  one-dimensional inner product space.
+
 For consequences in infinite dimension (Hilbert bases, etc.), see the file
 `Analysis.InnerProductSpace.L2Space`.
 
@@ -636,7 +639,7 @@ variable (ι 𝕜) in
 /-- `OrthonormalBasis.singleton ι 𝕜` is the orthonormal basis sending the unique element of `ι` to
 `1 : 𝕜`. -/
 protected noncomputable def singleton : OrthonormalBasis ι 𝕜 𝕜 :=
-  (Basis.singleton ι 𝕜).toOrthonormalBasis (by simp [orthonormal_iff_ite, Unique.eq_default])
+  (Basis.singleton ι 𝕜).toOrthonormalBasis (by simp)
 
 @[simp]
 theorem singleton_apply (i) : OrthonormalBasis.singleton ι 𝕜 i = 1 := Basis.singleton_apply _ _ _
@@ -1312,3 +1315,34 @@ theorem InnerProductSpace.symm_toEuclideanLin_rankOne {𝕜 m n : Type*} [RCLike
     [Fintype n] [DecidableEq n] (x : EuclideanSpace 𝕜 m) (y : EuclideanSpace 𝕜 n) :
     toEuclideanLin.symm (rankOne 𝕜 x y) = .vecMulVec x (star y) := by
   simp [toLpLin, toMatrix', ← ext_iff, vecMulVec_apply, inner_single_right, mul_comm]
+
+namespace FiniteDimensional
+variable [Unique ι] (h : Module.finrank 𝕜 E = 1) {v : E} (hv : ‖v‖ = 1)
+
+variable (ι 𝕜 v) in
+/-- In an inner product space with dimension 1, a set `{v}` is an orthonormal basis for
+`‖v‖ = 1`. -/
+def orthonormalBasisSingleton : OrthonormalBasis ι 𝕜 E :=
+  (basisSingleton ι h v (by aesop)).toOrthonormalBasis (by simpa)
+
+@[simp]
+theorem orthonormalBasisSingleton_apply (i : ι) :
+   orthonormalBasisSingleton ι 𝕜 h v hv i = v := by
+  simp [orthonormalBasisSingleton]
+
+@[simp]
+theorem toBasis_orthonormalBasisSingleton :
+    (orthonormalBasisSingleton ι 𝕜 h v hv).toBasis = basisSingleton ι h v (by aesop) := by
+  simp [orthonormalBasisSingleton]
+
+@[simp]
+theorem orthonormalBasisSingleton_repr_apply (w : E) :
+    (orthonormalBasisSingleton ι 𝕜 h v hv).repr w = .single default ⟪v, w⟫ := by
+  ext
+  simp [OrthonormalBasis.repr_apply_apply, Unique.eq_default]
+
+theorem range_orthonormalBasisSingleton :
+    Set.range (orthonormalBasisSingleton ι 𝕜 h v hv) = {v} := by
+  simp
+
+end FiniteDimensional

Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

@@ -238,7 +238,7 @@ lemma preconnected_iff_reachable_eq_top : G.Preconnected ↔ G.Reachable = ⊤ :
   aesop (add simp Preconnected)
 
 lemma preconnected_bot_iff_subsingleton : (⊥ : SimpleGraph V).Preconnected ↔ Subsingleton V := by
-  refine ⟨fun h ↦ ?_, fun h ↦ by simpa [subsingleton_iff, ← reachable_bot] using h⟩
+  refine ⟨fun h ↦ ?_, fun h ↦ by simp [Preconnected]⟩
   contrapose! h
   simp [nontrivial_iff.mp h, Preconnected, reachable_bot]
 

Mathlib/Combinatorics/SimpleGraph/Diam.lean

@@ -151,8 +151,7 @@ lemma ediam_eq_top : G.ediam = ⊤ ↔ ∀ b < ⊤, ∃ u v, b < G.edist u v :=
   simp only [ediam, eccent, iSup_eq_top, lt_iSup_iff]
 
 lemma ediam_eq_zero_of_subsingleton [Subsingleton α] : G.ediam = 0 := by
-  rw [ediam_def, ENat.iSup_eq_zero]
-  simpa [edist_eq_zero_iff, Prod.forall] using subsingleton_iff.mp ‹_›
+  simp [ediam_def]
 
 lemma nontrivial_of_ediam_ne_zero (h : G.ediam ≠ 0) : Nontrivial α := by
   contrapose! h