bump to nightly-2023-03-03-22

mathlib commit leanprover-community/mathlib@62e8311

Mathbin/Algebra/Algebra/Bilinear.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 
 ! This file was ported from Lean 3 source module algebra.algebra.bilinear
-! leanprover-community/mathlib commit 657df4339ae6ceada048c8a2980fb10e393143ec
+! leanprover-community/mathlib commit 832f7b9162039c28b9361289c8681f155cae758f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -16,6 +16,9 @@ import Mathbin.LinearAlgebra.TensorProduct
 /-!
 # Facts about algebras involving bilinear maps and tensor products
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We move a few basic statements about algebras out of `algebra.algebra.basic`,
 in order to avoid importing `linear_algebra.bilinear_map` and
 `linear_algebra.tensor_product` unnecessarily.

Mathbin/Algebra/Algebra/Operations.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 
 ! This file was ported from Lean 3 source module algebra.algebra.operations
-! leanprover-community/mathlib commit 2bbc7e3884ba234309d2a43b19144105a753292e
+! leanprover-community/mathlib commit 27b54c47c3137250a521aa64e9f1db90be5f6a26
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -555,13 +555,14 @@ theorem map_unop_pow (n : ℕ) (M : Submodule R Aᵐᵒᵖ) :
 
 /-- `span` is a semiring homomorphism (recall multiplication is pointwise multiplication of subsets
 on either side). -/
+@[simps]
 def span.ringHom : SetSemiring A →+* Submodule R A
     where
-  toFun := Submodule.span R
+  toFun s := Submodule.span R s.down
   map_zero' := span_empty
   map_one' := one_eq_span.symm
   map_add' := span_union
-  map_mul' s t := by erw [span_mul_span, ← image_mul_prod]
+  map_mul' s t := by rw [SetSemiring.down_mul, span_mul_span, ← image_mul_prod]
 #align submodule.span.ring_hom Submodule.span.ringHom
 
 section
@@ -627,25 +628,22 @@ variable (R A)
 /-- R-submodules of the R-algebra A are a module over `set A`. -/
 instance moduleSet : Module (SetSemiring A) (Submodule R A)
     where
-  smul s P := span R s * P
+  smul s P := span R s.down * P
   smul_add _ _ _ := mul_add _ _ _
-  add_smul s t P := show span R (s ⊔ t) * P = _ by erw [span_union, right_distrib]
-  mul_smul s t P := show _ = _ * (_ * _) by rw [← mul_assoc, span_mul_span, ← image_mul_prod]
-  one_smul P :=
-    show span R {(1 : A)} * P = _ by
-      conv_lhs => erw [← span_eq P]
-      erw [span_mul_span, one_mul, span_eq]
-  zero_smul P := show span R ∅ * P = ⊥ by erw [span_empty, bot_mul]
+  add_smul s t P := by simp_rw [SMul.smul, SetSemiring.down_add, span_union, sup_mul, add_eq_sup]
+  mul_smul s t P := by simp_rw [SMul.smul, SetSemiring.down_mul, ← mul_assoc, span_mul_span]
+  one_smul P := by simp_rw [SMul.smul, SetSemiring.down_one, ← one_eq_span_one_set, one_mul]
+  zero_smul P := by simp_rw [SMul.smul, SetSemiring.down_zero, span_empty, bot_mul, bot_eq_zero]
   smul_zero _ := mul_bot _
 #align submodule.module_set Submodule.moduleSet
 
 variable {R A}
 
-theorem smul_def {s : SetSemiring A} {P : Submodule R A} : s • P = span R s * P :=
+theorem smul_def (s : SetSemiring A) (P : Submodule R A) : s • P = span R s.down * P :=
   rfl
 #align submodule.smul_def Submodule.smul_def
 
-theorem smul_le_smul {s t : SetSemiring A} {M N : Submodule R A} (h₁ : s.down ≤ t.down)
+theorem smul_le_smul {s t : SetSemiring A} {M N : Submodule R A} (h₁ : s.down ⊆ t.down)
     (h₂ : M ≤ N) : s • M ≤ t • N :=
   mul_le_mul (span_mono h₁) h₂
 #align submodule.smul_le_smul Submodule.smul_le_smul

Mathbin/Algebra/Algebra/Pi.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 
 ! This file was ported from Lean 3 source module algebra.algebra.pi
