chore(ring_theory/fractional_ideal): prefer (⊤ : ideal R) over 1 (#…

…8298)

`fractional_ideal.lean` sometimes used `1` to denote the ideal of `R` containing each element of `R`. This PR should replace all remaining usages with `⊤ : ideal R`, following the convention in the rest of mathlib.

Also a little `simp` lemma `coe_ideal_top` which was the motivation, since the proof should have been, and is now `by refl`.

src/ring_theory/dedekind_domain.lean

@@ -127,8 +127,8 @@ J⁻¹ = ⟨(1 : fractional_ideal R₁⁰ K) / J, fractional_ideal.fractional_di
 fractional_ideal.div_nonzero _
 
 lemma coe_inv_of_nonzero {J : fractional_ideal R₁⁰ K} (h : J ≠ 0) :
-  (↑J⁻¹ : submodule R₁ K) = is_localization.coe_submodule K 1 / J :=
-by { rwa inv_nonzero _, refl, assumption}
+  (↑J⁻¹ : submodule R₁ K) = is_localization.coe_submodule K ⊤ / J :=
+by { rwa inv_nonzero _, refl, assumption }
 
 /-- `I⁻¹` is the inverse of `I` if `I` has an inverse. -/
 theorem right_inverse_eq (I J : fractional_ideal R₁⁰ K) (h : I * J = 1) :

src/ring_theory/fractional_ideal.lean

@@ -216,12 +216,15 @@ not_iff_not.mpr coe_to_submodule_eq_bot
 instance : inhabited (fractional_ideal S P) := ⟨0⟩
 
 instance : has_one (fractional_ideal S P) :=
-⟨(1 : ideal R)⟩
+⟨(⊤ : ideal R)⟩
 
 variables (S)
 
+@[simp, norm_cast] lemma coe_ideal_top : ((⊤ : ideal R) : fractional_ideal S P) = 1 :=
+rfl
+
 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', rfl⟩, h⟩)
+iff.intro (λ ⟨x', _, h⟩, ⟨x', h⟩) (λ ⟨x', h⟩, ⟨x', ⟨⟩, h⟩)
 
 lemma coe_mem_one (x : R) : algebra_map R P x ∈ (1 : fractional_ideal S P) :=
 (mem_one_iff S).mpr ⟨x, rfl⟩
@@ -235,13 +238,13 @@ variables {S}
 
 However, this is not definitionally equal to `1 : submodule R P`,
 which is proved in the actual `simp` lemma `coe_one`. -/
-lemma coe_one_eq_coe_submodule_one :
-  ↑(1 : fractional_ideal S P) = coe_submodule P (1 : ideal R) :=
+lemma coe_one_eq_coe_submodule_top :
+  ↑(1 : fractional_ideal S P) = coe_submodule P (⊤ : ideal R) :=
 rfl
 
 @[simp, norm_cast] lemma coe_one :
   (↑(1 : fractional_ideal S P) : submodule R P) = 1 :=
-by rw [coe_one_eq_coe_submodule_one, ideal.one_eq_top, coe_submodule_top]
+by rw [coe_one_eq_coe_submodule_top, coe_submodule_top]
 
 section lattice
 
@@ -555,7 +558,7 @@ end
 
 @[simp] lemma map_one :
   (1 : fractional_ideal S P).map g = 1 :=
-map_coe_ideal g 1
+map_coe_ideal g ⊤
 
 @[simp] lemma map_zero :
   (0 : fractional_ideal S P).map g = 0 :=