Bump mathlib to v4.26.0

ClassFieldTheory.lean

@@ -40,27 +40,22 @@ import ClassFieldTheory.IsNonarchimedeanLocalField.ValuationExactSequence
 import ClassFieldTheory.LocalCFT.Continuity
 import ClassFieldTheory.LocalCFT.Teichmuller
 import ClassFieldTheory.Mathlib.Algebra.Algebra.Subalgebra.Basic
-import ClassFieldTheory.Mathlib.Algebra.Group.Action.Units
 import ClassFieldTheory.Mathlib.Algebra.Group.Solvable
-import ClassFieldTheory.Mathlib.Algebra.Group.Units.Basic
+import ClassFieldTheory.Mathlib.Algebra.Group.Units.Defs
 import ClassFieldTheory.Mathlib.Algebra.Group.Units.Hom
 import ClassFieldTheory.Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import ClassFieldTheory.Mathlib.Algebra.Homology.ConcreteCategory
-import ClassFieldTheory.Mathlib.Algebra.Homology.ImageToKernel
 import ClassFieldTheory.Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
 import ClassFieldTheory.Mathlib.Algebra.Homology.ShortComplex.Exact
 import ClassFieldTheory.Mathlib.Algebra.Homology.ShortComplex.ModuleCat
 import ClassFieldTheory.Mathlib.Algebra.Homology.ShortComplex.ShortExact
 import ClassFieldTheory.Mathlib.Algebra.Module.Equiv.Basic
 import ClassFieldTheory.Mathlib.Algebra.Module.Equiv.Defs
 import ClassFieldTheory.Mathlib.Algebra.Module.LinearMap.Defs
-import ClassFieldTheory.Mathlib.Algebra.Module.NatInt
-import ClassFieldTheory.Mathlib.Algebra.Module.Submodule.Range
 import ClassFieldTheory.Mathlib.Algebra.Module.Torsion.Basic
+import ClassFieldTheory.Mathlib.Algebra.Order.Group.OrderIso
 import ClassFieldTheory.Mathlib.Algebra.Order.GroupWithZero.Canonical
-import ClassFieldTheory.Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
 import ClassFieldTheory.Mathlib.Algebra.Order.Hom.Monoid
-import ClassFieldTheory.Mathlib.CategoryTheory.Abelian.Exact
 import ClassFieldTheory.Mathlib.CategoryTheory.Category.Basic
 import ClassFieldTheory.Mathlib.CategoryTheory.Category.Cat
 import ClassFieldTheory.Mathlib.Data.Finset.Range

ClassFieldTheory/Cohomology/AugmentationModule.lean

@@ -1,5 +1,5 @@
 import ClassFieldTheory.Cohomology.Functors.Restriction
-import ClassFieldTheory.Cohomology.Functors.UpDown
+import ClassFieldTheory.Cohomology.IndCoind.TrivialCohomology
 import ClassFieldTheory.Cohomology.LeftRegular
 import ClassFieldTheory.Cohomology.TrivialCohomology
 import ClassFieldTheory.Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

ClassFieldTheory/Cohomology/FiniteCyclic/UpDown.lean

@@ -1,9 +1,7 @@
 import ClassFieldTheory.Cohomology.Functors.UpDown
 import ClassFieldTheory.Cohomology.IndCoind.Finite
-import ClassFieldTheory.Mathlib.Algebra.Homology.ImageToKernel
 import ClassFieldTheory.Mathlib.Algebra.Homology.ShortComplex.Exact
 import ClassFieldTheory.Mathlib.Algebra.Homology.ShortComplex.ModuleCat
-import ClassFieldTheory.Mathlib.CategoryTheory.Abelian.Exact
 import ClassFieldTheory.Mathlib.GroupTheory.SpecificGroups.Cyclic
 
 /-!

ClassFieldTheory/Cohomology/Functors/Corestriction.lean

@@ -4,12 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard, Aaron Liu, Yunzhou Xie
 -/
 import ClassFieldTheory.Cohomology.Functors.UpDown
-import ClassFieldTheory.Mathlib.GroupTheory.GroupAction.Quotient
+import ClassFieldTheory.Mathlib.Algebra.Module.Torsion.Basic
 import ClassFieldTheory.Mathlib.CategoryTheory.Category.Basic
 import ClassFieldTheory.Mathlib.CategoryTheory.Category.Cat
