feat: add Algebra.compHom and related lemma

Mathlib/Algebra/Algebra/Defs.lean

@@ -175,6 +175,18 @@ def RingHom.toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S)
   smul_def' _ _ := rfl
   toRingHom := i
 
+/-- definition of smul of toAlgebra'-/
+theorem RingHom.smul_toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S)
+    (h : ∀ c x, i c * x = x * i c) (r: R) (s: S) :
+    let _ := RingHom.toAlgebra' i h
+    r • s = i r * s := rfl
+
+/--definition of algebraMap of toAlgebra'-/
+theorem RingHom.algebraMap_toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S)
+    (h : ∀ c x, i c * x = x * i c) :
+    @algebraMap R S _ _ (i.toAlgebra' h) = i :=
+  rfl
+
 /-- Creating an algebra from a morphism to a commutative semiring. -/
 def RingHom.toAlgebra {R S} [CommSemiring R] [CommSemiring S] (i : R →+* S) : Algebra R S :=
   i.toAlgebra' fun _ => mul_comm _
@@ -311,6 +323,47 @@ section
 
 end
 
+section compHom
+variable {R : Type u} {S : Type v} (A : Type w)
+    [CommSemiring R] [Semiring A] [Algebra R A] [CommSemiring S]
+    (f : S →+* R)
+
+/--
+Compose a Algebra with a RingHom, with action f s • m.
+-/
+abbrev compHom: Algebra S A :=
+  {
+    (algebraMap R A).comp f with
+    smul := fun s x => f s • x
+    commutes' := fun _ _ => Algebra.commutes' _ _,
+    smul_def' := fun s x =>  smul_def (f s) x
+  }
+
+theorem compHom_smul_def (s : S) (x : A):
+    letI := compHom A f
+    s • x = f s • x := by
+      letI := compHom A f
+      rw [Algebra.smul_def]
+      exact Eq.symm (smul_def (f s) x)
+
+theorem compHom_algebraMap_eq :
+    letI := compHom A f
+    algebraMap S A = (algebraMap R A).comp f := rfl
+
+theorem compHom_algebraMap_apply (s : S) :
+    letI := compHom A f
+    algebraMap S A s = (algebraMap R A) (f s) := rfl
+
+theorem compHom_toRingHom_eq :
+    letI := compHom A f
+    (compHom A f).toRingHom = (algebraMap R A).comp f := rfl
+
+theorem compHom_toRingHom_apply (s : S) :
+    letI := compHom A f
+    (compHom A f).toRingHom s = (algebraMap R A) (f s) := rfl
+
+end compHom
+
 variable (R A)
 
 /-- The canonical ring homomorphism `algebraMap R A : R →+* A` for any `R`-algebra `A`,

Mathlib/Algebra/Algebra/Equiv.lean

@@ -812,3 +812,36 @@ def toAlgAut : G →* A ≃ₐ[R] A where
 end
 
 end MulSemiringAction
+
+namespace AlgEquiv
+section CompHom
+/--
+Define an equivalence of algebras in the following commutative diagram:
+A₁ <------> A₂
+/\         /\
+|           |
+|           |
+S --------> R
+-/
+@[simps apply symm_apply toEquiv]
+def ofRingEquiv_compHom
+    {A₁: Type u} {A₂: Type v} {S: Type w} {R: Type u₁}
+    [Semiring A₁] [Semiring A₂]
+    [CommSemiring R] [CommSemiring S]
+    [Algebra R A₂] [Algebra S A₁]
+    (f: S →+* R) {equiv : A₁ ≃+* A₂}
+    (commute: ∀ x, (algebraMap R A₂) (f x) = equiv (algebraMap S A₁ x)) :
+    letI := Algebra.compHom A₂ f
+    A₁ ≃ₐ[S] A₂ :=
+      letI := Algebra.compHom A₂ f
+      {
+        equiv with
+        toFun := equiv,
+        invFun := equiv.symm,
+        commutes' := by
+            simp only [Algebra.compHom_algebraMap_eq, RingHom.coe_comp, Function.comp_apply]
+            exact (fun x => (commute x).symm)
+      }
+
+end CompHom
+end AlgEquiv