Generic Ore-localization facts

This file records unconditional fraction and denominator results used by a stage argument. The common-denominator lemma is proved directly from the Ore condition. No flatness, Noetherianity, or freeness of a localized ring over a stage ring is assumed.

theorem AlgebraicAnalysis.OreStageLocalization.exists_common_left_multiple {R : Type u} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (s : Finset ↥S) : ∃ (t : ↥S), ∀ a ∈ s, ∃ (u : R), ↑t = u * ↑a

A finite family of Ore denominators has a common left multiple.

theorem AlgebraicAnalysis.OreStageLocalization.exists_fraction {R : Type u} [Ring R] {S : Submonoid R} [OreLocalization.OreSet S] (x : OreLocalization S R) : ∃ (r : R) (s : ↥S), x = r /ₒ s

Every element of an Ore localization has an explicit numerator/denominator form.

theorem AlgebraicAnalysis.OreStageLocalization.exists_ne_zero_numerator {R : Type u} [Ring R] {S : Submonoid R} [OreLocalization.OreSet S] {x : OreLocalization S R} (hx : x ≠ 0) : ∃ (r : R), r ≠ 0 ∧ ∃ (s : ↥S), x = r /ₒ s

A nonzero localized element has a representative with nonzero numerator.

theorem AlgebraicAnalysis.OreStageLocalization.numerator_injective {R : Type u} [Ring R] [Nontrivial R] [NoZeroDivisors R] {S : Submonoid R} [OreLocalization.OreSet S] (hS : S ≤ nonZeroDivisorsRight R) : Function.Injective ⇑OreLocalization.numeratorHom

Under a right non-zero-divisor hypothesis, the numerator embedding is injective.

theorem AlgebraicAnalysis.OreStageLocalization.denominator_isUnit {R : Type u} [Ring R] {S : Submonoid R} [OreLocalization.OreSet S] (s : ↥S) : IsUnit (OreLocalization.numeratorHom ↑s)

Every chosen denominator becomes a unit in an Ore localization.

theorem AlgebraicAnalysis.OreStageLocalization.nonzero_numerator_isUnit {R : Type u} [Ring R] [Nontrivial R] [NoZeroDivisors R] [OreLocalization.OreSet (nonZeroDivisors R)] {r : R} (hr : r ≠ 0) : IsUnit (OreLocalization.numeratorHom r)

Every nonzero numerator is a unit in the full Ore division-ring localization.

theorem AlgebraicAnalysis.OreStageLocalization.full_isUnit_of_ne_zero {R : Type u} [Ring R] [Nontrivial R] [NoZeroDivisors R] [OreLocalization.OreSet (nonZeroDivisors R)] {x : OreLocalization (nonZeroDivisors R) R} (hx : x ≠ 0) : IsUnit x

Every nonzero element of the full Ore localization is a unit.