feat(algebra/algebra): the range of `algebra_map (S : subalgebra R A)…

… A` (#9450)




Co-authored-by: Anne Baanen <t.baanen@vu.nl>

src/algebra/algebra/basic.lean

@@ -239,7 +239,9 @@ variables {R A}
 
 namespace id
 
-@[simp] lemma map_eq_self (x : R) : algebra_map R R x = x := rfl
+@[simp] lemma map_eq_id : algebra_map R R = ring_hom.id _ := rfl
+
+lemma map_eq_self (x : R) : algebra_map R R x = x := rfl
 
 @[simp] lemma smul_eq_mul (x y : R) : x • y = x * y := rfl
 

src/algebra/algebra/subalgebra.lean

@@ -292,6 +292,14 @@ by refine_struct { to_fun := (coe : S → A) }; intros; refl
 
 lemma val_apply (x : S) : S.val x = (x : A) := rfl
 
+@[simp] lemma to_subsemiring_subtype : S.to_subsemiring.subtype = (S.val : S →+* A) :=
+rfl
+
+@[simp] lemma to_subring_subtype {R A : Type*} [comm_ring R] [ring A]
+  [algebra R A] (S : subalgebra R A) : S.to_subring.subtype = (S.val : S →+* A) :=
+rfl
+
+
 /-- As submodules, subalgebras are idempotent. -/
 @[simp] theorem mul_self : S.to_submodule * S.to_submodule = S.to_submodule :=
 begin
@@ -868,6 +876,22 @@ instance to_algebra {R A : Type*} [comm_semiring R] [comm_semiring A] [semiring
   [algebra R A] [algebra A α] (S : subalgebra R A) : algebra S α :=
 algebra.of_subsemiring S.to_subsemiring
 
+lemma algebra_map_eq {R A : Type*} [comm_semiring R] [comm_semiring A] [semiring α]
+  [algebra R A] [algebra A α] (S : subalgebra R A) :
+  algebra_map S α = (algebra_map A α).comp S.val := rfl
+
+@[simp] lemma srange_algebra_map {R A : Type*} [comm_semiring R] [comm_semiring A]
+  [algebra R A] (S : subalgebra R A) :
+  (algebra_map S A).srange = S.to_subsemiring :=
+by rw [algebra_map_eq, algebra.id.map_eq_id, ring_hom.id_comp, ← to_subsemiring_subtype,
+       subsemiring.srange_subtype]
+
+@[simp] lemma range_algebra_map {R A : Type*} [comm_ring R] [comm_ring A]
+  [algebra R A] (S : subalgebra R A) :
+  (algebra_map S A).range = S.to_subring :=
+by rw [algebra_map_eq, algebra.id.map_eq_id, ring_hom.id_comp, ← to_subring_subtype,
+       subring.range_subtype]
+
 instance no_zero_smul_divisors_top [no_zero_divisors A] (S : subalgebra R A) :
   no_zero_smul_divisors S A :=
 ⟨λ c x h,