Bump to v4.16.0 rc2

FLT/AutomorphicForm/QuaternionAlgebra/Defs.lean

@@ -33,7 +33,7 @@ noncomputable abbrev incl₁ : Dˣ →* Dfx F D :=
   Units.map Algebra.TensorProduct.includeLeftRingHom.toMonoidHom
 
 noncomputable abbrev incl₂ : (FiniteAdeleRing (𝓞 F) F)ˣ →* Dfx F D :=
-  Units.map Algebra.TensorProduct.rightAlgebra.toMonoidHom
+  Units.map Algebra.TensorProduct.rightAlgebra.algebraMap.toMonoidHom
 
 /-!
 This definition is made in mathlib-generality but is *not* the definition of an automorphic

FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean

@@ -1,12 +1,19 @@
+import Mathlib.Algebra.Algebra.Subalgebra.Pi
+import Mathlib.Algebra.Group.Int.TypeTags
+import Mathlib.Algebra.Lie.OfAssociative
+import Mathlib.Algebra.Order.Group.Int
 import Mathlib.FieldTheory.Separable
 import Mathlib.NumberTheory.RamificationInertia.Basic
+import Mathlib.Order.CompletePartialOrder
+import Mathlib.RingTheory.DedekindDomain.Dvr
 import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
-import Mathlib.RingTheory.DedekindDomain.IntegralClosure
-import Mathlib.Topology.Algebra.Algebra
+import Mathlib.RingTheory.Henselian
 import Mathlib.Topology.Algebra.Module.ModuleTopology
-import FLT.Mathlib.Algebra.Algebra.Subalgebra.Pi
+import Mathlib.Topology.Separation.CompletelyRegular
 import FLT.Mathlib.Algebra.Order.Hom.Monoid
 
+import Mathlib.RingTheory.DedekindDomain.IntegralClosure -- for example
+
 /-!
 
 # Base change of adele rings.
@@ -194,13 +201,18 @@ noncomputable def adicCompletionComapRingHom
 -- So we need to be careful making L_w into a K-algebra
 -- https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/beef.20up.20smul.20on.20completion.20to.20algebra.20instance/near/484166527
 -- Hopefully resolved in https://github.com/leanprover-community/mathlib4/pull/19466
+variable (w : HeightOneSpectrum B) in
+noncomputable instance : SMul K (w.adicCompletion L) := inferInstanceAs <|
+  SMul K (@UniformSpace.Completion L w.adicValued.toUniformSpace)
+
 variable (w : HeightOneSpectrum B) in
 noncomputable instance : Algebra K (adicCompletion L w) where
