Theory Nagata_Factoriality
theory Nagata_Factoriality
imports
Prime_Generated
Nagata_Lemmas
Polynomial_Applications
Fraction_Field_Applications
"HOL-Computational_Algebra.Polynomial"
begin
section ‹Nagata-factoriality scaffolding›
text ‹
Nagata's factoriality theorem descends unique factorization from a localization
to the base ring under a prime-generated hypothesis on the multiplicative
set. The present entry now packages the prime-generated core, a wrapper
layer over the AFP localization entry, and a record-based HOL-Algebra proof
of both the prime-generated and prime-or-unit descent variants in
@{text Nagata_Lemmas}. That theory now also packages theorem-level
entry points for submonoid closures generated by prime families, including
a finite-generator wrapper. The additional theories
@{text Polynomial_Applications} and @{text Fraction_Field_Applications}
package abstract polynomial applications for localization away @{text X} and
for localizations generated by constant prime polynomials, cf.\ Nagata and
Samuel.\<^cite>‹"Nagata1962"› \<^cite>‹"Samuel1964"›
›
lemma prime_generated_constant_prime_polynomials:
fixes A :: "'a :: semidom set"
assumes "⋀c. c ∈ A ⟹ prime_elem c"
shows "prime_generated (mult_submonoid_closure ((λc. [:c:]) ` A))"
proof (rule prime_generated_mult_submonoid_closure)
fix q
assume "q ∈ (λc. [:c:]) ` A"
then obtain c where "c ∈ A" and q_def: "q = [:c:]"
by blast
from assms[OF ‹c ∈ A›] show "prime_elem q"
unfolding q_def by (rule lift_prime_elem_poly)
qed
corollary zero_notin_constant_prime_polynomial_closure:
fixes A :: "'a :: idom set"
assumes "⋀c. c ∈ A ⟹ prime_elem c"
shows "0 ∉ mult_submonoid_closure ((λc. [:c:]) ` A)"
proof -
have "prime_generated (mult_submonoid_closure ((λc. [:c:]) ` A))"
using assms by (rule prime_generated_constant_prime_polynomials)
then show ?thesis
by (rule zero_notin_prime_generated[where S = "mult_submonoid_closure ((λc. [:c:]) ` A)"])
qed
text ‹
The last corollary isolates one of the key configurations in the
constant-prime polynomial application: the multiplicative set generated by
constant prime polynomials is prime-generated and therefore avoids zero.
›
text ‹
Separately, the theory @{text Localization_Interface} exposes an Isabelle/HOL
wrapper around the AFP localization construction with lemmas for representative
equality, numerator-denominator surjectivity, denominator rescaling,
cross-multiplication in the domain case, units coming from both the
multiplicative set and base-ring units, and injectivity of the canonical
localization map under the usual domain hypotheses. On top of that,
@{text Nagata_Lemmas} proves the descent lemmas needed for Nagata's theorem,
together with a record-based multiplicative-closure API
@{thm [display] ring_prime_generated_mult_submonoid_closure} for the
constant-prime submonoids used in the fraction-field route, culminating in
theorem statements @{thm [display] nagata_localization.nagata_theorem} and
@{thm [display] nagata_localization.nagata_theorem_of_prime_or_unit} together with the
prime-generator closure wrappers
@{thm [display] nagata_localization.nagata_theorem_of_prime_generators} and
@{thm [display] nagata_localization.nagata_theorem_of_finite_prime_generators}. The theory
@{text Polynomial_Applications} then specializes this framework to the
polynomial ring case by proving @{thm [display] domain.polynomial_prime_X} over
fields and the abstract away-X descent theorem
@{thm [display] polynomial_away_X_localization.polynomial_factorial_of_localized_X_factorial}, while
@{text Fraction_Field_Applications} packages the companion constant-prime
closure theorem
@{thm [display] polynomial_constant_prime_localization.polynomial_factorial_of_localized_constant_primes_factorial}.
›
end