Merge branch 'main' into fujisaki-latex

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,13 +1,20 @@
+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 FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
 
+import Mathlib.RingTheory.DedekindDomain.IntegralClosure -- for example
+
 /-!
 
 # Base change of adele rings.
@@ -202,13 +209,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]
@@ -262,8 +274,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