Localization over left Ore sets. #
This file defines the localization of a monoid over a left Ore set and proves its universal mapping property.
Notations #
Introduces the notation R[S⁻¹]
for the Ore localization of a monoid R
at a right Ore
subset S
. Also defines a new heterogeneous division notation r /ₒ s
for a numerator r : R
and
a denominator s : S
.
References #
- https://ncatlab.org/nlab/show/Ore+localization
- [Zoran Škoda, Noncommutative localization in noncommutative geometry][skoda2006]
Tags #
localization, Ore, non-commutative
The setoid on R × S
used for the Ore localization.
Equations
Instances For
The setoid on R × S
used for the Ore localization.
Equations
Instances For
The Ore localization of an additive monoid and a submonoid fulfilling the Ore condition.
Equations
- AddOreLocalization S X = Quotient (AddOreLocalization.oreEqv S X)
Instances For
The Ore localization of a monoid and a submonoid fulfilling the Ore condition.
Equations
- OreLocalization S X = Quotient (OreLocalization.oreEqv S X)
Instances For
The Ore localization of a monoid and a submonoid fulfilling the Ore condition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The subtraction in the Ore localization,
as a difference of an element of X
and S
.
Equations
- r -ₒ s = Quotient.mk' (r, s)
Instances For
The division in the Ore localization X[S⁻¹]
, as a fraction of an element of X
and S
.
Equations
- r /ₒ s = Quotient.mk' (r, s)
Instances For
The division in the Ore localization X[S⁻¹]
, as a fraction of an element of X
and S
.
Equations
- OreLocalization.«term_/ₒ_» = Lean.ParserDescr.trailingNode `OreLocalization.term_/ₒ_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " /ₒ ") (Lean.ParserDescr.cat `term 71))
Instances For
The subtraction in the Ore localization,
as a difference of an element of X
and S
.
Equations
- OreLocalization.«term_-ₒ_» = Lean.ParserDescr.trailingNode `OreLocalization.term_-ₒ_ 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " -ₒ ") (Lean.ParserDescr.cat `term 66))
Instances For
A difference r -ₒ s
is equal to its expansion by an
arbitrary translation t
if t + s ∈ S
.
A difference is equal to its expansion by a summand from S
.
Differences whose minuends differ by a common summand can be proven equal if
those summands expand to equal elements of R
.
Fractions which differ by a factor of the numerator can be proven equal if
those factors expand to equal elements of R
.
A function or predicate over X
and S
can be lifted to the localizaton if it is
invariant under expansion on the left.
Equations
- AddOreLocalization.liftExpand P hP = Quotient.lift (fun (p : X × ↥S) => P p.1 p.2) ⋯
Instances For
A function or predicate over X
and S
can be lifted to X[S⁻¹]
if it is invariant
under expansion on the left.
Equations
- OreLocalization.liftExpand P hP = Quotient.lift (fun (p : X × ↥S) => P p.1 p.2) ⋯
Instances For
A version of liftExpand
used to simultaneously lift functions with two arguments
Equations
- AddOreLocalization.lift₂Expand P hP = AddOreLocalization.liftExpand (fun (r₁ : X) (s₁ : ↥S) => AddOreLocalization.liftExpand (P r₁ s₁) ⋯) ⋯
Instances For
A version of liftExpand
used to simultaneously lift functions with two arguments
in X[S⁻¹]
.
Equations
- OreLocalization.lift₂Expand P hP = OreLocalization.liftExpand (fun (r₁ : X) (s₁ : ↥S) => OreLocalization.liftExpand (P r₁ s₁) ⋯) ⋯
Instances For
the vector addition on the Ore localization of additive monoids.
Equations
- AddOreLocalization.vadd = AddOreLocalization.liftExpand OreLocalization.vadd'' ⋯
Instances For
The scalar multiplication on the Ore localization of monoids.
Equations
- OreLocalization.smul = OreLocalization.liftExpand OreLocalization.smul'' ⋯
Instances For
Equations
- AddOreLocalization.instVAdd = { vadd := AddOreLocalization.vadd }
Equations
- OreLocalization.instSMul = { smul := OreLocalization.smul }
Equations
- AddOreLocalization.instAdd = { add := AddOreLocalization.vadd }
Equations
- OreLocalization.instMul = { mul := OreLocalization.smul }
A characterization lemma for the vector addition on the Ore localization, allowing for a choice of Ore minuend and Ore subtrahend.
A characterization lemma for the scalar multiplication on the Ore localization, allowing for a choice of Ore numerator and Ore denominator.
A characterization lemma for the addition on the Ore localization, allowing for a choice of Ore minuend and Ore subtrahend.
A characterization lemma for the multiplication on the Ore localization, allowing for a choice of Ore numerator and Ore denominator.
Another characterization lemma for the vector addition on the Ore localizaion delivering Ore witnesses and conditions bundled in a sigma type.
Equations
- AddOreLocalization.oreSubVAddChar' r₁ r₂ s₁ s₂ = ⟨AddOreLocalization.oreMin r₁ s₂, ⟨AddOreLocalization.oreSubtra r₁ s₂, ⋯⟩⟩
Instances For
Another characterization lemma for the scalar multiplication on the Ore localizaion delivering Ore witnesses and conditions bundled in a sigma type.
Equations
- OreLocalization.oreDivSMulChar' r₁ r₂ s₁ s₂ = ⟨OreLocalization.oreNum r₁ s₂, ⟨OreLocalization.oreDenom r₁ s₂, ⋯⟩⟩
Instances For
Another characterization lemma for the addition on the Ore localizaion delivering Ore witnesses and conditions bundled in a sigma type.
Equations
- AddOreLocalization.oreSubAddChar' r₁ r₂ s₁ s₂ = ⟨AddOreLocalization.oreMin r₁ s₂, ⟨AddOreLocalization.oreSubtra r₁ s₂, ⋯⟩⟩
Instances For
Another characterization lemma for the multiplication on the Ore localizaion delivering Ore witnesses and conditions bundled in a sigma type.
Equations
- OreLocalization.oreDivMulChar' r₁ r₂ s₁ s₂ = ⟨OreLocalization.oreNum r₁ s₂, ⟨OreLocalization.oreDenom r₁ s₂, ⋯⟩⟩
Instances For
0
in the additive localization, defined as 0 -ₒ 0
.
Instances For
1
in the localization, defined as 1 /ₒ 1
.
Instances For
Equations
- AddOreLocalization.instZero = { zero := AddOreLocalization.zero }
Equations
- OreLocalization.instOne = { one := OreLocalization.one }
Equations
- AddOreLocalization.instInhabited = { default := 0 }
Equations
- OreLocalization.instInhabited = { default := 1 }
Equations
- AddOreLocalization.nsmul = nsmulRec
Instances For
Equations
- OreLocalization.npow = npowRec
Instances For
Equations
- AddOreLocalization.instAddMonoid = AddMonoid.mk ⋯ ⋯ AddOreLocalization.nsmul ⋯ ⋯
Equations
- AddOreLocalization.instAddActionOreLocalization = AddAction.mk ⋯ ⋯
Equations
- OreLocalization.instMulActionOreLocalization = MulAction.mk ⋯ ⋯
The difference s -ₒ 0
as a an additive unit.
Equations
- AddOreLocalization.numeratorAddUnit s = { val := ↑s -ₒ 0, neg := 0 -ₒ s, val_neg := ⋯, neg_val := ⋯ }
Instances For
The fraction s /ₒ 1
as a unit in R[S⁻¹]
, where s : S
.
Equations
- OreLocalization.numeratorUnit s = { val := ↑s /ₒ 1, inv := 1 /ₒ s, val_inv := ⋯, inv_val := ⋯ }
Instances For
The additive homomorphism from R
to AddOreLocalization R S
,
mapping r : R
to the difference r -ₒ 0
.
Equations
Instances For
The multiplicative homomorphism from R
to R[S⁻¹]
, mapping r : R
to the
fraction r /ₒ 1
.
Equations
Instances For
The universal lift from a morphism R →+ T
, which maps elements of S
to
additive-units of T
, to a morphism AddOreLocalization R S →+ T
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The universal lift from a morphism R →* T
, which maps elements of S
to units of T
,
to a morphism R[S⁻¹] →* T
.
Equations
- OreLocalization.universalMulHom f fS hf = { toFun := fun (x : OreLocalization S R) => OreLocalization.liftExpand (fun (r : R) (s : ↥S) => ↑(fS s)⁻¹ * f r) ⋯ x, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The universal morphism universalAddHom
is unique.
The universal morphism universalMulHom
is unique.
Vector addition in an additive monoid localization.
Equations
- AddOreLocalization.hvadd c = AddOreLocalization.liftExpand (fun (m : X) (s : ↥S) => AddOreLocalization.oreMin (c +ᵥ 0) s +ᵥ m -ₒ AddOreLocalization.oreSubtra (c +ᵥ 0) s) ⋯
Instances For
Scalar multiplication in a monoid localization.
Equations
- OreLocalization.hsmul c = OreLocalization.liftExpand (fun (m : X) (s : ↥S) => OreLocalization.oreNum (c • 1) s • m /ₒ OreLocalization.oreDenom (c • 1) s) ⋯
Instances For
Equations
- AddOreLocalization.instVAddOfIsScalarTower = { vadd := AddOreLocalization.hvadd }
Equations
- OreLocalization.instSMulOfIsScalarTower = { smul := OreLocalization.hsmul }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- AddOreLocalization.instAddActionOfIsScalarTower = AddAction.mk ⋯ ⋯
Equations
- OreLocalization.instMulActionOfIsScalarTower = MulAction.mk ⋯ ⋯
Equations
- AddOreLocalization.instAddCommMonoid = AddCommMonoid.mk ⋯
Equations
- OreLocalization.instCommMonoid = CommMonoid.mk ⋯
0
in the localization, defined as 0 /ₒ 1
.
Instances For
Equations
- OreLocalization.instZero = { zero := OreLocalization.zero }
Equations
- OreLocalization.instMonoidWithZero = MonoidWithZero.mk ⋯ ⋯
Equations
- OreLocalization.instCommMonoidWithZero = CommMonoidWithZero.mk ⋯ ⋯
Equations
- OreLocalization.instAdd = { add := OreLocalization.add }
A characterization of the addition on the Ore localizaion, allowing for arbitrary Ore numerator and Ore denominator.
Another characterization of the addition on the Ore localization, bundling up all witnesses and conditions into a sigma type.
Equations
- OreLocalization.oreDivAddChar' r r' s s' = ⟨OreLocalization.oreNum (↑s) s', ⟨OreLocalization.oreDenom (↑s) s', ⋯⟩⟩
Instances For
Equations
- OreLocalization.instAddMonoid = AddMonoid.mk ⋯ ⋯ OreLocalization.nsmul ⋯ ⋯
Equations
- OreLocalization.instDistribMulAction = DistribMulAction.mk ⋯ ⋯
Equations
- OreLocalization.instDistribMulActionOfIsScalarTower = DistribMulAction.mk ⋯ ⋯
Equations
- OreLocalization.instAddCommMonoidOreLocalization = AddCommMonoid.mk ⋯
Negation on the Ore localization is defined via negation on the numerator.
Equations
- OreLocalization.neg = OreLocalization.liftExpand (fun (r : X) (s : ↥S) => -r /ₒ s) ⋯
Instances For
Equations
- OreLocalization.instNegOreLocalization = { neg := OreLocalization.neg }
Equations
- OreLocalization.zsmul = zsmulRec
Instances For
Equations
- OreLocalization.instAddGroupOreLocalization = AddGroup.mk ⋯
Equations
- OreLocalization.instAddCommGroup = AddCommGroup.mk ⋯