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_4)
[CommRing A]
[IsDomain A]
[UniqueFactorizationMonoid A]
{K : Type u_5}
[Field K]
[Algebra A K]
[IsFractionRing A K]
(x : K)
:
∃ (a : A) (b : ↥(nonZeroDivisors A)), (∀ {d : A}, d ∣ a → d ∣ ↑b → IsUnit d) ∧ IsLocalization.mk' K a b = x
noncomputable def
IsFractionRing.num
(A : Type u_4)
[CommRing A]
[IsDomain A]
[UniqueFactorizationMonoid A]
{K : Type u_5}
[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 (_ : ∃ (a : A) (b : ↥(nonZeroDivisors A)), (∀ {d : A}, d ∣ a → d ∣ ↑b → IsUnit d) ∧ IsLocalization.mk' K a b = x)
Instances For
noncomputable def
IsFractionRing.den
(A : Type u_4)
[CommRing A]
[IsDomain A]
[UniqueFactorizationMonoid A]
{K : Type u_5}
[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
- One or more equations did not get rendered due to their size.
Instances For
theorem
IsFractionRing.num_den_reduced
(A : Type u_4)
[CommRing A]
[IsDomain A]
[UniqueFactorizationMonoid A]
{K : Type u_5}
[Field K]
[Algebra A K]
[IsFractionRing A K]
(x : K)
{d : A}
:
d ∣ IsFractionRing.num A x → d ∣ ↑(IsFractionRing.den A x) → IsUnit d
theorem
IsFractionRing.mk'_num_den
(A : Type u_4)
[CommRing A]
[IsDomain A]
[UniqueFactorizationMonoid A]
{K : Type u_5}
[Field K]
[Algebra A K]
[IsFractionRing A K]
(x : K)
:
IsLocalization.mk' K (IsFractionRing.num A x) (IsFractionRing.den A x) = x
@[simp]
theorem
IsFractionRing.mk'_num_den'
(A : Type u_4)
[CommRing A]
[IsDomain A]
[UniqueFactorizationMonoid A]
{K : Type u_5}
[Field K]
[Algebra A K]
[IsFractionRing A K]
(x : K)
:
(algebraMap A K) (IsFractionRing.num A x) / (algebraMap A K) ↑(IsFractionRing.den A x) = x
theorem
IsFractionRing.num_mul_den_eq_num_iff_eq
{A : Type u_4}
[CommRing A]
[IsDomain A]
[UniqueFactorizationMonoid A]
{K : Type u_5}
[Field K]
[Algebra A K]
[IsFractionRing A K]
{x : K}
{y : K}
:
x * (algebraMap A K) ↑(IsFractionRing.den A y) = (algebraMap A K) (IsFractionRing.num A y) ↔ x = y
theorem
IsFractionRing.num_mul_den_eq_num_iff_eq'
{A : Type u_4}
[CommRing A]
[IsDomain A]
[UniqueFactorizationMonoid A]
{K : Type u_5}
[Field K]
[Algebra A K]
[IsFractionRing A K]
{x : K}
{y : K}
:
y * (algebraMap A K) ↑(IsFractionRing.den A x) = (algebraMap A K) (IsFractionRing.num A x) ↔ x = y
theorem
IsFractionRing.num_mul_den_eq_num_mul_den_iff_eq
{A : Type u_4}
[CommRing A]
[IsDomain A]
[UniqueFactorizationMonoid A]
{K : Type u_5}
[Field K]
[Algebra A K]
[IsFractionRing A K]
{x : K}
{y : K}
:
IsFractionRing.num A y * ↑(IsFractionRing.den A x) = IsFractionRing.num A x * ↑(IsFractionRing.den A y) ↔ x = y
theorem
IsFractionRing.eq_zero_of_num_eq_zero
{A : Type u_4}
[CommRing A]
[IsDomain A]
[UniqueFactorizationMonoid A]
{K : Type u_5}
[Field K]
[Algebra A K]
[IsFractionRing A K]
{x : K}
(h : IsFractionRing.num A x = 0)
:
x = 0
theorem
IsFractionRing.isInteger_of_isUnit_den
{A : Type u_4}
[CommRing A]
[IsDomain A]
[UniqueFactorizationMonoid A]
{K : Type u_5}
[Field K]
[Algebra A K]
[IsFractionRing A K]
{x : K}
(h : IsUnit ↑(IsFractionRing.den A x))
:
theorem
IsFractionRing.isUnit_den_of_num_eq_zero
{A : Type u_4}
[CommRing A]
[IsDomain A]
[UniqueFactorizationMonoid A]
{K : Type u_5}
[Field K]
[Algebra A K]
[IsFractionRing A K]
{x : K}
(h : IsFractionRing.num A x = 0)
:
IsUnit ↑(IsFractionRing.den A x)