Numerator and denominator in a localization

Implementation notes

See Mathlib/RingTheory/Localization/Basic.lean for a design overview.

Tags

localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions

theorem IsFractionRing.exists_reduced_fraction (A : Type u_1) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) : ∃ (a : A) (b : ↥(nonZeroDivisors A)), IsRelPrime a ↑b ∧ IsLocalization.mk' K a b = x

noncomputable def IsFractionRing.num (A : Type u_1) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) : A

f.num x is the numerator of x : f.codomain as a reduced fraction.

Equations

• IsFractionRing.num A x = Classical.choose ⋯

noncomputable def IsFractionRing.den (A : Type u_1) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) : ↥(nonZeroDivisors A)

f.den x is the denominator of x : f.codomain as a reduced fraction.

Equations

• IsFractionRing.den A x = Classical.choose ⋯

theorem IsFractionRing.num_den_reduced (A : Type u_1) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) : IsRelPrime (num A x) ↑(den A x)

theorem IsFractionRing.mk'_num_den (A : Type u_1) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) : IsLocalization.mk' K (num A x) (den A x) = x

@[simp]

theorem IsFractionRing.mk'_num_den' (A : Type u_1) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) : (algebraMap A K) (num A x) / (algebraMap A K) ↑(den A x) = x

theorem IsFractionRing.num_mul_den_eq_num_iff_eq {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {x y : K} : x * (algebraMap A K) ↑(den A y) = (algebraMap A K) (num A y) ↔ x = y

theorem IsFractionRing.num_mul_den_eq_num_iff_eq' {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {x y : K} : y * (algebraMap A K) ↑(den A x) = (algebraMap A K) (num A x) ↔ x = y

theorem IsFractionRing.num_mul_den_eq_num_mul_den_iff_eq {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {x y : K} : num A y * ↑(den A x) = num A x * ↑(den A y) ↔ x = y

theorem IsFractionRing.eq_zero_of_num_eq_zero {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {x : K} (h : num A x = 0) : x = 0

@[simp]

theorem IsFractionRing.num_zero {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] : num A 0 = 0

@[simp]

theorem IsFractionRing.num_eq_zero {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) : num A x = 0 ↔ x = 0

theorem IsFractionRing.isInteger_of_isUnit_den {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {x : K} (h : IsUnit ↑(den A x)) : IsLocalization.IsInteger A x

theorem IsFractionRing.isUnit_den_iff {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) : IsUnit ↑(den A x) ↔ IsLocalization.IsInteger A x

theorem IsFractionRing.isUnit_den_zero {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] : IsUnit ↑(den A 0)

theorem IsFractionRing.associated_den_num_inv {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) (hx : x ≠ 0) : Associated (↑(den A x)) (num A x⁻¹)

theorem IsFractionRing.associated_num_den_inv {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) (hx : x ≠ 0) : Associated (num A x) ↑(den A x⁻¹)