-! leanprover-community/mathlib commit b16045e4bf61c6fd619a1a68854ab3d605dcd017
+! leanprover-community/mathlib commit 832f7b9162039c28b9361289c8681f155cae758f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.Algebra.Algebra.Equiv
 /-!
 # The R-algebra structure on families of R-algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The R-algebra structure on `Π i : I, A i` when each `A i` is an R-algebra.
 
 ## Main defintions

Mathbin/Algebra/Algebra/Tower.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Anne Baanen
 
 ! This file was ported from Lean 3 source module algebra.algebra.tower
-! leanprover-community/mathlib commit 71150516f28d9826c7341f8815b31f7d8770c212
+! leanprover-community/mathlib commit 832f7b9162039c28b9361289c8681f155cae758f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.LinearAlgebra.Span
 /-!
 # Towers of algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove basic facts about towers of algebra.
 
 An algebra tower A/S/R is expressed by having instances of `algebra A S`,

Mathbin/Algebra/BigOperators/Finsupp.lean

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 
 ! This file was ported from Lean 3 source module algebra.big_operators.finsupp
-! leanprover-community/mathlib commit 13a5329a8625701af92e9a96ffc90fa787fff24d
+! leanprover-community/mathlib commit 842328d9df7e96fd90fc424e115679c15fb23a71
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathbin.Data.Finsupp.Defs
+import Mathbin.Data.Finsupp.Indicator
 import Mathbin.Algebra.BigOperators.Pi
 import Mathbin.Algebra.BigOperators.Ring
 import Mathbin.Algebra.BigOperators.Order
