Merge remote-tracking branch 'origin/master' into adomani/use_cdots

Mathlib.lean

@@ -362,6 +362,7 @@ import Mathlib.Algebra.Module.Bimodule
 import Mathlib.Algebra.Module.CharacterModule
 import Mathlib.Algebra.Module.DedekindDomain
 import Mathlib.Algebra.Module.Equiv
+import Mathlib.Algebra.Module.FinitePresentation
 import Mathlib.Algebra.Module.GradedModule
 import Mathlib.Algebra.Module.Hom
 import Mathlib.Algebra.Module.Injective
@@ -1130,6 +1131,7 @@ import Mathlib.CategoryTheory.Adjunction.Mates
 import Mathlib.CategoryTheory.Adjunction.Opposites
 import Mathlib.CategoryTheory.Adjunction.Over
 import Mathlib.CategoryTheory.Adjunction.Reflective
+import Mathlib.CategoryTheory.Adjunction.Restrict
 import Mathlib.CategoryTheory.Adjunction.Whiskering
 import Mathlib.CategoryTheory.Balanced
 import Mathlib.CategoryTheory.Bicategory.Adjunction

Mathlib/Algebra/BigOperators/Associated.lean

@@ -91,15 +91,15 @@ theorem Multiset.prod_primes_dvd [CancelCommMonoidWithZero α]
     apply mul_dvd_mul_left a
     refine induct _ (fun a ha => h a (Multiset.mem_cons_of_mem ha)) (fun b b_in_s => ?_)
       fun a => (Multiset.countP_le_of_le _ (Multiset.le_cons_self _ _)).trans (uniq a)
-    · have b_div_n := div b (Multiset.mem_cons_of_mem b_in_s)
-      have a_prime := h a (Multiset.mem_cons_self a s)
-      have b_prime := h b (Multiset.mem_cons_of_mem b_in_s)
-      refine' (b_prime.dvd_or_dvd b_div_n).resolve_left fun b_div_a => _
-      have assoc := b_prime.associated_of_dvd a_prime b_div_a
-      have := uniq a
-      rw [Multiset.countP_cons_of_pos _ (Associated.refl _), Nat.succ_le_succ_iff, ← not_lt,
-        Multiset.countP_pos] at this
-      exact this ⟨b, b_in_s, assoc.symm⟩
+    have b_div_n := div b (Multiset.mem_cons_of_mem b_in_s)
+    have a_prime := h a (Multiset.mem_cons_self a s)
+    have b_prime := h b (Multiset.mem_cons_of_mem b_in_s)
+    refine' (b_prime.dvd_or_dvd b_div_n).resolve_left fun b_div_a => _
+    have assoc := b_prime.associated_of_dvd a_prime b_div_a
+    have := uniq a
+    rw [Multiset.countP_cons_of_pos _ (Associated.refl _), Nat.succ_le_succ_iff, ← not_lt,
+      Multiset.countP_pos] at this
+    exact this ⟨b, b_in_s, assoc.symm⟩
 #align multiset.prod_primes_dvd Multiset.prod_primes_dvd
 
 theorem Finset.prod_primes_dvd [CancelCommMonoidWithZero α] [Unique αˣ] {s : Finset α} (n : α)

Mathlib/Algebra/BigOperators/Basic.lean

@@ -2075,8 +2075,8 @@ theorem mem_sum {f : α → Multiset β} (s : Finset α) (b : β) :
     (b ∈ ∑ x in s, f x) ↔ ∃ a ∈ s, b ∈ f a := by
   classical
     refine' s.induction_on (by simp) _
-    · intro a t hi ih
-      simp [sum_insert hi, ih, or_and_right, exists_or]
+    intro a t hi ih
+    simp [sum_insert hi, ih, or_and_right, exists_or]
 #align finset.mem_sum Finset.mem_sum
 
 section ProdEqZero

Mathlib/Algebra/BigOperators/Intervals.lean

@@ -295,7 +295,7 @@ lemma prod_range_diag_flip (n : ℕ) (f : ℕ → ℕ → M) :
       Nat.lt_succ_iff, le_add_iff_nonneg_right, Nat.zero_le, and_true, and_imp, imp_self,
       implies_true, Sigma.forall, forall_const, add_tsub_cancel_of_le, Sigma.mk.inj_iff,
       add_tsub_cancel_left, heq_eq_eq]
-  · exact fun a b han hba ↦ lt_of_le_of_lt hba han
+  exact fun a b han hba ↦ lt_of_le_of_lt hba han
 #align sum_range_diag_flip Finset.sum_range_diag_flip
 
 end Generic

Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

