refactor(Algebra/Algebra/Pi): cleanup and renaming

mistarro · mistarro · commit 7cbd368ae195 · 2025-01-29T10:52:49.000+01:00
diff --git a/Mathlib/Algebra/Algebra/Pi.lean b/Mathlib/Algebra/Algebra/Pi.lean
@@ -8,7 +8,7 @@ import Mathlib.Algebra.Algebra.Equiv
 /-!
 # The R-algebra structure on families of R-algebras
 
-The R-algebra structure on `∀ i : I, A i` when each `A i` is an R-algebra.
+The R-algebra structure on `Π i : I, A i` when each `A i` is an R-algebra.
 
 ## Main definitions
 
@@ -17,79 +17,66 @@ The R-algebra structure on `∀ i : I, A i` when each `A i` is an R-algebra.
 * `Pi.constAlgHom`
 -/
 
-
-universe u v w
-
 namespace Pi
 
 -- The indexing type
-variable {I : Type u}
+variable (ι : Type*)
 
 -- The scalar type
 variable {R : Type*}
 
 -- The family of types already equipped with instances
-variable {f : I → Type v}
-variable (x y : ∀ i, f i) (i : I)
-variable (I f)
+variable (A : ι → Type*)
+variable [CommSemiring R] [∀ i, Semiring (A i)] [∀ i, Algebra R (A i)]
 
-instance algebra {r : CommSemiring R} [s : ∀ i, Semiring (f i)] [∀ i, Algebra R (f i)] :
-    Algebra R (∀ i : I, f i) where
-  algebraMap := (Pi.ringHom fun i => algebraMap R (f i) : R →+* ∀ i : I, f i)
+instance algebra : Algebra R (Π i, A i) where
+  algebraMap := (Pi.ringHom fun i => algebraMap R (A i) : R →+* Π i, A i)
   commutes' := fun a f => by ext; simp [Algebra.commutes]
   smul_def' := fun a f => by ext; simp [Algebra.smul_def]
 
-theorem algebraMap_def {_ : CommSemiring R} [_s : ∀ i, Semiring (f i)] [∀ i, Algebra R (f i)]
-    (a : R) : algebraMap R (∀ i, f i) a = fun i => algebraMap R (f i) a :=
+theorem algebraMap_def (a : R) : algebraMap R (Π i, A i) a = fun i => algebraMap R (A i) a :=
   rfl
 
 @[simp]
-theorem algebraMap_apply {_ : CommSemiring R} [_s : ∀ i, Semiring (f i)] [∀ i, Algebra R (f i)]
-    (a : R) (i : I) : algebraMap R (∀ i, f i) a i = algebraMap R (f i) a :=
+theorem algebraMap_apply (a : R) (i : ι) : algebraMap R (Π i, A i) a i = algebraMap R (A i) a :=
   rfl
 
-variable {I} in
-instance (g : I → Type*) [∀ i, CommSemiring (f i)] [∀ i, Semiring (g i)]
-    [∀ i, Algebra (f i) (g i)] : Algebra (∀ i, f i) (∀ i, g i) where
-  algebraMap := Pi.ringHom fun _ ↦ (algebraMap _ _).comp (Pi.evalRingHom f _)
-  commutes' _ _ := funext fun _ ↦ Algebra.commutes _ _
-  smul_def' _ _ := funext fun _ ↦ Algebra.smul_def _ _
-
-example [∀ i, CommSemiring (f i)] : Pi.instAlgebraForall f f = Algebra.id _ := rfl
-
--- One could also build a `∀ i, R i`-algebra structure on `∀ i, A i`,
--- when each `A i` is an `R i`-algebra, although I'm not sure that it's useful.
-variable {I} (R)
+variable {ι} (R)
 
-/-- A family of algebra homomorphisms `g i : A →ₐ[R] f i` defines a ring homomorphism
-`Pi.algHom g : A →ₐ[R] Π i, f i` given by `Pi.algHom g x i = f i x`. -/
+/-- A family of algebra homomorphisms `g i : B →ₐ[R] A i` defines a ring homomorphism
+`Pi.algHom g : B →ₐ[R] Π i, A i` given by `Pi.algHom g x i = g i x`. -/
 @[simps!]
