Theory Fraction_Field_Applications

theory Fraction_Field_Applications
  imports
    Nagata_Lemmas
    Polynomial_Applications
    "HOL-Algebra.Polynomial_Divisibility"
begin

section ‹Constant-prime localization applications›

text ‹
  This theory packages the constant-prime specialization of the polynomial
  application layer at the same level of abstraction as
  @{text "Polynomial_Applications"}: it specializes Nagata's theorem to
  multiplicative sets generated by constant prime polynomials and isolates the
  corresponding descent step for polynomial rings.
›

context domain
begin

lemma polynomial_prime_generated_constant_closure:
  assumes Ksub: "subring K R"
    and A_sub: "A ⊆ carrier (R ⦇carrier := K⦈)"
    and hprime: "⋀q. q ∈ A ⟹ ring_prime⇘K[X]⇙ (poly_of_const q)"
  shows
    "ring_prime_generated (K[X])
      (ring_mult_submonoid_closure (K[X]) (poly_of_const ` A))"
proof (rule ring_prime_generated_mult_submonoid_closure[OF univ_poly_is_ring[OF Ksub]])
  show "poly_of_const ` A ⊆ carrier (K[X])"
  proof
    fix p
    assume p_in: "p ∈ poly_of_const ` A"
    then obtain q where q_in: "q ∈ A" and p_def: "p = poly_of_const q"
      by blast
    have qK: "q ∈ carrier (R ⦇carrier := K⦈)"
      using A_sub q_in by blast
    show "p ∈ carrier (K[X])"
      unfolding p_def by (rule ring_hom_closed[OF canonical_embedding_is_hom[OF Ksub] qK])
  qed
  fix p
  assume "p ∈ poly_of_const ` A"
  then obtain q where q_in: "q ∈ A" and p_def: "p = poly_of_const q"
    by blast
  show "ring_prime⇘K[X]⇙ p"
    unfolding p_def by (rule hprime[OF q_in])
qed

end

locale polynomial_constant_prime_localization =
  fixes R (structure) and P (structure) and S and K :: "'a set" and A :: "'a set"
  assumes poly_axioms: "nagata_localization P S"
    and base_axioms: "domain R"
    and P_eq: "P = K[X]"
    and S_eq: "S = ring_mult_submonoid_closure (K[X]) (ring.poly_of_const (R ⦇carrier := K⦈) ` A)"
begin

abbreviation const_poly where
  "const_poly ≡ ring.poly_of_const (R ⦇carrier := K⦈)"

abbreviation loc_ring where "loc_ring ≡ eq_obj_rng_of_frac.rec_rng_of_frac P S"

text ‹
  Once a localization of @{text "K[X]"} at a constant-prime closure has been
  fixed, Nagata's theorem immediately reduces factoriality of @{text "K[X]"} to
  factoriality of that localization.
›

lemma polynomial_factorial_of_localized_constant_primes_factorial:
  assumes Ksub: "subring K R"
    and A_sub: "A ⊆ carrier (R ⦇carrier := K⦈)"
    and noeth: "noetherian_domain (K[X])"
    and hprime: "⋀q. q ∈ A ⟹ ring_prime⇘K[X]⇙ (const_poly q)"
    and loc_fd: "factorial_domain loc_ring"
  shows "factorial_domain (K[X])"
proof -
  interpret base: domain R
    by (rule base_axioms)
  interpret K_ring: ring "R ⦇carrier := K⦈"
    by (rule base.subring_is_ring[OF Ksub])
  have noethP: "noetherian_domain P"
    using noeth unfolding P_eq .
  have hprimeP: "⋀q. q ∈ A ⟹ ring_prime⇘P⇙ (const_poly q)"
    using P_eq hprime by blast
  have S_closure_eq: "S = ring_mult_submonoid_closure P (const_poly ` A)"
    using P_eq S_eq by blast
  have Aimg_sub: "const_poly ` A ⊆ carrier P"
  proof
    fix p
    assume p_in: "p ∈ const_poly ` A"
    then obtain q where q_in: "q ∈ A" and p_def: "p = const_poly q"
      by blast
    have qK: "q ∈ carrier (R ⦇carrier := K⦈)"
      using A_sub q_in by blast
    have q_poly_in_base: "base.poly_of_const q ∈ carrier (K[X])"
      using ring_hom_memE(1)[OF base.canonical_embedding_is_hom[OF Ksub] qK] by simp
    have p_def_base: "p = base.poly_of_const q"
      using p_def fun_cong[OF base.poly_of_const_consistent[OF Ksub], of q] by simp
    show "p ∈ carrier P"
      unfolding P_eq
      using p_def_base q_poly_in_base by simp
  qed
  have hprime_img: "⋀p. p ∈ const_poly ` A ⟹ ring_prime⇘P⇙ p"
    using hprimeP by blast
  have fdP: "factorial_domain P"
    by (rule nagata_localization.nagata_theorem_of_prime_generators[
          OF poly_axioms noethP S_closure_eq Aimg_sub hprime_img loc_fd])
  show ?thesis
    using fdP unfolding P_eq .
qed

end

end