@@ -138,7 +138,7 @@ private theorem pentagon_aux (W X Y Z : Type*) [AddCommMonoid W] [AddCommMonoid
     [AddCommMonoid Y] [AddCommMonoid Z] [Module R W] [Module R X] [Module R Y] [Module R Z] :
     (((assoc R X Y Z).toLinearMap.lTensor W).comp
             (assoc R W (X ⊗[R] Y) Z).toLinearMap).comp
-        ((assoc R W X Y).rTensor Z) =
+        ((assoc R W X Y).toLinearMap.rTensor Z) =
       (assoc R W X (Y ⊗[R] Z)).toLinearMap.comp (assoc R (W ⊗[R] X) Y Z).toLinearMap := by
   apply TensorProduct.ext_fourfold
   intro w x y z

Mathlib/Algebra/CharP/Basic.lean

@@ -466,8 +466,9 @@ section NonAssocSemiring
 
 variable {R} [NonAssocSemiring R]
 
--- see Note [lower instance priority]
-instance (priority := 100) CharOne.subsingleton [CharP R 1] : Subsingleton R :=
+-- This lemma is not an instance, to make sure that trying to prove `α` is a subsingleton does
+-- not try to find a ring structure on `α`, which can be expensive.
+lemma CharOne.subsingleton [CharP R 1] : Subsingleton R :=
   Subsingleton.intro <|
     suffices ∀ r : R, r = 0 from fun a b => show a = b by rw [this a, this b]
     fun r =>
@@ -477,8 +478,9 @@ instance (priority := 100) CharOne.subsingleton [CharP R 1] : Subsingleton R :=
       _ = 0 * r := by rw [CharP.cast_eq_zero]
       _ = 0 := by rw [zero_mul]
 
-theorem false_of_nontrivial_of_char_one [Nontrivial R] [CharP R 1] : False :=
-  false_of_nontrivial_of_subsingleton R
+theorem false_of_nontrivial_of_char_one [Nontrivial R] [CharP R 1] : False := by
+  have : Subsingleton R := CharOne.subsingleton
+  exact false_of_nontrivial_of_subsingleton R
 #align char_p.false_of_nontrivial_of_char_one CharP.false_of_nontrivial_of_char_one
 
 theorem ringChar_ne_one [Nontrivial R] : ringChar R ≠ 1 := by

Mathlib/Algebra/Lie/Derivation/AdjointAction.lean

@@ -53,6 +53,10 @@ variable {R L}
 /-- The definitions `LieDerivation.ad` and `LieAlgebra.ad` agree. -/
 @[simp] lemma coe_ad_apply_eq_ad_apply (x : L) : ad R L x = LieAlgebra.ad R L x := by ext; simp
 
+lemma ad_apply_lieDerivation (x : L) (D : LieDerivation R L L) : ad R L (D x) = - ⁅x, D⁆ := rfl
+
+lemma lie_ad (x : L) (D : LieDerivation R L L) : ⁅ad R L x, D⁆ = ⁅x, D⁆ := by ext; simp
+
 variable (R L) in
 /-- The kernel of the adjoint action on a Lie algebra is equal to its center. -/
 lemma ad_ker_eq_center : (ad R L).ker = LieAlgebra.center R L := by
@@ -67,9 +71,7 @@ lemma injective_ad_of_center_eq_bot (h : LieAlgebra.center R L = ⊥) :
 
 /-- The commutator of a derivation `D` and a derivation of the form `ad x` is `ad (D x)`. -/
 lemma lie_der_ad_eq_ad_der (D : LieDerivation R L L) (x : L) : ⁅D, ad R L x⁆ = ad R L (D x) := by
-  ext a
-  rw [commutator_apply, ad_apply_apply, ad_apply_apply, ad_apply_apply, apply_lie_eq_add,
-    add_sub_cancel_left]
+  rw [ad_apply_lieDerivation, ← lie_ad, lie_skew]
 
 variable (R L) in
 /-- The range of the adjoint action homomorphism from a Lie algebra `L` to the Lie algebra of its
@@ -84,6 +86,15 @@ lemma mem_ad_idealRange_iff {D : LieDerivation R L L} :
     D ∈ (ad R L).idealRange ↔ ∃ x : L, ad R L x = D :=
   (ad R L).mem_idealRange_iff (ad_isIdealMorphism R L)
 
+lemma maxTrivSubmodule_eq_bot_of_center_eq_bot (h : LieAlgebra.center R L = ⊥) :
+    LieModule.maxTrivSubmodule R L (LieDerivation R L L) = ⊥ := by
+  refine (LieSubmodule.eq_bot_iff _).mpr fun D hD ↦ ext fun x ↦ ?_
+  have : ad R L (D x) = 0 := by
+    rw [LieModule.mem_maxTrivSubmodule] at hD
+    simp [ad_apply_lieDerivation, hD]
+  rw [← LieHom.mem_ker, ad_ker_eq_center, h, LieSubmodule.mem_bot] at this
+  simp [this]
+
 end AdjointAction
 
 end LieDerivation

Mathlib/Algebra/Lie/Derivation/Basic.lean

@@ -291,6 +291,10 @@ instance : LieRing (LieDerivation R L L) where
 instance instLieAlgebra : LieAlgebra R (LieDerivation R L L) where
   lie_smul := fun r d e => by ext a; simp only [commutator_apply, map_smul, smul_sub, smul_apply]
 
+@[simp] lemma lie_apply (D₁ D₂ : LieDerivation R L L) (x : L) :
+    ⁅D₁, D₂⁆ x = D₁ (D₂ x) - D₂ (D₁ x) :=
+  rfl
+
 end
 
 section
@@ -328,6 +332,29 @@ def inner : M →ₗ[R] LieDerivation R L M where
   map_add' m n := by ext; simp
   map_smul' t m := by ext; simp
 
+instance instLieRingModule : LieRingModule L (LieDerivation R L M) where
+  bracket x D := inner R L M (D x)
+  add_lie x y D := by simp
+  lie_add x D₁ D₂ := by simp
+  leibniz_lie x y D := by simp
+
+@[simp] lemma lie_lieDerivation_apply (x y : L) (D : LieDerivation R L M) :
+    ⁅x, D⁆ y = ⁅y, D x⁆ :=
+  rfl
+
+@[simp] lemma lie_coe_lieDerivation_apply (x : L) (D : LieDerivation R L M) :
+    ⁅x, (D : L →ₗ[R] M)⁆ = ⁅x, D⁆ := by
+  ext; simp
+
+instance instLieModule : LieModule R L (LieDerivation R L M) where
+  smul_lie t x D := by ext; simp
+  lie_smul t x D := by ext; simp
+
+protected lemma leibniz_lie (x : L) (D₁ D₂ : LieDerivation R L L) :
+    ⁅x, ⁅D₁, D₂⁆⁆ = ⁅⁅x, D₁⁆, D₂⁆ + ⁅D₁, ⁅x, D₂⁆⁆ := by
+  ext y
+  simp [-lie_skew, ← lie_skew (D₁ x) (D₂ y), ← lie_skew (D₂ x) (D₁ y), sub_eq_neg_add]
+
 end Inner
 
 end LieDerivation

Mathlib/Algebra/Lie/Derivation/Killing.lean

@@ -42,17 +42,26 @@ lemma killingForm_restrict_range_ad : (killingForm R 𝔻).restrict 𝕀 = killi
   rw [← (ad_isIdealMorphism R L).eq, ← LieIdeal.killingForm_eq]
   rfl
 
+/-- The orthogonal complement of the inner derivations is a Lie submodule of all derivations. -/
+@[simps!] noncomputable def rangeAdOrthogonal : LieSubmodule R L (LieDerivation R L L) where
+  __ := 𝕀ᗮ
+  lie_mem := by
+    intro x D hD
+    have : 𝕀ᗮ = (ad R L).idealRange.killingCompl := by simp [← (ad_isIdealMorphism R L).eq]
+    change D ∈ 𝕀ᗮ at hD
+    change ⁅x, D⁆ ∈ 𝕀ᗮ
+    rw [this] at hD ⊢
+    rw [← lie_ad]
+    exact lie_mem_right _ _ (ad R L).idealRange.killingCompl _ _ hD
+
 variable {R L}
 
 /-- If a derivation `D` is in the Killing orthogonal of the range of the adjoint action, then, for
 any `x : L`, `ad (D x)` is also in this orthogonal. -/
 lemma ad_mem_orthogonal_of_mem_orthogonal {D : LieDerivation R L L} (hD : D ∈ 𝕀ᗮ) (x : L) :
     ad R L (D x) ∈ 𝕀ᗮ := by
-  have : 𝕀ᗮ = (ad R L).idealRange.killingCompl := by
-    simp [← (ad_isIdealMorphism R L).eq]
-  rw [this] at hD ⊢
-  rw [← lie_der_ad_eq_ad_der]
-  exact lie_mem_left _ _ (ad R L).idealRange.killingCompl _ _ hD
+  simp only [ad_apply_lieDerivation, LieHom.range_coeSubmodule, neg_mem_iff]
+  exact (rangeAdOrthogonal R L).lie_mem hD
 
 lemma ad_mem_ker_killingForm_ad_range_of_mem_orthogonal
     {D : LieDerivation R L L} (hD : D ∈ 𝕀ᗮ) (x : L) :