Module

UniqueFactorizationMonoid_of_isLocalization_away_of_prime.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.UniqueFactorizationMonoid_of_isLocalization_away_of_prime

5 declarations indexed from sourceView source ↗

Module documentation

Unique Factorization Monoid of is Localization away of prime

Imports6

Mathlib.RingTheory.Localization.Away.Basic
Mathlib.RingTheory.Localization.Ideal
Mathlib.RingTheory.Noetherian.Defs
Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain
Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
Mathlib.Tactic.Ring.RingNF

Imported by2

lemma

pow_dvd_of_pow_dvd_mul_left

L35 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.UniqueFactorizationMonoid_of_isLocalization_away_of_prime.P2mNagata.pow_dvd_of_pow_dvd_mul_left

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace UniqueFactorizationMonoid_of_isLocalization_away_of_prime
namespace P2mNagata
open IsLocalization
variable {R : Type*} [CommRing R] [IsDomain R]

Lean source · statement

lemma pow_dvd_of_pow_dvd_mul_left {x r : R} (hx : Prime x) (hr : ¬x ∣ r) :
    ∀ (n : ℕ) (c : R), x ^ n ∣ r * c → x ^ n ∣ c

lemma

algebraMap_injective

L56 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.UniqueFactorizationMonoid_of_isLocalization_away_of_prime.P2mNagata.algebraMap_injective

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace UniqueFactorizationMonoid_of_isLocalization_away_of_prime
namespace P2mNagata
open IsLocalization
variable {R : Type*} [CommRing R] [IsDomain R]
variable {x : R} (S : Type*) [CommRing S] [Algebra R S] [IsLocalization.Away x S]

Lean source · statement

lemma algebraMap_injective (hx0 : x ≠ 0) : Function.Injective (algebraMap R S)

lemma

prime_of_prime_algebraMap

L60 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.UniqueFactorizationMonoid_of_isLocalization_away_of_prime.P2mNagata.prime_of_prime_algebraMap

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace UniqueFactorizationMonoid_of_isLocalization_away_of_prime
namespace P2mNagata
open IsLocalization
variable {R : Type*} [CommRing R] [IsDomain R]
variable {x : R} (S : Type*) [CommRing S] [Algebra R S] [IsLocalization.Away x S]

Lean source · statement

lemma prime_of_prime_algebraMap (hx : Prime x) {r₀ : R} (hr₀ : ¬x ∣ r₀) (hunit : ¬IsUnit r₀)
    (hprime : Prime (algebraMap R S r₀)) : Prime r₀

theorem

main

L81 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.UniqueFactorizationMonoid_of_isLocalization_away_of_prime.P2mNagata.main

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace UniqueFactorizationMonoid_of_isLocalization_away_of_prime
namespace P2mNagata
open IsLocalization
variable {R : Type*} [CommRing R] [IsDomain R]
variable {x : R} (S : Type*) [CommRing S] [Algebra R S] [IsLocalization.Away x S]

Lean source · statement

theorem main [IsNoetherianRing R] (hx : Prime x) [IsDomain S] [UniqueFactorizationMonoid S] :
    UniqueFactorizationMonoid R

theorem

of_isLocalization_away_of_prime

L131 ↗

UniqueFactorizationMonoid.of_isLocalization_away_of_prime

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace UniqueFactorizationMonoid_of_isLocalization_away_of_prime

Lean source · statement

theorem _root_.UniqueFactorizationMonoid.of_isLocalization_away_of_prime
    {R : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] {x : R} (hx : Prime x)
    (S : Type*) [CommRing S] [IsDomain S] [Algebra R S] [IsLocalization.Away x S]
    [UniqueFactorizationMonoid S] : UniqueFactorizationMonoid R

Module documentation

Unique Factorization Monoid of is Localization away of prime

Declarations

pow_dvd_of_pow_dvd_mul_left

algebraMap_injective

prime_of_prime_algebraMap

main

of_isLocalization_away_of_prime