feat(ring_theory): coe_submodule S (⊤ : ideal R) = 1 (#8272)

A little `simp` lemma and its dependencies. As I was implementing it, I saw the definition of `has_one (submodule R A)` can be cleaned up a bit.

src/algebra/algebra/operations.lean

@@ -42,19 +42,22 @@ variables (S T : set A) {M N P Q : submodule R A} {m n : A}
 
 /-- `1 : submodule R A` is the submodule R of A. -/
 instance : has_one (submodule R A) :=
-⟨submodule.map (of_id R A).to_linear_map (⊤ : submodule R R)⟩
+⟨(algebra.linear_map R A).range⟩
 
-theorem one_eq_map_top :
-  (1 : submodule R A) = submodule.map (of_id R A).to_linear_map (⊤ : submodule R R) := rfl
+theorem one_eq_range :
+  (1 : submodule R A) = (algebra.linear_map R A).range := rfl
+
+lemma algebra_map_mem (r : R) : algebra_map R A r ∈ (1 : submodule R A) :=
+linear_map.mem_range_self _ _
+
+@[simp] lemma mem_one {x : A} : x ∈ (1 : submodule R A) ↔ ∃ y, algebra_map R A y = x :=
+by simp only [one_eq_range, linear_map.mem_range, algebra.linear_map_apply]
 
 theorem one_eq_span : (1 : submodule R A) = R ∙ 1 :=
 begin
   apply submodule.ext,
   intro a,
-  erw [mem_map, mem_span_singleton],
-  apply exists_congr,
-  intro r,
-  simpa [smul_def],
+  simp only [mem_one, mem_span_singleton, algebra.smul_def, mul_one]
 end
 
 theorem one_le : (1 : submodule R A) ≤ P ↔ (1 : A) ∈ P :=
@@ -220,8 +223,7 @@ on either side). -/
 def span.ring_hom : set_semiring A →+* submodule R A :=
 { to_fun := submodule.span R,
   map_zero' := span_empty,
-  map_one' := le_antisymm (span_le.2 $ singleton_subset_iff.2 ⟨1, ⟨⟩, (algebra_map R A).map_one⟩)
-    (map_le_iff_le_comap.2 $ λ r _, mem_span_singleton.2 ⟨r, (algebra_map_eq_smul_one r).symm⟩),
+  map_one' := one_eq_span.symm,
   map_add' := span_union,
   map_mul' := λ s t, by erw [span_mul_span, ← image_mul_prod] }
 

src/ring_theory/fractional_ideal.lean

@@ -221,7 +221,7 @@ instance : has_one (fractional_ideal S P) :=
 variables (S)
 
 lemma mem_one_iff {x : P} : x ∈ (1 : fractional_ideal S P) ↔ ∃ x' : R, algebra_map R P x' = x :=
-iff.intro (λ ⟨x', _, h⟩, ⟨x', h⟩) (λ ⟨x', h⟩, ⟨x', ⟨x', set.mem_univ _, rfl⟩, h⟩)
+iff.intro (λ ⟨x', _, h⟩, ⟨x', h⟩) (λ ⟨x', h⟩, ⟨x', ⟨x', rfl⟩, h⟩)
 
 lemma coe_mem_one (x : R) : algebra_map R P x ∈ (1 : fractional_ideal S P) :=
 (mem_one_iff S).mpr ⟨x, rfl⟩
@@ -241,10 +241,7 @@ rfl
 
 @[simp, norm_cast] lemma coe_one :
   (↑(1 : fractional_ideal S P) : submodule R P) = 1 :=
-begin
-  simp only [coe_one_eq_coe_submodule_one, ideal.one_eq_top],
-  convert (submodule.one_eq_map_top).symm,
-end
+by rw [coe_one_eq_coe_submodule_one, ideal.one_eq_top, coe_submodule_top]
 
 section lattice
 

src/ring_theory/ideal/operations.lean

@@ -265,7 +265,7 @@ instance : has_mul (ideal R) := ⟨(•)⟩
 @[simp] lemma add_eq_sup : I + J = I ⊔ J := rfl
 @[simp] lemma zero_eq_bot : (0 : ideal R) = ⊥ := rfl
 @[simp] lemma one_eq_top : (1 : ideal R) = ⊤ :=
-by erw [submodule.one_eq_map_top, submodule.map_id]
+by erw [submodule.one_eq_range, linear_map.range_id]
 
 theorem mul_mem_mul {r s} (hr : r ∈ I) (hs : s ∈ J) : r * s ∈ I * J :=
 submodule.smul_mem_smul hr hs

src/ring_theory/integral_closure.lean

@@ -180,8 +180,8 @@ end
 theorem fg_adjoin_of_finite {s : set A} (hfs : s.finite)
   (his : ∀ x ∈ s, is_integral R x) : (algebra.adjoin R s).to_submodule.fg :=
 set.finite.induction_on hfs (λ _, ⟨{1}, submodule.ext $ λ x,
-  by { erw [algebra.adjoin_empty, finset.coe_singleton, ← one_eq_span, one_eq_map_top,
-      map_top, linear_map.mem_range, algebra.mem_bot], refl }⟩)
+  by { erw [algebra.adjoin_empty, finset.coe_singleton, ← one_eq_span, one_eq_range,
+            linear_map.mem_range, algebra.mem_bot], refl }⟩)
 (λ a s has hs ih his, by rw [← set.union_singleton, algebra.adjoin_union_coe_submodule]; exact
   fg_mul _ _ (ih $ λ i hi, his i $ set.mem_insert_of_mem a hi)
     (fg_adjoin_singleton_of_integral _ $ his a $ set.mem_insert a s)) his

src/ring_theory/localization.lean

@@ -1005,6 +1005,9 @@ lemma mem_coe_submodule (I : ideal R) {x : S} :
   x ∈ coe_submodule S I ↔ ∃ y : R, y ∈ I ∧ algebra_map R S y = x :=
 iff.rfl
 
+@[simp] lemma coe_submodule_top : coe_submodule S (⊤ : ideal R) = 1 :=
+by rw [coe_submodule, submodule.map_top, submodule.one_eq_range]
+
 variables {g : R →+* P}
 variables {T : submonoid P} (hy : M ≤ T.comap g) {Q : Type*} [comm_ring Q]
 variables [algebra P Q] [is_localization T Q]