feat(fractional_ideal): coe : ideal → fractional_ideal as ring hom (#…

…8511)

This PR bundles the coercion from integral ideals to fractional ideals as a ring hom, and proves the missing `simp` lemmas that show the map indeed preserves the ring structure.



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/ring_theory/fractional_ideal.lean

@@ -165,6 +165,8 @@ end
 This is a bundled version of `is_localization.coe_submodule : ideal R → submodule R P`,
 which is not to be confused with the `coe : fractional_ideal S P → submodule R P`,
 also called `coe_to_submodule` in theorem names.
+
+This map is available as a ring hom, called `fractional_ideal.coe_ideal_hom`.
 -/
 instance coe_to_fractional_ideal : has_coe (ideal R) (fractional_ideal S P) :=
 ⟨λ I, ⟨coe_submodule P I, is_fractional_of_le_one _
@@ -365,6 +367,10 @@ lemma sup_eq_add (I J : fractional_ideal S P) : I ⊔ J = I + J := rfl
 @[simp, norm_cast]
 lemma coe_add (I J : fractional_ideal S P) : (↑(I + J) : submodule R P) = I + J := rfl
 
+@[simp, norm_cast]
+lemma coe_ideal_sup (I J : ideal R) : ↑(I ⊔ J) = (I + J : fractional_ideal S P) :=
+coe_to_submodule_injective $ coe_submodule_sup _ _ _
+
 lemma fractional_mul (I J : fractional_ideal S P) : is_fractional S (I * J : submodule R P) :=
 begin
   rcases I with ⟨I, aI, haI, hI⟩,
@@ -409,6 +415,10 @@ instance : has_mul (fractional_ideal S P) := ⟨λ I J, mul I J⟩
 @[simp, norm_cast]
 lemma coe_mul (I J : fractional_ideal S P) : (↑(I * J) : submodule R P) = I * J := rfl
 
+@[simp, norm_cast]
+lemma coe_ideal_mul (I J : ideal R) : (↑(I * J) : fractional_ideal S P) = I * J :=
+coe_to_submodule_injective $ coe_submodule_mul _ _ _
+
 lemma mul_left_mono (I : fractional_ideal S P) : monotone ((*) I) :=
 λ J J' h, mul_le.mpr (λ x hx y hy, mul_mem_mul hx (h hy))
 
@@ -529,6 +539,17 @@ begin
     apply coe_ideal_le_one },
 end
 
+variables (S P)
+
+/-- `coe_ideal_hom (S : submonoid R) P` is `coe : ideal R → fractional_ideal S P` as a ring hom -/
+@[simps]
+def coe_ideal_hom : ideal R →+* fractional_ideal S P :=
+{ to_fun := coe,
+  map_add' := coe_ideal_sup,
+  map_mul' := coe_ideal_mul,
+  map_one' := by rw [ideal.one_eq_top, coe_ideal_top],
+  map_zero' := coe_to_fractional_ideal_bot }
+
 end order
 
 variables {P' : Type*} [comm_ring P'] [algebra R P'] [loc' : is_localization S P']

src/ring_theory/localization.lean

@@ -1009,9 +1009,20 @@ lemma coe_submodule_mono {I J : ideal R} (h : I ≤ J) :
   coe_submodule S I ≤ coe_submodule S J :=
 submodule.map_mono h
 
+@[simp] lemma coe_submodule_bot : coe_submodule S (⊥ : ideal R) = ⊥ :=
+by rw [coe_submodule, submodule.map_bot]
+
 @[simp] lemma coe_submodule_top : coe_submodule S (⊤ : ideal R) = 1 :=
 by rw [coe_submodule, submodule.map_top, submodule.one_eq_range]
 
+@[simp] lemma coe_submodule_sup (I J : ideal R) :
+  coe_submodule S (I ⊔ J) = coe_submodule S I ⊔ coe_submodule S J :=
+submodule.map_sup _ _ _
+
+@[simp] lemma coe_submodule_mul (I J : ideal R) :
+  coe_submodule S (I * J) = coe_submodule S I * coe_submodule S J :=
+submodule.map_mul _ _ (algebra.of_id R S)
+
 lemma coe_submodule_fg
   (hS : function.injective (algebra_map R S)) (I : ideal R) :
   submodule.fg (coe_submodule S I) ↔ submodule.fg I :=