feat(ring_theory): define fractional_ideal.adjoin_integral (#8296)

This PR shows if `x` is integral over `R`, then `R[x]` is a fractional ideal, and proves some of the essential properties of this fractional ideal.

This is an important step towards showing `is_dedekind_domain_inv` implies that the ring is integrally closed.

Co-Authored-By: Ashvni ashvni.n@gmail.com
Co-Authored-By: Filippo A. E. Nuccio filippo.nuccio@univ-st-etienne.fr

src/ring_theory/fractional_ideal.lean

@@ -1115,6 +1115,30 @@ begin
   apply is_noetherian_coe_to_fractional_ideal,
 end
 
+section adjoin
+
+include loc
+omit frac
+
+variables {R P} (S) (x : P) (hx : is_integral R x)
+
+/-- `A[x]` is a fractional ideal for every integral `x`. -/
+lemma is_fractional_adjoin_integral :
+  is_fractional S (algebra.adjoin R ({x} : set P)).to_submodule :=
+is_fractional_of_fg (fg_adjoin_singleton_of_integral x hx)
+
+/-- `fractional_ideal.adjoin_integral (S : submonoid R) x hx` is `R[x]` as a fractional ideal,
+where `hx` is a proof that `x : P` is integral over `R`. -/
+@[simps]
+def adjoin_integral : fractional_ideal S P :=
+⟨_, is_fractional_adjoin_integral S x hx⟩
+
+lemma mem_adjoin_integral_self :
+  x ∈ adjoin_integral S x hx :=
+algebra.subset_adjoin (set.mem_singleton x)
+
+end adjoin
+
 end fractional_ideal
 
 end ring