Bump mathlib (#318)

FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean

@@ -8,10 +8,10 @@ import Mathlib.Order.CompletePartialOrder
 import Mathlib.RingTheory.DedekindDomain.Dvr
 import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
 import Mathlib.RingTheory.Henselian
+import Mathlib.Topology.Algebra.Algebra.Equiv
 import Mathlib.Topology.Algebra.Module.ModuleTopology
 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
 

FLT/FLT_files.lean

@@ -12,36 +12,36 @@ import FLT.GaloisRepresentation.HardlyRamified
 import FLT.GlobalLanglandsConjectures.GLnDefs
 import FLT.GlobalLanglandsConjectures.GLzero
 import FLT.GroupScheme.FiniteFlat
+import FLT.HIMExperiments.flatness
 import FLT.HaarMeasure.DistribHaarChar.Basic
 import FLT.HaarMeasure.DistribHaarChar.Padic
 import FLT.HaarMeasure.DistribHaarChar.RealComplex
 import FLT.HaarMeasure.DomMulActMeasure
 import FLT.HaarMeasure.MeasurableSpacePadics
 import FLT.Hard.Results
-import FLT.HIMExperiments.flatness
 import FLT.Junk.Algebra
 import FLT.Junk.Algebra2
 import FLT.Mathlib.Algebra.Group.Subgroup.Defs
 import FLT.Mathlib.Algebra.Module.LinearMap.Defs
 import FLT.Mathlib.Algebra.Order.Hom.Monoid
-import FLT.MathlibExperiments.Coalgebra.Monoid
-import FLT.MathlibExperiments.Coalgebra.Sweedler
-import FLT.MathlibExperiments.Coalgebra.TensorProduct
-import FLT.MathlibExperiments.HopfAlgebra.Basic
-import FLT.MathlibExperiments.IsCentralSimple
-import FLT.MathlibExperiments.IsFrobenius
 import FLT.Mathlib.GroupTheory.Index
 import FLT.Mathlib.LinearAlgebra.Determinant
 import FLT.Mathlib.LinearAlgebra.Span.Defs
 import FLT.Mathlib.MeasureTheory.Group.Action
+import FLT.Mathlib.NumberTheory.NumberField.Basic
 import FLT.Mathlib.NumberTheory.NumberField.Completion
 import FLT.Mathlib.NumberTheory.Padics.PadicIntegers
 import FLT.Mathlib.RepresentationTheory.Basic
-import FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
 import FLT.Mathlib.Topology.Algebra.Module.ModuleTopology
 import FLT.Mathlib.Topology.Algebra.Monoid
 import FLT.Mathlib.Topology.Constructions
 import FLT.Mathlib.Topology.Homeomorph
+import FLT.MathlibExperiments.Coalgebra.Monoid
+import FLT.MathlibExperiments.Coalgebra.Sweedler
+import FLT.MathlibExperiments.Coalgebra.TensorProduct
+import FLT.MathlibExperiments.HopfAlgebra.Basic
+import FLT.MathlibExperiments.IsCentralSimple
+import FLT.MathlibExperiments.IsFrobenius
 import FLT.NumberField.AdeleRing
 import FLT.NumberField.InfiniteAdeleRing
 import FLT.TateCurve.TateCurve

FLT/HaarMeasure/DistribHaarChar/Basic.lean

@@ -43,7 +43,7 @@ noncomputable def distribHaarChar : G →* ℝ≥0 where
     rw [addHaarScalarFactor_eq_mul _ (DomMulAct.mk g' • addHaar (G := A))]
     congr 1
     simp_rw [mul_smul]
-    rw [addHaarScalarFactor_dma_smul]
+    rw [addHaarScalarFactor_domSMul]
 
 variable (μ) in
 lemma addHaarScalarFactor_smul_eq_distribHaarChar (g : G) :
@@ -53,7 +53,7 @@ lemma addHaarScalarFactor_smul_eq_distribHaarChar (g : G) :
 variable (μ) in
 lemma addHaarScalarFactor_smul_inv_eq_distribHaarChar (g : G) :
     addHaarScalarFactor μ ((DomMulAct.mk g)⁻¹ • μ) = distribHaarChar A g := by
-  rw [← addHaarScalarFactor_dma_smul _ _ (DomMulAct.mk g)]
+  rw [← addHaarScalarFactor_domSMul _ _ (DomMulAct.mk g)]
   simp_rw [← mul_smul, mul_inv_cancel, one_smul]
   exact addHaarScalarFactor_smul_eq_distribHaarChar ..
 
@@ -69,7 +69,7 @@ variable [Regular μ] {s : Set A}
 
 variable (μ) in
 lemma distribHaarChar_mul (g : G) (s : Set A) : distribHaarChar A g * μ s = μ (g • s) := by
-  have : (DomMulAct.mk g • μ) s = μ (g • s) := by simp [dma_smul_apply]
+  have : (DomMulAct.mk g • μ) s = μ (g • s) := by simp [domSMul_apply]
   rw [eq_comm, ← nnreal_smul_coe_apply, ← addHaarScalarFactor_smul_eq_distribHaarChar μ,
     ← this, ← smul_apply, ← isAddLeftInvariant_eq_smul_of_regular]
 

FLT/HaarMeasure/DomMulActMeasure.lean

@@ -11,35 +11,18 @@ namespace MeasureTheory.Measure
 
 variable {G A : Type*} [Group G] [AddCommGroup A] [DistribMulAction G A]
   [MeasurableSpace A]
-  [MeasurableSpace G] -- not needed actually
-  [MeasurableSMul G A] -- We only need `MeasurableConstSMul` but we don't have this class.
+  -- We only need `MeasurableConstSMul G A` but we don't have this class. So we erroneously must
+  -- assume `MeasurableSpace G` + `MeasurableSMul G A`
+  [MeasurableSpace G] [MeasurableSMul G A]
 variable {μ ν : Measure A} {g : G}
 
-noncomputable
-instance : DistribMulAction Gᵈᵐᵃ (Measure A) where
-  smul g μ := μ.map ((DomMulAct.mk.symm g)⁻¹ • ·)
-  one_smul μ := show μ.map _ = _ by simp
-  mul_smul g g' μ := by
-    show μ.map _ = ((μ.map _).map _)
-    rw [map_map]
-    · simp [Function.comp_def, mul_smul]
-    · exact measurable_const_smul ..
-    · exact measurable_const_smul ..
-  smul_zero g := by
-    show (0 : Measure A).map _ = 0
-    simp
-  smul_add g μ ν := by
-    show (μ + ν).map _ = μ.map _ + ν.map _
-    rw [Measure.map_add]
-    exact measurable_const_smul ..
-
-lemma dma_smul_apply (μ : Measure A) (g : Gᵈᵐᵃ) (s : Set A) :
+lemma domSMul_apply (μ : Measure A) (g : Gᵈᵐᵃ) (s : Set A) :
     (g • μ) s = μ ((DomMulAct.mk.symm g) • s) := by
   refine ((MeasurableEquiv.smul ((DomMulAct.mk.symm g : G)⁻¹)).map_apply _).trans ?_
   congr 1
   exact Set.preimage_smul_inv (DomMulAct.mk.symm g) s
 
-lemma integral_dma_smul {α} [NormedAddCommGroup α] [NormedSpace ℝ α] (g : Gᵈᵐᵃ) (f : A → α) :
+lemma integral_domSMul {α} [NormedAddCommGroup α] [NormedSpace ℝ α] (g : Gᵈᵐᵃ) (f : A → α) :
     ∫ x, f x ∂g • μ = ∫ x, f ((DomMulAct.mk.symm g)⁻¹ • x) ∂μ :=
   integral_map_equiv (MeasurableEquiv.smul ((DomMulAct.mk.symm g : G)⁻¹)) f
 
@@ -59,28 +42,28 @@ instance (g : Gᵈᵐᵃ) : (g • μ).IsAddHaarMeasure :=
     (continuous_const_smul _) (continuous_const_smul _)
 
 variable (μ ν) in
-lemma addHaarScalarFactor_dma_smul (g : Gᵈᵐᵃ) :
+lemma addHaarScalarFactor_domSMul (g : Gᵈᵐᵃ) :
     addHaarScalarFactor (g • μ) (g • ν) = addHaarScalarFactor μ ν := by
   obtain ⟨⟨f, f_cont⟩, f_comp, f_nonneg, f_zero⟩ :
     ∃ f : C(A, ℝ), HasCompactSupport f ∧ 0 ≤ f ∧ f 0 ≠ 0 := exists_continuous_nonneg_pos 0
   have int_f_ne_zero : ∫ x, f x ∂g • ν ≠ 0 :=
     (f_cont.integral_pos_of_hasCompactSupport_nonneg_nonzero f_comp f_nonneg f_zero).ne'
   apply NNReal.coe_injective
   rw [addHaarScalarFactor_eq_integral_div (g • μ) (g • ν) f_cont f_comp int_f_ne_zero,
-    integral_dma_smul, integral_dma_smul]
+    integral_domSMul, integral_domSMul]
   refine (addHaarScalarFactor_eq_integral_div _ _ (by fun_prop) ?_ ?_).symm
   · exact f_comp.comp_isClosedEmbedding (Homeomorph.smul _).isClosedEmbedding
-  · rw [← integral_dma_smul]
+  · rw [← integral_domSMul]
     exact (f_cont.integral_pos_of_hasCompactSupport_nonneg_nonzero f_comp f_nonneg f_zero).ne'
 
 variable (μ) in
 lemma addHaarScalarFactor_smul_congr (g : Gᵈᵐᵃ) :
     addHaarScalarFactor μ (g • μ) = addHaarScalarFactor ν (g • ν) := by
-  rw [addHaarScalarFactor_eq_mul _ (g • ν), addHaarScalarFactor_dma_smul,
+  rw [addHaarScalarFactor_eq_mul _ (g • ν), addHaarScalarFactor_domSMul,
     mul_comm, ← addHaarScalarFactor_eq_mul]
 
 variable (μ) in
 lemma addHaarScalarFactor_smul_congr' (g : Gᵈᵐᵃ) :
     addHaarScalarFactor (g • μ) μ = addHaarScalarFactor (g • ν) ν := by
-  rw [addHaarScalarFactor_eq_mul _ (g • ν), addHaarScalarFactor_dma_smul,
+  rw [addHaarScalarFactor_eq_mul _ (g • ν), addHaarScalarFactor_domSMul,
     mul_comm, ← addHaarScalarFactor_eq_mul]