Krull domain construction: UFD proof

Shows the intersection subring S is a UFD. Primes of R lying in the maximal ideal remain prime in S the localisation of S away from the product y_1 * y_2 is a UFD Nagata's criterion then gives that S itself is a UFD.

theorem build_R_prime_in_S {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x₁ x₂ : T) (y₁ y₂ : ↥R.carrier) (S_sub : Subring T) (hR_le : R.carrier ≤ S_sub) (hx₁_trans : Transcendental (↥R.carrier) x₁) (hx₂_trans : Transcendental (↥R.carrier) x₂) (hcoprime : ∀ (p : ↥R.carrier), Prime p → ¬(p ∣ y₁ ∧ p ∣ y₂)) (hS_sub_eq : ↑S_sub = {t : T | ∃ (a : T) (b : T), a ∈ intersectionSet R x₁ x₂ y₁ y₂ ∧ b ∈ intersectionSet R x₁ x₂ y₁ y₂ ∧ b ∉ IsLocalRing.maximalIdeal T ∧ t * b = a}) (hR_prime_div_Rbar : ∀ (p : ↥R.carrier), Prime p → ∀ t ∈ intersectionSet R x₁ x₂ y₁ y₂, ∀ (d : T), t = ↑p * d → d ∈ intersectionSet R x₁ x₂ y₁ y₂) (_hinv : ∀ (s : ↥S_sub), ↑s ∉ IsLocalRing.maximalIdeal T → IsUnit s) (p : ↥R.carrier) (hp : Prime p) (hp_M : ↑p ∈ IsLocalRing.maximalIdeal T) : Prime ⟨↑p, ⋯⟩

theorem build_loc_away_ufd {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x₁ x₂ : T) (y₁ y₂ : ↥R.carrier) (S_sub : Subring T) [IsDomain ↥S_sub] (hR_le : R.carrier ≤ S_sub) (hy₁ : ↑y₁ ≠ 0) (hy₂ : ↑y₂ ≠ 0) (hx₁_trans : Transcendental (↥R.carrier) x₁) (hinv : ∀ (s : ↥S_sub), ↑s ∉ IsLocalRing.maximalIdeal T → IsUnit s) (hS_sub_eq : ↑S_sub = {t : T | ∃ (a : T) (b : T), a ∈ intersectionSet R x₁ x₂ y₁ y₂ ∧ b ∈ intersectionSet R x₁ x₂ y₁ y₂ ∧ b ∉ IsLocalRing.maximalIdeal T ∧ t * b = a}) (hRbar_le_S : ∀ t ∈ intersectionSet R x₁ x₂ y₁ y₂, t ∈ ↑S_sub) (hx₁_Rbar : x₁ ∈ intersectionSet R x₁ x₂ y₁ y₂) : UniqueFactorizationMonoid (Localization.Away ((Subring.inclusion hR_le) y₁ * (Subring.inclusion hR_le) y₂))

theorem build_ufd_proof {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x₁ x₂ : T) (y₁ y₂ : ↥R.carrier) (S_sub : Subring T) [IsDomain ↥S_sub] [WfDvdMonoid ↥S_sub] (hR_le : R.carrier ≤ S_sub) (_hcoprime : ∀ (p : ↥R.carrier), Prime p → ¬(p ∣ y₁ ∧ p ∣ y₂)) (hy₁ : ↑y₁ ≠ 0) (hy₂ : ↑y₂ ≠ 0) (hx₁_trans : Transcendental (↥R.carrier) x₁) (_hx₂_trans : Transcendental (↥R.carrier) x₂) (_hx₁_mod_trans : ∀ (p : ↥R.carrier), Prime p → ¬p ∣ y₂ → ∀ (f : Polynomial ↥R.carrier), (Polynomial.aeval x₁) f ∈ Ideal.span {↑p} → Polynomial.C p ∣ f) (_hx₂_mod_trans : ∀ (p : ↥R.carrier), Prime p → ¬p ∣ y₁ → ∀ (f : Polynomial ↥R.carrier), (Polynomial.aeval x₂) f ∈ Ideal.span {↑p} → Polynomial.C p ∣ f) (hinv : ∀ (s : ↥S_sub), ↑s ∉ IsLocalRing.maximalIdeal T → IsUnit s) (hR_prime_in_S : ∀ (p : ↥R.carrier), Prime p → ↑p ∈ IsLocalRing.maximalIdeal T → Prime ⟨↑p, ⋯⟩) (hS_sub_eq : ↑S_sub = {t : T | ∃ (a : T) (b : T), a ∈ intersectionSet R x₁ x₂ y₁ y₂ ∧ b ∈ intersectionSet R x₁ x₂ y₁ y₂ ∧ b ∉ IsLocalRing.maximalIdeal T ∧ t * b = a}) (hRbar_le_S : ∀ t ∈ intersectionSet R x₁ x₂ y₁ y₂, t ∈ ↑S_sub) (hx₁_Rbar : x₁ ∈ intersectionSet R x₁ x₂ y₁ y₂) (_hx₂_Rbar : x₂ ∈ intersectionSet R x₁ x₂ y₁ y₂) : UniqueFactorizationMonoid ↥S_sub

theorem build_primes_preserved {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x₁ x₂ : T) (y₁ y₂ : ↥R.carrier) (S_sub : Subring T) [IsLocalRing ↥S_sub] [UniqueFactorizationMonoid ↥S_sub] (hR_le : R.carrier ≤ S_sub) (hx₁_trans : Transcendental (↥R.carrier) x₁) (hx₂_trans : Transcendental (↥R.carrier) x₂) (hcoprime : ∀ (p : ↥R.carrier), Prime p → ¬(p ∣ y₁ ∧ p ∣ y₂)) (hmax_eq : IsLocalRing.maximalIdeal ↥S_sub = Ideal.comap S_sub.subtype (IsLocalRing.maximalIdeal T)) (hS_sub_eq : ↑S_sub = {t : T | ∃ (a : T) (b : T), a ∈ intersectionSet R x₁ x₂ y₁ y₂ ∧ b ∈ intersectionSet R x₁ x₂ y₁ y₂ ∧ b ∉ IsLocalRing.maximalIdeal T ∧ t * b = a}) (_hR_prime_div_Rbar : ∀ (p : ↥R.carrier), Prime p → ∀ t ∈ intersectionSet R x₁ x₂ y₁ y₂, ∀ (d : T), t = ↑p * d → d ∈ intersectionSet R x₁ x₂ y₁ y₂) (r : ↥R.carrier) (hr : Prime r) : Prime ⟨↑r, ⋯⟩