-def algHom [CommSemiring R] [s : ∀ i, Semiring (f i)] [∀ i, Algebra R (f i)]
-    {A : Type*} [Semiring A] [Algebra R A] (g : ∀ i, A →ₐ[R] f i) :
-    A →ₐ[R] ∀ i, f i where
+def algHom {B : Type*} [Semiring B] [Algebra R B] (g : ∀ i, B →ₐ[R] A i) :
+    B →ₐ[R] Π i, A i where
   __ := Pi.ringHom fun i ↦ (g i).toRingHom
   commutes' r := by ext; simp
 
 /-- `Function.eval` as an `AlgHom`. The name matches `Pi.evalRingHom`, `Pi.evalMonoidHom`,
 etc. -/
 @[simps]
-def evalAlgHom {_ : CommSemiring R} [∀ i, Semiring (f i)] [∀ i, Algebra R (f i)] (i : I) :
-    (∀ i, f i) →ₐ[R] f i :=
-  { Pi.evalRingHom f i with
+def evalAlgHom (i : ι) : (Π i, A i) →ₐ[R] A i :=
+  { Pi.evalRingHom A i with
     toFun := fun f => f i
     commutes' := fun _ => rfl }
 
 @[simp]
-theorem algHom_evalAlgHom [CommSemiring R] [s : ∀ i, Semiring (f i)] [∀ i, Algebra R (f i)] :
-    algHom R f (evalAlgHom R f) = AlgHom.id R (Π i, f i) := rfl
+theorem algHom_evalAlgHom : algHom R A (evalAlgHom R A) = AlgHom.id R (Π i, A i) := rfl
 
 /-- `Pi.algHom` commutes with composition. -/
-theorem algHom_comp [CommSemiring R] [∀ i, Semiring (f i)] [∀ i, Algebra R (f i)]
-    {A B : Type*} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B]
-    (g : ∀ i, B →ₐ[R] f i) (h : A →ₐ[R] B) :
-    (algHom R f g).comp h = algHom R f (fun i ↦ (g i).comp h) := rfl
+theorem algHom_comp {B C : Type*} [Semiring B] [Algebra R B] [Semiring C] [Algebra R C]
+    (g : ∀ i, C →ₐ[R] A i) (h : B →ₐ[R] C) :
+    (algHom R A g).comp h = algHom R A (fun i ↦ (g i).comp h) := rfl
 
-variable (A B : Type*) [CommSemiring R] [Semiring B] [Algebra R B]
+variable (S : ι → Type*) [∀ i, CommSemiring (S i)]
+
+instance [∀ i, Algebra (S i) (A i)] : Algebra (Π i, S i) (Π i, A i) where
+  algebraMap := Pi.ringHom fun _ ↦ (algebraMap _ _).comp (Pi.evalRingHom S _)
+  commutes' _ _ := funext fun _ ↦ Algebra.commutes _ _
+  smul_def' _ _ := funext fun _ ↦ Algebra.smul_def _ _
+
+example : Pi.instAlgebraForall S S = Algebra.id _ := rfl
+
+variable (A B : Type*) [Semiring B] [Algebra R B]
 
 /-- `Function.const` as an `AlgHom`. The name matches `Pi.constRingHom`, `Pi.constMonoidHom`,
 etc. -/
@@ -113,21 +100,21 @@ end Pi
 
 /-- A special case of `Pi.algebra` for non-dependent types. Lean struggles to elaborate
 definitions elsewhere in the library without this, -/
-instance Function.algebra {R : Type*} (I : Type*) (A : Type*) [CommSemiring R] [Semiring A]
-    [Algebra R A] : Algebra R (I → A) :=
+instance Function.algebra {R : Type*} (ι : Type*) (A : Type*) [CommSemiring R] [Semiring A]
+    [Algebra R A] : Algebra R (ι → A) :=
   Pi.algebra _ _
 
 namespace AlgHom
 
-variable {R : Type u} {A : Type v} {B : Type w} {I : Type*}
+variable {R A B : Type*}
 variable [CommSemiring R] [Semiring A] [Semiring B]
 variable [Algebra R A] [Algebra R B]
 
-/-- `R`-algebra homomorphism between the function spaces `I → A` and `I → B`, induced by an
+/-- `R`-algebra homomorphism between the function spaces `ι → A` and `ι → B`, induced by an
 `R`-algebra homomorphism `f` between `A` and `B`. -/
 @[simps]
-protected def compLeft (f : A →ₐ[R] B) (I : Type*) : (I → A) →ₐ[R] I → B :=
-  { f.toRingHom.compLeft I with
+protected def compLeft (f : A →ₐ[R] B) (ι : Type*) : (ι → A) →ₐ[R] ι → B :=
+  { f.toRingHom.compLeft ι with
     toFun := fun h => f ∘ h
     commutes' := fun c => by
       ext
@@ -137,16 +124,18 @@ end AlgHom
 
 namespace AlgEquiv
 
+variable {R ι : Type*} {A₁ A₂ A₃ : ι → Type*}
+variable [CommSemiring R] [∀ i, Semiring (A₁ i)] [∀ i, Semiring (A₂ i)] [∀ i, Semiring (A₃ i)]
+variable [∀ i, Algebra R (A₁ i)] [∀ i, Algebra R (A₂ i)] [∀ i, Algebra R (A₃ i)]
+
 /-- A family of algebra equivalences `∀ i, (A₁ i ≃ₐ A₂ i)` generates a
-multiplicative equivalence between `∀ i, A₁ i` and `∀ i, A₂ i`.
+multiplicative equivalence between `Π i, A₁ i` and `Π i, A₂ i`.
 
 This is the `AlgEquiv` version of `Equiv.piCongrRight`, and the dependent version of
 `AlgEquiv.arrowCongr`.
 -/
 @[simps apply]
-def piCongrRight {R ι : Type*} {A₁ A₂ : ι → Type*} [CommSemiring R] [∀ i, Semiring (A₁ i)]
-    [∀ i, Semiring (A₂ i)] [∀ i, Algebra R (A₁ i)] [∀ i, Algebra R (A₂ i)]
-    (e : ∀ i, A₁ i ≃ₐ[R] A₂ i) : (∀ i, A₁ i) ≃ₐ[R] ∀ i, A₂ i :=
+def piCongrRight (e : ∀ i, A₁ i ≃ₐ[R] A₂ i) : (Π i, A₁ i) ≃ₐ[R] Π i, A₂ i :=
   { @RingEquiv.piCongrRight ι A₁ A₂ _ _ fun i => (e i).toRingEquiv with
     toFun := fun x j => e j (x j)
     invFun := fun x j => (e j).symm (x j)
@@ -155,22 +144,17 @@ def piCongrRight {R ι : Type*} {A₁ A₂ : ι → Type*} [CommSemiring R] [∀
       simp }
 
 @[simp]
-theorem piCongrRight_refl {R ι : Type*} {A : ι → Type*} [CommSemiring R] [∀ i, Semiring (A i)]
-    [∀ i, Algebra R (A i)] :
-    (piCongrRight fun i => (AlgEquiv.refl : A i ≃ₐ[R] A i)) = AlgEquiv.refl :=
+theorem piCongrRight_refl :
+    (piCongrRight fun i => (AlgEquiv.refl : A₁ i ≃ₐ[R] A₁ i)) = AlgEquiv.refl :=
   rfl
 
 @[simp]
-theorem piCongrRight_symm {R ι : Type*} {A₁ A₂ : ι → Type*} [CommSemiring R]
-    [∀ i, Semiring (A₁ i)] [∀ i, Semiring (A₂ i)] [∀ i, Algebra R (A₁ i)] [∀ i, Algebra R (A₂ i)]
-    (e : ∀ i, A₁ i ≃ₐ[R] A₂ i) : (piCongrRight e).symm = piCongrRight fun i => (e i).symm :=
+theorem piCongrRight_symm (e : ∀ i, A₁ i ≃ₐ[R] A₂ i) :
+    (piCongrRight e).symm = piCongrRight fun i => (e i).symm :=
   rfl
 
 @[simp]
-theorem piCongrRight_trans {R ι : Type*} {A₁ A₂ A₃ : ι → Type*} [CommSemiring R]
-    [∀ i, Semiring (A₁ i)] [∀ i, Semiring (A₂ i)] [∀ i, Semiring (A₃ i)] [∀ i, Algebra R (A₁ i)]
-    [∀ i, Algebra R (A₂ i)] [∀ i, Algebra R (A₃ i)] (e₁ : ∀ i, A₁ i ≃ₐ[R] A₂ i)
-    (e₂ : ∀ i, A₂ i ≃ₐ[R] A₃ i) :
+theorem piCongrRight_trans (e₁ : ∀ i, A₁ i ≃ₐ[R] A₂ i) (e₂ : ∀ i, A₂ i ≃ₐ[R] A₃ i) :
     (piCongrRight e₁).trans (piCongrRight e₂) = piCongrRight fun i => (e₁ i).trans (e₂ i) :=
   rfl
 