-  toFun k := algebraMap L (adicCompletion L w) (algebraMap K L k)
-  map_one' := by simp only [map_one]
-  map_mul' k₁ k₂ := by simp only [map_mul]
-  map_zero' := by simp only [map_zero]
-  map_add' k₁ k₂ := by simp only [map_add]
+  algebraMap :=
+    { toFun k := algebraMap L (adicCompletion L w) (algebraMap K L k)
+      map_one' := by simp only [map_one]
+      map_mul' k₁ k₂ := by simp only [map_mul]
+      map_zero' := by simp only [map_zero]
+      map_add' k₁ k₂ := by simp only [map_add] }
   commutes' k lhat := mul_comm _ _
   smul_def' k lhat := by
     simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
@@ -253,8 +265,8 @@ lemma v_adicCompletionComapAlgHom
   · exact Valued.continuous_valuation.pow _
   · exact Valued.continuous_valuation.comp (adicCompletionComapAlgHom ..).cont
   intro a
-  simp only [Valued.valuedCompletion_apply, adicCompletionComapAlgHom_coe]
-  show v.valuation a ^ _ = (w.valuation _)
+  simp_rw [adicCompletionComapAlgHom_coe, adicCompletion, Valued.valuedCompletion_apply,
+    adicValued_apply]
   subst hvw
   rw [← valuation_comap A K L B w a]
 

FLT/DivisionAlgebra/Finiteness.lean

@@ -9,7 +9,6 @@ import Mathlib.NumberTheory.NumberField.Basic
 import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
 import Mathlib.Algebra.Group.Subgroup.Pointwise
 import FLT.Mathlib.Topology.Algebra.Module.ModuleTopology
-import FLT.NumberField.IsTotallyReal
 import FLT.NumberField.AdeleRing
 import Mathlib.GroupTheory.DoubleCoset
 

FLT/FLT_files.lean

@@ -21,8 +21,6 @@ import FLT.Hard.Results
 import FLT.HIMExperiments.flatness
 import FLT.Junk.Algebra
 import FLT.Junk.Algebra2
-import FLT.Mathlib.Algebra.Algebra.Subalgebra.Pi
-import FLT.Mathlib.Algebra.BigOperators.Finprod
 import FLT.Mathlib.Algebra.Group.Subgroup.Defs
 import FLT.Mathlib.Algebra.Module.LinearMap.Defs
 import FLT.Mathlib.Algebra.Order.Hom.Monoid
@@ -32,7 +30,6 @@ import FLT.MathlibExperiments.Coalgebra.TensorProduct
 import FLT.MathlibExperiments.HopfAlgebra.Basic
 import FLT.MathlibExperiments.IsCentralSimple
 import FLT.MathlibExperiments.IsFrobenius
-import FLT.Mathlib.GroupTheory.Complement
 import FLT.Mathlib.GroupTheory.Index
 import FLT.Mathlib.LinearAlgebra.Determinant
 import FLT.Mathlib.LinearAlgebra.Span.Defs
@@ -47,5 +44,4 @@ import FLT.Mathlib.Topology.Constructions
 import FLT.Mathlib.Topology.Homeomorph
 import FLT.NumberField.AdeleRing
 import FLT.NumberField.InfiniteAdeleRing
-import FLT.NumberField.IsTotallyReal
 import FLT.TateCurve.TateCurve

FLT/GlobalLanglandsConjectures/GLnDefs.lean

@@ -166,7 +166,7 @@ variable (n : ℕ)
 variable (G : Type) [TopologicalSpace G] [Group G]
   (E : Type) [NormedAddCommGroup E] [NormedSpace ℝ E]
   [ChartedSpace E G]
-  [LieGroup 𝓘(ℝ, E) G]
+  [LieGroup 𝓘(ℝ, E) ⊤ G]
 
 def action :
     LeftInvariantDerivation 𝓘(ℝ, E) G →ₗ⁅ℝ⁆ (Module.End ℝ C^∞⟮𝓘(ℝ, E), G; ℝ⟯) where

FLT/GlobalLanglandsConjectures/GLzero.lean

@@ -80,7 +80,7 @@ def ofComplex (c : ℂ) : AutomorphicFormForGLnOverQ 0 ρ := {
       rw [annihilator]
       simp
       exact {
-        out := by sorry
+        fg_top := by sorry
       }
     has_finite_level := by
       let U : Subgroup (GL (Fin 0) (DedekindDomain.FiniteAdeleRing ℤ ℚ)) := {

FLT/HIMExperiments/flatness.lean

@@ -127,7 +127,7 @@ theorem flat_iff_torsion_eq_bot [IsPrincipalIdealRing R] [IsDomain R] :
     -- now assume R is a PID and M is a torsionfree R-module
   · intro htors
     -- we need to show that if I is an ideal of R then the natural map I ⊗ M → M is injective
-    constructor
+    rw [iff_lift_lsmul_comp_subtype_injective]
     rintro I -
     -- If I = 0 this is obvious because I ⊗ M is a subsingleton (i.e. has ≤1 element)
     obtain (rfl | h) := eq_or_ne I ⊥

FLT/Mathlib/Algebra/Module/LinearMap/Defs.lean

@@ -1,6 +1,6 @@
+import Mathlib.Algebra.BigOperators.Finprod
 import Mathlib.Algebra.Module.LinearMap.Defs
 import Mathlib.Data.Fintype.Option
-import FLT.Mathlib.Algebra.BigOperators.Finprod
 
 theorem LinearMap.finsum_apply {R : Type*} [Semiring R] {A B : Type*} [AddCommMonoid A] [Module R A]
     [AddCommMonoid B] [Module R B] {ι : Type*} [Finite ι] (φ : ∀ _ : ι, A →ₗ[R] B) (a : A) :
@@ -12,4 +12,5 @@ theorem LinearMap.finsum_apply {R : Type*} [Semiring R] {A B : Type*} [AddCommMo
     · exact (finsum_comp_equiv e).symm
   · simp [finsum_of_isEmpty]
   · case h_option X _ hX =>
-    simp [finsum_option, hX]
+    rw [finsum_option (Set.toFinite _), finsum_option (Set.toFinite _)]
+    simp [hX]

FLT/Mathlib/MeasureTheory/Group/Action.lean

@@ -1,8 +1,8 @@
+import Mathlib.GroupTheory.Complement
 import Mathlib.MeasureTheory.Group.Action
 import Mathlib.MeasureTheory.Group.Pointwise
 import Mathlib.Topology.Algebra.InfiniteSum.ENNReal
 import FLT.Mathlib.Algebra.Group.Subgroup.Defs
-import FLT.Mathlib.GroupTheory.Complement
 import FLT.Mathlib.GroupTheory.Index
 
 /-!
@@ -45,12 +45,12 @@ instance (μ : Measure G) [μ.IsMulRightInvariant] :
 @[to_additive index_mul_addHaar_addSubgroup]
 lemma index_mul_haar_subgroup [H.FiniteIndex] (hH : MeasurableSet (H : Set G)) (μ : Measure G)
     [μ.IsMulLeftInvariant] : H.index * μ H = μ univ := by
-  obtain ⟨s, hs, -⟩ := H.exists_left_transversal 1
-  have hs' : Finite s := finite_of_mem_leftTransversals hs
+  obtain ⟨s, hs, -⟩ := H.exists_isComplement_left 1
+  have hs' : Finite s := hs.finite_left_iff.mpr inferInstance
   calc
     H.index * μ H = ∑' a : s, μ (a.val • H) := by
       simp [measure_smul]
-      rw [← Set.Finite.cast_ncard_eq hs', ← Nat.card_coe_set_eq, card_left_transversal hs]
+      rw [← Set.Finite.cast_ncard_eq hs', ← Nat.card_coe_set_eq, hs.card_left]
       norm_cast
     _ = μ univ := by
       rw [← measure_iUnion _ fun _ ↦ hH.const_smul _]

FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean

@@ -255,7 +255,7 @@ theorem Module.continuous_bilinear_of_pi_finite (ι : Type*) [Finite ι]
       -- Is there a missing delaborator? No ∑ᶠ notation
       change (∑ᶠ (i : ι), Pi.single i (f i)) j = f j
       -- last tactic has no effect
-      rw [finsum_apply]
+      rw [finsum_apply (Set.toFinite _)]
       convert finsum_eq_single (fun i ↦ Pi.single i (f i) j) j
         (by simp (config := {contextual := true})) using 1
       simp

FLT/NumberField/AdeleRing.lean

@@ -1,17 +1,18 @@
 import Mathlib
 import FLT.Mathlib.NumberTheory.NumberField.Basic
-import FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation
 
 universe u
 
+open NumberField
+
 section LocallyCompact
 
 -- see https://github.com/smmercuri/adele-ring_locally-compact
 -- for a proof of this
 
 variable (K : Type*) [Field K] [NumberField K]
 
-instance NumberField.AdeleRing.locallyCompactSpace : LocallyCompactSpace (AdeleRing K) :=
+instance NumberField.AdeleRing.locallyCompactSpace : LocallyCompactSpace (AdeleRing (𝓞 K) K) :=
   sorry -- issue #253
 
 end LocallyCompact
@@ -22,10 +23,10 @@ end BaseChange
 
 section Discrete
 
-open NumberField DedekindDomain
+open DedekindDomain
 
-theorem Rat.AdeleRing.zero_discrete : ∃ U : Set (AdeleRing ℚ),
-    IsOpen U ∧ (algebraMap ℚ (AdeleRing ℚ)) ⁻¹' U = {0} := by
+theorem Rat.AdeleRing.zero_discrete : ∃ U : Set (AdeleRing (𝓞 ℚ) ℚ),
+    IsOpen U ∧ (algebraMap ℚ (AdeleRing (𝓞 ℚ) ℚ)) ⁻¹' U = {0} := by
   use {f | ∀ v, f v ∈ (Metric.ball 0 1)} ×ˢ
     {f | ∀ v , f v ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ v}
   refine ⟨?_, ?_⟩
@@ -36,7 +37,7 @@ theorem Rat.AdeleRing.zero_discrete : ∃ U : Set (AdeleRing ℚ),
     · intro x hx
       rw [Set.mem_preimage] at hx
       simp only [Set.mem_singleton_iff]
-      have : (algebraMap ℚ (AdeleRing ℚ)) x =
+      have : (algebraMap ℚ (AdeleRing (𝓞 ℚ) ℚ)) x =
         (algebraMap ℚ (InfiniteAdeleRing ℚ) x, algebraMap ℚ (FiniteAdeleRing (𝓞 ℚ) ℚ) x)
       · rfl
       rw [this] at hx
@@ -52,7 +53,7 @@ theorem Rat.AdeleRing.zero_discrete : ∃ U : Set (AdeleRing ℚ),
       simp at h1
       have intx: ∃ (y:ℤ), y = x
       · obtain ⟨z, hz⟩ := IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_one
-            (𝓞 ℚ) ℚ x <| fun v ↦ by
+            ℚ x <| fun v ↦ by
           specialize h2 v
           letI : UniformSpace ℚ := v.adicValued.toUniformSpace
           rw [IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers] at h2
@@ -88,11 +89,11 @@ theorem Rat.AdeleRing.zero_discrete : ∃ U : Set (AdeleRing ℚ),
 -- Maybe this discreteness isn't even stated in the best way?
 -- I'm ambivalent about how it's stated
 open Pointwise in
-theorem Rat.AdeleRing.discrete : ∀ q : ℚ, ∃ U : Set (AdeleRing ℚ),
-    IsOpen U ∧ (algebraMap ℚ (AdeleRing ℚ)) ⁻¹' U = {q} := by
+theorem Rat.AdeleRing.discrete : ∀ q : ℚ, ∃ U : Set (AdeleRing (𝓞 ℚ) ℚ),
+    IsOpen U ∧ (algebraMap ℚ (AdeleRing (𝓞 ℚ) ℚ)) ⁻¹' U = {q} := by
   obtain ⟨V, hV, hV0⟩ := zero_discrete
   intro q
-  set ι  := algebraMap ℚ (AdeleRing ℚ)    with hι
+  set ι  := algebraMap ℚ (AdeleRing (𝓞 ℚ) ℚ)    with hι
   set qₐ := ι q                           with hqₐ
   set f  := Homeomorph.subLeft qₐ         with hf
   use f ⁻¹' V, f.isOpen_preimage.mpr hV
@@ -104,8 +105,8 @@ theorem Rat.AdeleRing.discrete : ∀ q : ℚ, ∃ U : Set (AdeleRing ℚ),
 
 variable (K : Type*) [Field K] [NumberField K]
 
-theorem NumberField.AdeleRing.discrete : ∀ k : K, ∃ U : Set (AdeleRing K),
-    IsOpen U ∧ (algebraMap K (AdeleRing K)) ⁻¹' U = {k} := sorry -- issue #257
+theorem NumberField.AdeleRing.discrete : ∀ k : K, ∃ U : Set (AdeleRing (𝓞 K) K),
+    IsOpen U ∧ (algebraMap K (AdeleRing (𝓞 K) K)) ⁻¹' U = {k} := sorry -- issue #257
 
 end Discrete
 
@@ -114,13 +115,13 @@ section Compact
 open NumberField
 
 theorem Rat.AdeleRing.cocompact :
-    CompactSpace (AdeleRing ℚ ⧸ AddMonoidHom.range (algebraMap ℚ (AdeleRing ℚ)).toAddMonoidHom) :=
+    CompactSpace (AdeleRing (𝓞 ℚ) ℚ ⧸ AddMonoidHom.range (algebraMap ℚ (AdeleRing (𝓞 ℚ) ℚ)).toAddMonoidHom) :=
   sorry -- issue #258
 
 variable (K : Type*) [Field K] [NumberField K]
 
 theorem NumberField.AdeleRing.cocompact :
-    CompactSpace (AdeleRing K ⧸ AddMonoidHom.range (algebraMap K (AdeleRing K)).toAddMonoidHom) :=
+    CompactSpace (AdeleRing (𝓞 K) K ⧸ AddMonoidHom.range (algebraMap K (AdeleRing (𝓞 K) K)).toAddMonoidHom) :=
   sorry -- issue #259
 
 end Compact