feat(algebra/algebra/subalgebra): inclusion map of subalgebras (#9013)

Co-authored-by: Chris Hughes <chrishughes24@gmail.com>

Author: ChrisHughes24

src/algebra/algebra/subalgebra.lean

@@ -648,6 +648,35 @@ instance : unique (subalgebra R R) :=
   end
   .. algebra.subalgebra.inhabited }
 
+/-- The map `S → T` when `S` is a subalgebra contained in the subalgebra `T`.
+
+This is the subalgebra version of `submodule.of_le`, or `subring.inclusion`  -/
+def inclusion {S T : subalgebra R A} (h : S ≤ T) : S →ₐ[R] T :=
+{ to_fun := set.inclusion h,
+  map_one' := rfl,
+  map_add' := λ _ _, rfl,
+  map_mul' := λ _ _, rfl,
+  map_zero' := rfl,
+  commutes' := λ _, rfl }
+
+lemma inclusion_injective {S T : subalgebra R A} (h : S ≤ T) :
+  function.injective (inclusion h) :=
+λ _ _, subtype.ext ∘ subtype.mk.inj
+
+@[simp] lemma inclusion_self {S : subalgebra R A}:
+  inclusion (le_refl S) = alg_hom.id R S :=
+alg_hom.ext $ λ x, subtype.ext rfl
+
+@[simp] lemma inclusion_right {S T : subalgebra R A} (h : S ≤ T) (x : T)
+  (m : (x : A) ∈ S) : inclusion h ⟨x, m⟩ = x := subtype.ext rfl
+
+@[simp] lemma inclusion_inclusion {S T U : subalgebra R A} (hst : S ≤ T) (htu : T ≤ U)
+  (x : S) : inclusion htu (inclusion hst x) = inclusion (le_trans hst htu) x :=
+subtype.ext rfl
+
+@[simp] lemma coe_inclusion {S T : subalgebra R A} (h : S ≤ T) (s : S) :
+  (inclusion h s : A) = s := rfl
+
 /-- Two subalgebras that are equal are also equivalent as algebras.
 
 This is the `subalgebra` version of `linear_equiv.of_eq` and `equiv.set.of_eq`. -/