@@ -943,6 +943,26 @@ theorem prod_dvd_prod_of_subset_of_dvd [AddCommMonoid M] [CommMonoid N] {f1 f2 :
     exact h2
 #align finsupp.prod_dvd_prod_of_subset_of_dvd Finsupp.prod_dvd_prod_of_subset_of_dvd
 
+theorem indicator_eq_sum_single [AddCommMonoid M] (s : Finset α) (f : ∀ a ∈ s, M) :
+    indicator s f = ∑ x in s.attach, single x (f x x.2) :=
+  by
+  rw [← sum_single (indicator s f), Sum, sum_subset (support_indicator_subset _ _), ← sum_attach]
+  · refine' Finset.sum_congr rfl fun x hx => _
+    rw [indicator_of_mem]
+  intro i _ hi
+  rw [not_mem_support_iff.mp hi, single_zero]
+#align finsupp.indicator_eq_sum_single Finsupp.indicator_eq_sum_single
+
+@[simp, to_additive]
+theorem prod_indicator_index [Zero M] [CommMonoid N] {s : Finset α} (f : ∀ a ∈ s, M) {h : α → M → N}
+    (h_zero : ∀ a ∈ s, h a 0 = 1) : (indicator s f).Prod h = ∏ x in s.attach, h x (f x x.2) :=
+  by
+  rw [prod_of_support_subset _ (support_indicator_subset _ _) h h_zero, ← prod_attach]
+  refine' Finset.prod_congr rfl fun x hx => _
+  rw [indicator_of_mem]
+#align finsupp.prod_indicator_index Finsupp.prod_indicator_index
+#align finsupp.sum_indicator_index Finsupp.sum_indicator_index
+
 end Finsupp
 
 /- warning: finset.sum_apply' -> Finset.sum_apply' is a dubious translation:

Mathbin/Algebra/DirectLimit.lean

@@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Chris Hughes
 
 ! This file was ported from Lean 3 source module algebra.direct_limit
-! leanprover-community/mathlib commit 4cfc30e317caad46858393f1a7a33f609296cc30
+! leanprover-community/mathlib commit e7f0ddbf65bd7181a85edb74b64bdc35ba4bdc74
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathbin.Data.Finset.Order
 import Mathbin.Algebra.DirectSum.Module
 import Mathbin.RingTheory.FreeCommRing
-import Mathbin.RingTheory.Ideal.Operations
+import Mathbin.RingTheory.Ideal.QuotientOperations
 
 /-!
 # Direct limit of modules, abelian groups, rings, and fields.

Mathbin/Algebra/Module/Pid.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Pierre-Alexandre Bazin
 
 ! This file was ported from Lean 3 source module algebra.module.pid
-! leanprover-community/mathlib commit 6623e6af705e97002a9054c1c05a980180276fc1
+! leanprover-community/mathlib commit f62c15c01a5409b31b97a82d79a12980be4eff35
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -292,7 +292,7 @@ theorem equiv_free_prod_directSum [h' : Module.Finite R N] :
   haveI := isNoetherian_submodule' (torsion R N)
   haveI := Module.Finite.of_surjective _ (torsion R N).mkQ_surjective
   obtain ⟨I, fI, p, hp, e, ⟨h⟩⟩ := equiv_direct_sum_of_is_torsion (@torsion_is_torsion R N _ _ _)
-  obtain ⟨n, ⟨g⟩⟩ := @Module.freeOfFiniteTypeTorsionFree' R _ _ _ (N ⧸ torsion R N) _ _ _ _
+  obtain ⟨n, ⟨g⟩⟩ := @Module.basisOfFiniteTypeTorsionFree' R _ _ _ (N ⧸ torsion R N) _ _ _ _
   haveI : Module.Projective R (N ⧸ torsion R N) := Module.projectiveOfBasis ⟨g⟩
   obtain ⟨f, hf⟩ := Module.projective_lifting_property _ LinearMap.id (torsion R N).mkQ_surjective
   refine'

Mathbin/All.lean

@@ -2486,6 +2486,7 @@ import Mathbin.RingTheory.Ideal.Operations
 import Mathbin.RingTheory.Ideal.Over
 import Mathbin.RingTheory.Ideal.Prod
 import Mathbin.RingTheory.Ideal.Quotient
+import Mathbin.RingTheory.Ideal.QuotientOperations
 import Mathbin.RingTheory.Int.Basic
 import Mathbin.RingTheory.IntegralClosure
 import Mathbin.RingTheory.IntegralDomain
@@ -2845,7 +2846,8 @@ import Mathbin.Topology.Algebra.Order.ProjIcc
 import Mathbin.Topology.Algebra.Order.T5
 import Mathbin.Topology.Algebra.Order.UpperLower
 import Mathbin.Topology.Algebra.Polynomial
-import Mathbin.Topology.Algebra.Ring
+import Mathbin.Topology.Algebra.Ring.Basic
+import Mathbin.Topology.Algebra.Ring.Ideal
 import Mathbin.Topology.Algebra.Semigroup
 import Mathbin.Topology.Algebra.Star
 import Mathbin.Topology.Algebra.StarSubalgebra

Mathbin/Analysis/Complex/UpperHalfPlane/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex Kontorovich, Heather Macbeth, Marc Masdeu
 
 ! This file was ported from Lean 3 source module analysis.complex.upper_half_plane.basic
-! leanprover-community/mathlib commit ae690b0c236e488a0043f6faa8ce3546e7f2f9c5
+! leanprover-community/mathlib commit f06058e64b7e8397234455038f3f8aec83aaba5a
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,7 @@ import Mathbin.LinearAlgebra.Matrix.SpecialLinearGroup
 import Mathbin.Analysis.Complex.Basic
 import Mathbin.GroupTheory.GroupAction.Defs
 import Mathbin.LinearAlgebra.Matrix.GeneralLinearGroup
+import Mathbin.Tactic.LinearCombination
 
 /-!
 # The upper half plane and its automorphisms
@@ -35,13 +36,18 @@ open Classical BigOperators MatrixGroups
 
 attribute [local instance] Fintype.card_fin_even
 
-/- Disable this instances as it is not the simp-normal form, and having them disabled ensures
+/- Disable these instances as they are not the simp-normal form, and having them disabled ensures
 we state lemmas in this file without spurious `coe_fn` terms. -/
 attribute [-instance] Matrix.SpecialLinearGroup.hasCoeToFun
 
+attribute [-instance] Matrix.GeneralLinearGroup.hasCoeToFun
+
 -- mathport name: «expr↑ₘ »
 local prefix:1024 "↑ₘ" => @coe _ (Matrix (Fin 2) (Fin 2) _) _
 
+-- mathport name: «expr↑ₘ[ ]»
+local notation:1024 "↑ₘ[" R "]" => @coe _ (Matrix (Fin 2) (Fin 2) R) _
+
 -- mathport name: «exprGL( , )⁺»
 local notation "GL(" n ", " R ")" "⁺" => Matrix.gLPos (Fin n) R
 
@@ -138,6 +144,10 @@ theorem normSq_ne_zero (z : ℍ) : Complex.normSq (z : ℂ) ≠ 0 :=
   (normSq_pos z).ne'
 #align upper_half_plane.norm_sq_ne_zero UpperHalfPlane.normSq_ne_zero
 
+theorem im_inv_neg_coe_pos (z : ℍ) : 0 < (-z : ℂ)⁻¹.im := by
+  simpa using div_pos z.property (norm_sq_pos z)
+#align upper_half_plane.im_inv_neg_coe_pos UpperHalfPlane.im_inv_neg_coe_pos
+
 /-- Numerator of the formula for a fractional linear transformation -/
 @[simp]
 def num (g : GL(2, ℝ)⁺) (z : ℍ) : ℂ :=
@@ -308,6 +318,15 @@ instance subgroup_to_SL_tower : IsScalarTower Γ SL(2, ℤ) ℍ
 
 end ModularScalarTowers
 
+theorem specialLinearGroup_apply {R : Type _} [CommRing R] [Algebra R ℝ] (g : SL(2, R)) (z : ℍ) :
+    g • z =
+      mk
+        ((((↑(↑ₘ[R] g 0 0) : ℝ) : ℂ) * z + ((↑(↑ₘ[R] g 0 1) : ℝ) : ℂ)) /
+          (((↑(↑ₘ[R] g 1 0) : ℝ) : ℂ) * z + ((↑(↑ₘ[R] g 1 1) : ℝ) : ℂ)))
+        (g • z).property :=
+  rfl
+#align upper_half_plane.special_linear_group_apply UpperHalfPlane.specialLinearGroup_apply
+
 @[simp]
 theorem coe_smul (g : GL(2, ℝ)⁺) (z : ℍ) : ↑(g • z) = num g z / denom g z :=
   rfl
@@ -441,5 +460,59 @@ theorem vadd_im : (x +ᵥ z).im = z.im :=
 
 end RealAddAction
 
+@[simp]
+theorem modular_s_smul (z : ℍ) : ModularGroup.s • z = mk (-z : ℂ)⁻¹ z.im_inv_neg_coe_pos :=
+  by
+  rw [special_linear_group_apply]
+  simp [ModularGroup.s, neg_div, inv_neg]
+#align upper_half_plane.modular_S_smul UpperHalfPlane.modular_s_smul
+
+theorem exists_SL2_smul_eq_of_apply_zero_one_eq_zero (g : SL(2, ℝ)) (hc : ↑ₘ[ℝ] g 1 0 = 0) :
+    ∃ (u : { x : ℝ // 0 < x })(v : ℝ), ((· • ·) g : ℍ → ℍ) = (fun z => v +ᵥ z) ∘ fun z => u • z :=
+  by
+  obtain ⟨a, b, ha, rfl⟩ := g.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero hc
+  refine' ⟨⟨_, mul_self_pos.mpr ha⟩, b * a, _⟩
+  ext1 ⟨z, hz⟩
+  ext1
+  suffices ↑a * z * a + b * a = b * a + a * a * z
+    by
+    rw [special_linear_group_apply]
+    simpa [add_mul]
+  ring
+#align upper_half_plane.exists_SL2_smul_eq_of_apply_zero_one_eq_zero UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_eq_zero
+
+theorem exists_SL2_smul_eq_of_apply_zero_one_ne_zero (g : SL(2, ℝ)) (hc : ↑ₘ[ℝ] g 1 0 ≠ 0) :
+    ∃ (u : { x : ℝ // 0 < x })(v w : ℝ),
+      ((· • ·) g : ℍ → ℍ) =
+        ((· +ᵥ ·) w : ℍ → ℍ) ∘
+          ((· • ·) ModularGroup.s : ℍ → ℍ) ∘ ((· +ᵥ ·) v : ℍ → ℍ) ∘ ((· • ·) u : ℍ → ℍ) :=
+  by
+  have h_denom := denom_ne_zero g
+  induction' g using Matrix.SpecialLinearGroup.fin_two_induction with a b c d h
+  replace hc : c ≠ 0
+  · simpa using hc
+  refine' ⟨⟨_, mul_self_pos.mpr hc⟩, c * d, a / c, _⟩
+  ext1 ⟨z, hz⟩
+  ext1
+  suffices (↑a * z + b) / (↑c * z + d) = a / c - (c * d + ↑c * ↑c * z)⁻¹
+    by
+    rw [special_linear_group_apply]
+    simpa [-neg_add_rev, inv_neg, ← sub_eq_add_neg]
+  replace hc : (c : ℂ) ≠ 0
+  · norm_cast
+    assumption
+  replace h_denom : ↑c * z + d ≠ 0
+  · simpa using h_denom ⟨z, hz⟩
+  have h_aux : (c : ℂ) * d + ↑c * ↑c * z ≠ 0 :=
+    by
+    rw [mul_assoc, ← mul_add, add_comm]
+    exact mul_ne_zero hc h_denom
+  replace h : (a * d - b * c : ℂ) = (1 : ℂ)
+  · norm_cast
+    assumption
+  field_simp
+  linear_combination (-(z * ↑c ^ 2) - ↑c * ↑d) * h
+#align upper_half_plane.exists_SL2_smul_eq_of_apply_zero_one_ne_zero UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_ne_zero
+
 end UpperHalfPlane
 

Mathbin/Analysis/Complex/UpperHalfPlane/Metric.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 
 ! This file was ported from Lean 3 source module analysis.complex.upper_half_plane.metric
-! leanprover-community/mathlib commit 832a8ba8f10f11fea99367c469ff802e69a5b8ec
+! leanprover-community/mathlib commit f06058e64b7e8397234455038f3f8aec83aaba5a
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -30,7 +30,7 @@ ball/sphere with another center and radius.
 
 noncomputable section
 
-open UpperHalfPlane ComplexConjugate NNReal Topology
+open UpperHalfPlane ComplexConjugate NNReal Topology MatrixGroups
 
 open Set Metric Filter Real
 
@@ -397,5 +397,29 @@ theorem isometry_pos_mul (a : { x : ℝ // 0 < x }) : Isometry ((· • ·) a :
   exact mul_div_mul_left _ _ (mt _root_.abs_eq_zero.1 a.2.ne')
 #align upper_half_plane.isometry_pos_mul UpperHalfPlane.isometry_pos_mul
 
+/-- `SL(2, ℝ)` acts on the upper half plane as an isometry.-/
+instance : HasIsometricSmul SL(2, ℝ) ℍ :=
+  ⟨fun g =>
+    by
+    have h₀ : Isometry (fun z => ModularGroup.s • z : ℍ → ℍ) :=
+      Isometry.of_dist_eq fun y₁ y₂ =>
+        by
+        have h₁ : 0 ≤ im y₁ * im y₂ := mul_nonneg y₁.property.le y₂.property.le
+        have h₂ : Complex.abs (y₁ * y₂) ≠ 0 := by simp [y₁.ne_zero, y₂.ne_zero]
+        simp only [dist_eq, modular_S_smul, inv_neg, neg_div, div_mul_div_comm, coe_mk, mk_im,
+          div_one, Complex.inv_im, Complex.neg_im, coe_im, neg_neg, Complex.normSq_neg,
+          mul_eq_mul_left_iff, Real.arsinh_inj, bit0_eq_zero, one_ne_zero, or_false_iff,
+          dist_neg_neg, mul_neg, neg_mul, dist_inv_inv₀ y₁.ne_zero y₂.ne_zero, ← map_mul, ←
+          Complex.normSq_mul, Real.sqrt_div h₁, ← Complex.abs_apply, mul_div (2 : ℝ),
+          div_div_div_comm, div_self h₂, Complex.norm_eq_abs]
+    by_cases hc : g 1 0 = 0
+    · obtain ⟨u, v, h⟩ := exists_SL2_smul_eq_of_apply_zero_one_eq_zero g hc
+      rw [h]
+      exact (isometry_real_vadd v).comp (isometry_pos_mul u)
+    · obtain ⟨u, v, w, h⟩ := exists_SL2_smul_eq_of_apply_zero_one_ne_zero g hc
+      rw [h]
+      exact
+        (isometry_real_vadd w).comp (h₀.comp <| (isometry_real_vadd v).comp <| isometry_pos_mul u)⟩
+
 end UpperHalfPlane