+import ClassFieldTheory.Mathlib.GroupTheory.GroupAction.Quotient
 import ClassFieldTheory.Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
-import ClassFieldTheory.Mathlib.Algebra.Module.NatInt
-import ClassFieldTheory.Mathlib.Algebra.Module.Torsion.Basic
 
 /-!
 # Corestriction
@@ -303,14 +302,15 @@ lemma torsion_of_finite_of_neZero {n : ℕ} [NeZero n] [DecidableEq G] (M : Rep
 
 lemma pTorsion_eq_sylowTorsion {n : ℕ} [NeZero n] [Finite G] [DecidableEq G] (M : Rep R G)
     (p : ℕ) [Fact p.Prime] (P : Sylow p G) (x : groupCohomology M n) :
-    (∃ d, (p ^ d) • x = 0) ↔ x ∈ Submodule.torsionBy R _ (Nat.card P) :=
-  ⟨fun ⟨d, hd⟩ ↦ Submodule.mem_torsionBy_iff _ _ |>.2 <| by
+    (∃ d, (p ^ d) • x = 0) ↔ x ∈ Submodule.torsionBy R _ (Nat.card P) where
+  mp := by
+    rintro ⟨d, hd⟩
     obtain ⟨k, hk1, hk2⟩ := Nat.dvd_prime_pow Fact.out|>.1 <| Nat.gcd_dvd_right (Nat.card G) (p ^ d)
     obtain ⟨m, hm⟩ := P.pow_dvd_card_of_pow_dvd_card (hk2 ▸ Nat.gcd_dvd_left (Nat.card G) (p ^ d))
-    simp [hm, mul_comm _ m, mul_smul, - Nat.cast_pow, Nat.cast_smul_eq_nsmul, ← hk2,
-      AddCommGroup.isTorsion_gcd_iff _ (p ^ d) x|>.2 ⟨torsion_of_finite_of_neZero M x, hd⟩],
-    fun h ↦ ⟨(Nat.card G).factorization p, P.card_eq_multiplicity ▸ by
-    simpa [Nat.cast_smul_eq_nsmul] using h⟩⟩
+    simp [hm, mul_comm _ m, mul_smul, - Nat.cast_pow, Nat.cast_smul_eq_nsmul, ← hk2, smul_comm m]
+    simp [smul_comm _ m, hd, torsion_of_finite_of_neZero]
+  mpr h := ⟨(Nat.card G).factorization p, P.card_eq_multiplicity ▸ by
+    simpa [Nat.cast_smul_eq_nsmul] using h⟩
 
 lemma injects_to_sylowCoh {n : ℕ} [NeZero n] [Finite G] [DecidableEq G] (M : Rep R G)
     (p : ℕ) [Fact p.Prime] (P : Sylow p G) : Function.Injective

ClassFieldTheory/Cohomology/IndCoind/TrivialCohomology.lean

@@ -6,7 +6,6 @@ Authors: Yaël Dillies, Nailin Guan, Gareth Ma, Arend Mellendijk, Yannis Monbru,
 -/
 import ClassFieldTheory.Cohomology.IndCoind.Finite
 import ClassFieldTheory.Cohomology.TrivialCohomology
-import ClassFieldTheory.Mathlib.Algebra.Module.Submodule.Range
 import ClassFieldTheory.Mathlib.LinearAlgebra.Finsupp.Defs
 import ClassFieldTheory.Mathlib.RepresentationTheory.Rep
 import Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro

ClassFieldTheory/Cohomology/Subrep/Basic.lean

@@ -14,19 +14,20 @@ structure Subrep {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G) extends Su
   le_comap (g) : toSubmodule ≤ toSubmodule.comap (A.ρ g)
 
 namespace Subrep
-variable {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G)
+variable {k G : Type u} [CommRing k] [Monoid G] {A : Rep k G}
+
+lemma toSubmodule_injective : (toSubmodule : Subrep A → Submodule k A.V).Injective :=
+  fun ⟨_, _⟩ _ _ ↦ by congr!
 
 instance : SetLike (Subrep A) A.V where
   coe w := w.carrier
-  coe_injective' := fun ⟨_, _⟩ ⟨_, _⟩ h ↦ by congr; exact SetLike.coe_injective h
+  coe_injective' := SetLike.coe_injective.comp toSubmodule_injective
 
 instance : AddSubgroupClass (Subrep A) A.V where
   add_mem {w} := w.add_mem
   zero_mem {w} := w.zero_mem
   neg_mem {w} := w.neg_mem
 
-variable {A}
-
 /-- `w` interpreted as a `G`-rep. -/
 @[coe] noncomputable def toRep (w : Subrep A) : Rep k G :=
   .subrepresentation _ w.toSubmodule w.le_comap
@@ -43,12 +44,14 @@ noncomputable def quotient (w : Subrep A) : Rep k G :=
 @[simps!] noncomputable def mkQ (w : Subrep A) : A ⟶ w.quotient :=
   A.mkQ _ _
 
+instance : Min (Subrep A) where
+  min w₁ w₂ := ⟨w₁.toSubmodule ⊓ w₂.toSubmodule, fun g ↦ inf_le_inf (w₁.le_comap g) (w₂.le_comap g)⟩
+
+@[simp] lemma toSubmodule_inf (w₁ w₂ : Subrep A) :
+    (w₁ ⊓ w₂).toSubmodule = w₁.toSubmodule ⊓ w₂.toSubmodule := rfl
+
 -- todo: complete lattice, two adjoint functors (aka galois insertions)
-instance : SemilatticeInf (Subrep A) where
-  inf w₁ w₂ := ⟨w₁.toSubmodule ⊓ w₂.toSubmodule, fun g ↦ inf_le_inf (w₁.le_comap g) (w₂.le_comap g)⟩
-  inf_le_left w₁ _ := inf_le_left (a := w₁.toSubmodule)
-  inf_le_right w₁ _ := inf_le_right (a := w₁.toSubmodule)
-  le_inf w₁ _ _ := le_inf (a := w₁.toSubmodule)
+instance : SemilatticeInf (Subrep A) := toSubmodule_injective.semilatticeInf _ toSubmodule_inf
 
 instance : OrderTop (Subrep A) where
   top := ⟨⊤, fun _ _ _ ↦ trivial⟩

ClassFieldTheory/IsNonarchimedeanLocalField/Actions.lean

@@ -1,6 +1,5 @@
 import ClassFieldTheory.IsNonarchimedeanLocalField.Basic
 import ClassFieldTheory.Mathlib.Topology.Algebra.Valued.ValuativeRel
-import Mathlib.FieldTheory.Galois.IsGaloisGroup
 
 /-! # Actions on local fields
 

ClassFieldTheory/IsNonarchimedeanLocalField/Basic.lean

@@ -1,19 +1,21 @@
 import ClassFieldTheory.LocalCFT.Continuity
+import ClassFieldTheory.Mathlib.Algebra.Order.Group.OrderIso
 import ClassFieldTheory.Mathlib.Algebra.Order.GroupWithZero.Canonical
-import ClassFieldTheory.Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
 import ClassFieldTheory.Mathlib.Data.Int.WithZero
 import ClassFieldTheory.Mathlib.RingTheory.DiscreteValuationRing.Basic
 import ClassFieldTheory.Mathlib.RingTheory.Localization.AtPrime.Basic
 import ClassFieldTheory.Mathlib.RingTheory.Unramified.Basic
 import ClassFieldTheory.Mathlib.RingTheory.Unramified.LocalRing
+import ClassFieldTheory.Mathlib.RingTheory.LocalRing.ResidueField.Basic
 import ClassFieldTheory.Mathlib.Topology.Algebra.Valued.ValuativeRel
+import ClassFieldTheory.Mathlib.Topology.Algebra.Valued.NormedValued
 import Mathlib.Analysis.Normed.Module.FiniteDimension
+import Mathlib.Analysis.Normed.Unbundled.SpectralNorm
 import Mathlib.FieldTheory.Finite.GaloisField
 import Mathlib.NumberTheory.LocalField.Basic
 import Mathlib.NumberTheory.Padics.ProperSpace
 import Mathlib.NumberTheory.Padics.ValuativeRel
 import Mathlib.NumberTheory.RamificationInertia.Basic
-import Mathlib.Order.CompletePartialOrder
 
 /-!
 # Non-Archimedean Local Fields

ClassFieldTheory/IsNonarchimedeanLocalField/UnramifiedCohomology.lean

@@ -1,4 +1,5 @@
 import ClassFieldTheory.IsNonarchimedeanLocalField.ValuationExactSequence
+import Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
 
 /-! # Galois cohomology of unramified extensions of local fields
 

ClassFieldTheory/IsNonarchimedeanLocalField/Valuation.lean

@@ -3,18 +3,15 @@ Copyright (c) 2025 Kevin Buzzard. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard
 -/
-import ClassFieldTheory.Cohomology.Functors.Restriction
 import ClassFieldTheory.IsNonarchimedeanLocalField.Basic
 import ClassFieldTheory.Mathlib.Topology.Algebra.Valued.ValuativeRel
-import Mathlib.FieldTheory.Galois.IsGaloisGroup
-/-
 
+/-!
 # 1 → 𝒪[K]ˣ → Kˣ → ℤ → 0
 
 We construct the short exact sequence `0 → Additive 𝒪[K]ˣ → Additive (Kˣ) → ℤ → 0` in
 the following sense: we define the maps `kerV K` and `v K`, prove the first is
 injective, the second is surjective, and the pair is `Function.Exact`.
-
 -/
 
 namespace ValuativeRel

ClassFieldTheory/IsNonarchimedeanLocalField/ValuationExactSequence.lean

@@ -1,21 +1,20 @@
 import ClassFieldTheory.Cohomology.Subrep.ShortExact
 import ClassFieldTheory.IsNonarchimedeanLocalField.Actions
 import ClassFieldTheory.IsNonarchimedeanLocalField.Valuation
-import ClassFieldTheory.Mathlib.Algebra.Group.Action.Units
-/-
+import Mathlib.FieldTheory.Galois.IsGaloisGroup
 
+/-!
 # 1 → 𝒪[L]ˣ → Lˣ → ℤ → 0 as G-module
 
 If L/K is a finite Galois extension of nonarch local fields, we construct the
 short exact sequence `0 → Additive 𝒪[K]ˣ → Additive (Kˣ) → ℤ → 0` in `Rep ℤ G`
-
 -/
 
 /-- The `G`-module `Mˣ` where `G` acts on `M` distributively. -/
 noncomputable abbrev Rep.units
     (G M : Type) [Monoid G] [CommMonoid M] [MulDistribMulAction G M] :
     Rep ℤ G :=
-  let : MulDistribMulAction G Mˣ := Units.mulDistribMulActionRight G M
+  let : MulDistribMulAction G Mˣ := Units.mulDistribMulActionRight
   Rep.ofMulDistribMulAction G Mˣ
 
 namespace IsNonarchimedeanLocalField

ClassFieldTheory/LocalCFT/Continuity.lean

@@ -1,9 +1,10 @@
-import Mathlib.Analysis.Normed.Unbundled.SpectralNorm
-import ClassFieldTheory.Mathlib.Topology.Algebra.Valued.NormedValued
+import ClassFieldTheory.Mathlib.RingTheory.Valuation.ValuativeRel
+import Mathlib.FieldTheory.Minpoly.Field
+import Mathlib.Topology.Algebra.Algebra
 import Mathlib.Topology.Algebra.Valued.ValuativeRel
 import Mathlib.Topology.Algebra.Valued.ValuedField
-/-!
 
+/-!
 # Main theorems
 
 * `continuous_algebraMap_of_density` Given a valuative algebraic extension of valuative topological
@@ -12,6 +13,7 @@ import Mathlib.Topology.Algebra.Valued.ValuedField
 * An instance of `ContinuousSMul K L` if `K,L` are valuative topological fields and `L/K`
   is a valuative algebraic extension.
 -/
+
 open ValuativeRel
 
 theorem Valuation.sum_eq_iSup {ι R Γ₀ : Type*} (f : ι → R) (s : Finset ι)

ClassFieldTheory/Mathlib/Algebra/Group/Units/Basic.lean → ClassFieldTheory/Mathlib/Algebra/Group/Units/Defs.lean

@@ -1,4 +1,4 @@
-import Mathlib.Algebra.Group.Units.Basic
+import Mathlib.Algebra.Group.Units.Defs
 
 theorem IsUnit.of_mul {M : Type*} [Monoid M] {x y z : M}
     (hxy : IsUnit (x * y)) (hzx : IsUnit (z * x)) : IsUnit x :=

ClassFieldTheory/Mathlib/Algebra/Group/Units/Hom.lean

@@ -1,4 +1,4 @@
-import ClassFieldTheory.Mathlib.Algebra.Group.Units.Basic
+import ClassFieldTheory.Mathlib.Algebra.Group.Units.Defs
 import Mathlib.Algebra.Group.Units.Hom
 
 theorem isLocalHom_iff_one {R S F : Type*} [Monoid R] [Monoid S]

ClassFieldTheory/Mathlib/Algebra/Homology/ShortComplex/Exact.lean

@@ -1,5 +1,4 @@
-import ClassFieldTheory.Mathlib.CategoryTheory.Abelian.Exact
-import Mathlib.CategoryTheory.Limits.Shapes.Kernels
+import Mathlib.Algebra.Homology.ShortComplex.Exact
 
 noncomputable section
 

ClassFieldTheory/Mathlib/Algebra/Module/Torsion/Basic.lean

@@ -4,10 +4,10 @@ import Mathlib.Algebra.Module.Torsion.Basic
 def Module.IsTorsionBy.coprime_decompose {k m1 m2: ℕ} {R M : Type*} [CommRing R] [AddCommGroup M]
     [Module R M] (hk : k = m1 * m2) (hmm : m1.Coprime m2) (hA : Module.IsTorsionBy R M k):
     M ≃ₗ[R] Submodule.torsionBy R M m1 × Submodule.torsionBy R M m2 where
-  toFun m := ⟨⟨(m2 : R) • m, by simp [← MulAction.mul_smul, ← Nat.cast_mul, ← hk, hA]⟩,
-    ⟨(m1 : R) • m, by simp [← MulAction.mul_smul, mul_comm, ← Nat.cast_mul, ← hk, hA]⟩⟩
+  toFun m := ⟨⟨(m2 : R) • m, by simp [← mul_smul, ← Nat.cast_mul, ← hk, hA]⟩,
+    ⟨(m1 : R) • m, by simp [← mul_smul, mul_comm, ← Nat.cast_mul, ← hk, hA]⟩⟩
   map_add' := by simp
-  map_smul' := by simp [← MulAction.mul_smul, mul_comm]
+  map_smul' := by simp [← mul_smul, mul_comm]
   invFun := fun ⟨x1, x2⟩ ↦ (m1.gcdB m2 : R) • x1.1 + (m1.gcdA m2 : R) • x2.1
   left_inv x := by
     simp only [← smul_assoc, smul_eq_mul, ← add_smul]

ClassFieldTheory/Mathlib/Algebra/Order/GroupWithZero/Unbundled/OrderIso.lean → ClassFieldTheory/Mathlib/Algebra/Order/Group/OrderIso.lean

@@ -1,4 +1,4 @@
-import Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
+import Mathlib.Algebra.Order.Group.OrderIso
 
 @[simp] lemma map_lt_one_iff {F α β : Type*} [Preorder α] [Preorder β]
     [MulOneClass α] [MulOneClass β] [EquivLike F α β] [OrderIsoClass F α β] [MulEquivClass F α β]

ClassFieldTheory/Mathlib/CategoryTheory/Category/Cat.lean

@@ -1,4 +1,3 @@
-import Mathlib.Data.Set.Function
 import Mathlib.CategoryTheory.Category.Cat
 
 open CategoryTheory

ClassFieldTheory/Mathlib/RingTheory/DiscreteValuationRing/Basic.lean

@@ -15,7 +15,7 @@ theorem factors_maximalIdeal_pow (n : ℕ) :
     Multiset.replicate n (IsLocalRing.maximalIdeal R) :=
   UniqueFactorizationMonoid.factors_spec_of_subsingleton_units
     (Multiset.mem_replicate.not.mpr <| mt And.right not_a_field'.symm)
-    (by simp; rfl) (by simp [Multiset.mem_replicate])
+    (by simp) (by simp [Multiset.mem_replicate])
 
 theorem factors_maximalIdeal :
     UniqueFactorizationMonoid.factors (IsLocalRing.maximalIdeal R) = {IsLocalRing.maximalIdeal R} :=