Right Ore localization

The opposite-ring presentation of a right Ore localization and its right-denominator clearing API. Extracted from Stafford38 commit c8a513d553b24c7c08da82f496c44dbbaeb1f2fc.

def AlgebraicAnalysis.OreRightLocalization.oppositeSubmonoid {R : Type u} [Monoid R] (S : Submonoid R) : Submonoid Rᵐᵒᵖ

The copy of S in the opposite ring.

Equations

• AlgebraicAnalysis.OreRightLocalization.oppositeSubmonoid S = { carrier := {x : Rᵐᵒᵖ | MulOpposite.unop x ∈ S}, mul_mem' := ⋯, one_mem' := ⋯ }

@[reducible, inline]

abbrev AlgebraicAnalysis.OreRightLocalization.RightOreLocalization (R : Type u) [Ring R] (S : Submonoid R) [OreLocalization.OreSet (oppositeSubmonoid S)] : Type u

The right Ore localization of R, implemented as the opposite of Mathlib's left Ore localization of Rᵐᵒᵖ.

Equations

• AlgebraicAnalysis.OreRightLocalization.RightOreLocalization R S = (OreLocalization (AlgebraicAnalysis.OreRightLocalization.oppositeSubmonoid S) Rᵐᵒᵖ)ᵐᵒᵖ

def AlgebraicAnalysis.OreRightLocalization.rightNumeratorRingHom {R : Type u} [Ring R] {S : Submonoid R} [OreLocalization.OreSet (oppositeSubmonoid S)] : R →+* RightOreLocalization R S

The numerator map into the right Ore localization.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicAnalysis.OreRightLocalization.rightOre_clear {R : Type u} [Ring R] {S : Submonoid R} [OreLocalization.OreSet (oppositeSubmonoid S)] (q : RightOreLocalization R S) : ∃ (a : R), ∃ s ∈ S, IsUnit (rightNumeratorRingHom s) ∧ q * rightNumeratorRingHom s = rightNumeratorRingHom a

Every element of a right Ore localization has a right denominator in S which is a unit and clears the fraction.