chore: backports for leanprover/lean4#4814 (part 32) (#15577)

Author: Parcly-Taxel

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -509,10 +509,13 @@ lemma span_eq_toSubmodule (s : NonUnitalSubalgebra R A) :
     Submodule.span R (s : Set A) = s.toSubmodule := by
   simp [SetLike.ext'_iff, Submodule.coe_span_eq_self]
 
-variable [IsScalarTower R A A] [SMulCommClass R A A]
-variable [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B]
+variable [NonUnitalNonAssocSemiring B] [Module R B]
 variable [FunLike F A B] [NonUnitalAlgHomClass F R A B]
 
+section IsScalarTower
+
+variable [IsScalarTower R A A] [SMulCommClass R A A]
+
 /-- The minimal non-unital subalgebra that includes `s`. -/
 def adjoin (s : Set A) : NonUnitalSubalgebra R A :=
   { Submodule.span R (NonUnitalSubsemiring.closure s : Set A) with
@@ -657,15 +660,15 @@ theorem adjoin_univ : adjoin R (Set.univ : Set A) = ⊤ :=
   eq_top_iff.2 fun _x hx => subset_adjoin R hx
 
 open NonUnitalSubalgebra in
-lemma _root_.NonUnitalAlgHom.map_adjoin (f : F) (s : Set A) :
-    map f (adjoin R s) = adjoin R (f '' s) :=
+lemma _root_.NonUnitalAlgHom.map_adjoin [IsScalarTower R B B] [SMulCommClass R B B]
+    (f : F) (s : Set A) : map f (adjoin R s) = adjoin R (f '' s) :=
   Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) NonUnitalAlgebra.gi.gc
     NonUnitalAlgebra.gi.gc fun _t => rfl
 
 open NonUnitalSubalgebra in
 @[simp]
-lemma _root_.NonUnitalAlgHom.map_adjoin_singleton (f : F) (x : A) :
-    map f (adjoin R {x}) = adjoin R {f x} := by
+lemma _root_.NonUnitalAlgHom.map_adjoin_singleton [IsScalarTower R B B] [SMulCommClass R B B]
+    (f : F) (x : A) : map f (adjoin R {x}) = adjoin R {f x} := by
   simp [NonUnitalAlgHom.map_adjoin]
 
 variable {R A}
@@ -718,7 +721,8 @@ theorem mul_mem_sup {S T : NonUnitalSubalgebra R A} {x y : A} (hx : x ∈ S) (hy
     x * y ∈ S ⊔ T :=
   mul_mem (mem_sup_left hx) (mem_sup_right hy)
 
-theorem map_sup (f : F) (S T : NonUnitalSubalgebra R A) :
+theorem map_sup [IsScalarTower R B B] [SMulCommClass R B B]
+    (f : F) (S T : NonUnitalSubalgebra R A) :
     ((S ⊔ T).map f : NonUnitalSubalgebra R B) = S.map f ⊔ T.map f :=
   (NonUnitalSubalgebra.gc_map_comap f).l_sup
 
@@ -788,10 +792,6 @@ theorem coe_bot : ((⊥ : NonUnitalSubalgebra R A) : Set A) = {0} := by
 theorem eq_top_iff {S : NonUnitalSubalgebra R A} : S = ⊤ ↔ ∀ x : A, x ∈ S :=
   ⟨fun h x => by rw [h]; exact mem_top, fun h => by ext x; exact ⟨fun _ => mem_top, fun _ => h x⟩⟩
 
-theorem range_top_iff_surjective (f : A →ₙₐ[R] B) :
-    NonUnitalAlgHom.range f = (⊤ : NonUnitalSubalgebra R B) ↔ Function.Surjective f :=
-  NonUnitalAlgebra.eq_top_iff
-
 @[simp]
 theorem range_id : NonUnitalAlgHom.range (NonUnitalAlgHom.id R A) = ⊤ :=
   SetLike.coe_injective Set.range_id
@@ -801,17 +801,25 @@ theorem map_top (f : A →ₙₐ[R] B) : (⊤ : NonUnitalSubalgebra R A).map f =
   SetLike.coe_injective Set.image_univ
 
 @[simp]
-theorem map_bot (f : A →ₙₐ[R] B) : (⊥ : NonUnitalSubalgebra R A).map f = ⊥ :=
+theorem map_bot [IsScalarTower R B B] [SMulCommClass R B B]
+    (f : A →ₙₐ[R] B) : (⊥ : NonUnitalSubalgebra R A).map f = ⊥ :=
   SetLike.coe_injective <| by simp [NonUnitalAlgebra.coe_bot, NonUnitalSubalgebra.coe_map]
 
 @[simp]
-theorem comap_top (f : A →ₙₐ[R] B) : (⊤ : NonUnitalSubalgebra R B).comap f = ⊤ :=
+theorem comap_top [IsScalarTower R B B] [SMulCommClass R B B]
+    (f : A →ₙₐ[R] B) : (⊤ : NonUnitalSubalgebra R B).comap f = ⊤ :=
   eq_top_iff.2 fun _ => mem_top
 
 /-- `NonUnitalAlgHom` to `⊤ : NonUnitalSubalgebra R A`. -/
 def toTop : A →ₙₐ[R] (⊤ : NonUnitalSubalgebra R A) :=
   NonUnitalAlgHom.codRestrict (NonUnitalAlgHom.id R A) ⊤ fun _ => mem_top
 
+end IsScalarTower
+
+theorem range_top_iff_surjective [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) :
+    NonUnitalAlgHom.range f = (⊤ : NonUnitalSubalgebra R B) ↔ Function.Surjective f :=
+  NonUnitalAlgebra.eq_top_iff
+
 end NonUnitalAlgebra
 
 namespace NonUnitalSubalgebra
@@ -831,9 +839,48 @@ theorem range_val : NonUnitalAlgHom.range (NonUnitalSubalgebraClass.subtype S) =
 instance subsingleton_of_subsingleton [Subsingleton A] : Subsingleton (NonUnitalSubalgebra R A) :=
   ⟨fun B C => ext fun x => by simp only [Subsingleton.elim x 0, zero_mem B, zero_mem C]⟩
 
-variable [IsScalarTower R A A] [SMulCommClass R A A]
 variable [NonUnitalNonAssocSemiring B] [Module R B]
 
+section Prod
+
+variable (S₁ : NonUnitalSubalgebra R B)
+
+/-- The product of two non-unital subalgebras is a non-unital subalgebra. -/
+def prod : NonUnitalSubalgebra R (A × B) :=
+  { S.toNonUnitalSubsemiring.prod S₁.toNonUnitalSubsemiring with
+    carrier := S ×ˢ S₁
+    smul_mem' := fun r _x hx => ⟨SMulMemClass.smul_mem r hx.1, SMulMemClass.smul_mem r hx.2⟩ }
+
+@[simp]
+theorem coe_prod : (prod S S₁ : Set (A × B)) = (S : Set A) ×ˢ S₁ :=
+  rfl
+
+theorem prod_toSubmodule : (S.prod S₁).toSubmodule = S.toSubmodule.prod S₁.toSubmodule :=
+  rfl
+
+@[simp]
+theorem mem_prod {S : NonUnitalSubalgebra R A} {S₁ : NonUnitalSubalgebra R B} {x : A × B} :
+    x ∈ prod S S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁ :=
+  Set.mem_prod
+
+variable [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B]
+
+@[simp]
+theorem prod_top : (prod ⊤ ⊤ : NonUnitalSubalgebra R (A × B)) = ⊤ := by ext; simp
+
+theorem prod_mono {S T : NonUnitalSubalgebra R A} {S₁ T₁ : NonUnitalSubalgebra R B} :
+    S ≤ T → S₁ ≤ T₁ → prod S S₁ ≤ prod T T₁ :=
+  Set.prod_mono
+
+@[simp]
+theorem prod_inf_prod {S T : NonUnitalSubalgebra R A} {S₁ T₁ : NonUnitalSubalgebra R B} :
+    S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁) :=
+  SetLike.coe_injective Set.prod_inter_prod
+
+end Prod
+
+variable [IsScalarTower R A A] [SMulCommClass R A A]
+
 instance _root_.NonUnitalAlgHom.subsingleton [Subsingleton (NonUnitalSubalgebra R A)] :
     Subsingleton (A →ₙₐ[R] B) :=
   ⟨fun f g =>
@@ -880,44 +927,6 @@ theorem coe_inclusion {S T : NonUnitalSubalgebra R A} (h : S ≤ T) (s : S) :
     (inclusion h s : A) = s :=
   rfl
 
-section Prod
-
-variable (S₁ : NonUnitalSubalgebra R B)
-
-/-- The product of two non-unital subalgebras is a non-unital subalgebra. -/
-def prod : NonUnitalSubalgebra R (A × B) :=
-  { S.toNonUnitalSubsemiring.prod S₁.toNonUnitalSubsemiring with
-    carrier := S ×ˢ S₁
-    smul_mem' := fun r _x hx => ⟨SMulMemClass.smul_mem r hx.1, SMulMemClass.smul_mem r hx.2⟩ }
-
-@[simp]
-theorem coe_prod : (prod S S₁ : Set (A × B)) = (S : Set A) ×ˢ S₁ :=
-  rfl
-
-theorem prod_toSubmodule : (S.prod S₁).toSubmodule = S.toSubmodule.prod S₁.toSubmodule :=
-  rfl
-
-@[simp]
-theorem mem_prod {S : NonUnitalSubalgebra R A} {S₁ : NonUnitalSubalgebra R B} {x : A × B} :
-    x ∈ prod S S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁ :=
-  Set.mem_prod
-
-variable [IsScalarTower R B B] [SMulCommClass R B B]
-
-@[simp]
-theorem prod_top : (prod ⊤ ⊤ : NonUnitalSubalgebra R (A × B)) = ⊤ := by ext; simp
-
-theorem prod_mono {S T : NonUnitalSubalgebra R A} {S₁ T₁ : NonUnitalSubalgebra R B} :
-    S ≤ T → S₁ ≤ T₁ → prod S S₁ ≤ prod T T₁ :=
-  Set.prod_mono
-
-@[simp]
-theorem prod_inf_prod {S T : NonUnitalSubalgebra R A} {S₁ T₁ : NonUnitalSubalgebra R B} :
-    S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁) :=
-  SetLike.coe_injective Set.prod_inter_prod
-
-end Prod
-
 section SuprLift
 
 variable {ι : Type*}

Mathlib/Algebra/DirectLimit.lean

@@ -79,10 +79,9 @@ nonrec theorem DirectedSystem.map_map [DirectedSystem G fun i j h => f i j h] {i
   DirectedSystem.map_map (fun i j h => f i j h) hij hjk x
 
 variable (G)
-variable [DecidableEq ι]
 
 /-- The direct limit of a directed system is the modules glued together along the maps. -/
-def DirectLimit : Type max v w :=
+def DirectLimit [DecidableEq ι] : Type max v w :=
   DirectSum ι G ⧸
     (span R <|
       { a |
@@ -91,6 +90,10 @@ def DirectLimit : Type max v w :=
 
 namespace DirectLimit
 
+section Basic
+
+variable [DecidableEq ι]
+
 instance addCommGroup : AddCommGroup (DirectLimit G f) :=
   Quotient.addCommGroup _
 
@@ -247,10 +250,9 @@ lemma congr_symm_apply_of [IsDirected ι (· ≤ ·)]
 
 end functorial
 
-section Totalize
-
+end Basic
 
-variable (G f)
+section Totalize
 
 open Classical in
 /-- `totalize G f i j` is a linear map from `G i` to `G j`, for *every* `i` and `j`.
@@ -269,7 +271,8 @@ theorem totalize_of_not_le {i j} (h : ¬i ≤ j) : totalize G f i j = 0 :=
 
 end Totalize
 
-variable [DirectedSystem G fun i j h => f i j h]
+variable [DecidableEq ι] [DirectedSystem G fun i j h => f i j h]
+variable {G f}
 
 theorem toModule_totalize_of_le [∀ i (k : G i), Decidable (k ≠ 0)] {x : DirectSum ι G} {i j : ι}
     (hij : i ≤ j) (hx : ∀ k ∈ x.support, k ≤ i) :
@@ -343,10 +346,10 @@ end Module
 
 namespace AddCommGroup
 
-variable [DecidableEq ι] [∀ i, AddCommGroup (G i)]
+variable [∀ i, AddCommGroup (G i)]
 
 /-- The direct limit of a directed system is the abelian groups glued together along the maps. -/
-def DirectLimit (f : ∀ i j, i ≤ j → G i →+ G j) : Type _ :=
+def DirectLimit [DecidableEq ι] (f : ∀ i j, i ≤ j → G i →+ G j) : Type _ :=
   @Module.DirectLimit ℤ _ ι _ G _ _ (fun i j hij => (f i j hij).toIntLinearMap) _
 
 namespace DirectLimit
@@ -359,6 +362,8 @@ protected theorem directedSystem [h : DirectedSystem G fun i j h => f i j h] :
 
 attribute [local instance] DirectLimit.directedSystem
 
+variable [DecidableEq ι]
+
 instance : AddCommGroup (DirectLimit G f) :=
   Module.DirectLimit.addCommGroup G fun i j hij => (f i j hij).toIntLinearMap
 
@@ -842,7 +847,7 @@ variable {G' : ι → Type v'} [∀ i, CommRing (G' i)]
 variable {f' : ∀ i j, i ≤ j → G' i →+* G' j}
 variable {G'' : ι → Type v''} [∀ i, CommRing (G'' i)]
 variable {f'' : ∀ i j, i ≤ j → G'' i →+* G'' j}
-variable [Nonempty ι]
+
 /--
 Consider direct limits `lim G` and `lim G'` with direct system `f` and `f'` respectively, any
 family of ring homomorphisms `gᵢ : Gᵢ ⟶ G'ᵢ` such that `g ∘ f = f' ∘ g` induces a ring
@@ -862,6 +867,8 @@ def map (g : (i : ι) → G i →+* G' i)
     map g hg (of G _ _ x) = of G' (fun _ _ h ↦ f' _ _ h) i (g i x) :=
   lift_of _ _ _ _ _
 
+variable [Nonempty ι]
+
 @[simp] lemma map_id [IsDirected ι (· ≤ ·)] :
     map (fun i ↦ RingHom.id _) (fun _ _ _ ↦ rfl) =
     RingHom.id (DirectLimit G fun _ _ h ↦ f _ _ h) :=

Mathlib/Algebra/DirectSum/Module.lean

@@ -54,6 +54,9 @@ theorem smul_apply (b : R) (v : ⨁ i, M i) (i : ι) : (b • v) i = b • v i :
   DFinsupp.smul_apply _ _ _
 
 variable (R ι M)
+
+section DecidableEq
+
 variable [DecidableEq ι]
 
 /-- Create the direct sum given a family `M` of `R` modules indexed over `ι`. -/
@@ -158,6 +161,8 @@ theorem linearEquivFunOnFintype_symm_single [Fintype ι] (i : ι) (m : M i) :
   rw [DFinsupp.equivFunOnFintype_symm_single i m]
   rfl
 
+end DecidableEq
+
 @[simp]
 theorem linearEquivFunOnFintype_symm_coe [Fintype ι] (f : ⨁ i, M i) :
     (linearEquivFunOnFintype R ι M).symm f = f := by
@@ -168,8 +173,6 @@ protected def lid (M : Type v) (ι : Type* := PUnit) [AddCommMonoid M] [Module R
     (⨁ _ : ι, M) ≃ₗ[R] M :=
   { DirectSum.id M ι, toModule R ι M fun _ ↦ LinearMap.id with }
 
-variable (ι M)
-
 /-- The projection map onto one component, as a linear map. -/
 def component (i : ι) : (⨁ i, M i) →ₗ[R] M i :=
   DFinsupp.lapply i
@@ -187,14 +190,15 @@ theorem ext_iff {f g : ⨁ i, M i} : f = g ↔ ∀ i, component R ι M i f = com
   ⟨fun h _ ↦ by rw [h], ext R⟩
 
 @[simp]
-theorem lof_apply (i : ι) (b : M i) : ((lof R ι M i) b) i = b :=
+theorem lof_apply [DecidableEq ι] (i : ι) (b : M i) : ((lof R ι M i) b) i = b :=
   DFinsupp.single_eq_same
 
 @[simp]
-theorem component.lof_self (i : ι) (b : M i) : component R ι M i ((lof R ι M i) b) = b :=
+theorem component.lof_self [DecidableEq ι] (i : ι) (b : M i) :
+    component R ι M i ((lof R ι M i) b) = b :=
   lof_apply R i b
 
-theorem component.of (i j : ι) (b : M j) :
+theorem component.of [DecidableEq ι] (i j : ι) (b : M j) :
     component R ι M i ((lof R ι M j) b) = if h : j = i then Eq.recOn h b else 0 :=
   DFinsupp.single_apply
 
@@ -216,7 +220,7 @@ end CongrLeft
 section Sigma
 
 variable {α : ι → Type*} {δ : ∀ i, α i → Type w}
-variable [∀ i j, AddCommMonoid (δ i j)] [∀ i j, Module R (δ i j)]
+variable [DecidableEq ι] [∀ i j, AddCommMonoid (δ i j)] [∀ i j, Module R (δ i j)]
 
 /-- `curry` as a linear map. -/
 def sigmaLcurry : (⨁ i : Σi, _, δ i.1 i.2) →ₗ[R] ⨁ (i) (j), δ i j :=

Mathlib/Algebra/Lie/Abelian.lean

@@ -271,8 +271,7 @@ open LieSubmodule LieSubalgebra
 
 variable {R : Type u} {L : Type v} {M : Type w}
 variable [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M]
-variable [LieRingModule L M] [LieModule R L M]
-variable (N N' : LieSubmodule R L M) (I J : LieIdeal R L)
+variable [LieRingModule L M] (N N' : LieSubmodule R L M) (I J : LieIdeal R L)
 
 @[simp]
 theorem LieSubmodule.trivial_lie_oper_zero [LieModule.IsTrivial L M] : ⁅I, N⁆ = ⊥ := by