Divisible Hull of an abelian group

This file constructs the divisible hull of an AddCommMonoid as a ℕ-module localized at ℕ+ (implemented using nonZeroDivisors ℕ), which is a ℚ≥0-module.

Furthermore, we show that

• when M is a group, so is DivisibleHull M, which is also a ℚ-module
• when M is linearly ordered and cancellative, so is DivisibleHull M, which is also an ordered ℚ≥0-module.
• when M is a linearly ordered group, DivisibleHull M is an ordered ℚ-module, and ArchimedeanClass is preserved.

Despite the name, this file doesn't implement a DivisibleBy instance on DivisibleHull. This should be implemented on LocalizedModule in a more general setting (TODO: implement this). This file mainly focuses on the specialization to ℕ and the linear order property introduced by it.

Main declarations

• DivisibleHull M is the divisible hull of an abelian group.
• DivisibleHull.archimedeanClassOrderIso M is the equivalence between ArchimedeanClass M and ArchimedeanClass (DivisibleHull M).

@[reducible, inline]

abbrev DivisibleHull (M : Type u_1) [AddCommMonoid M] : Type u_1

The divisible hull of a AddCommMonoid (as a ℕ-module) is the localized module by ℕ+ (implemented using nonZeroDivisors ℕ), thus a ℕ-divisble group, or a ℚ≥0-module.

Equations

• DivisibleHull M = LocalizedModule (nonZeroDivisors ℕ) M

def DivisibleHull.mk {M : Type u_1} [AddCommMonoid M] (m : M) (s : ℕ+) : DivisibleHull M

Create an element m / s.

Equations

• DivisibleHull.mk m s = LocalizedModule.mk m (PNat.equivNonZeroDivisorsNat s)

@[reducible, inline]

abbrev DivisibleHull.coe {M : Type u_1} [AddCommMonoid M] (m : M) : DivisibleHull M

Define coercion as m ↦ m / 1.

Equations

• ↑m = DivisibleHull.mk m 1

instance DivisibleHull.instCoe {M : Type u_1} [AddCommMonoid M] : Coe M (DivisibleHull M)

Coercion from M to DivisibleHull M defined as m ↦ m / 1.

Equations

• DivisibleHull.instCoe = { coe := DivisibleHull.coe }

@[simp]

theorem DivisibleHull.mk_zero {M : Type u_1} [AddCommMonoid M] (s : ℕ+) : mk 0 s = 0

theorem DivisibleHull.ind {M : Type u_1} [AddCommMonoid M] {motive : DivisibleHull M → Prop} (mk : ∀ (num : M) (den : ℕ+), motive (mk num den)) (x : DivisibleHull M) : motive x

theorem DivisibleHull.mk_eq_mk {M : Type u_1} [AddCommMonoid M] {m m' : M} {s s' : ℕ+} : mk m s = mk m' s' ↔ ∃ (u : ℕ+), ↑u • ↑s' • m = ↑u • ↑s • m'

def DivisibleHull.liftOn {M : Type u_1} [AddCommMonoid M] {α : Type u_2} (x : DivisibleHull M) (f : M → ℕ+ → α) (h : ∀ (m m' : M) (s s' : ℕ+), mk m s = mk m' s' → f m s = f m' s') : α

If f : M → ℕ+ → α respects the equivalence on localization, lift it to a function DivisibleHull M → α.

Equations

• x.liftOn f h = LocalizedModule.liftOn x (fun (p : M × ↥(nonZeroDivisors ℕ)) => f p.1 (PNat.equivNonZeroDivisorsNat.symm p.2)) ⋯

@[simp]

theorem DivisibleHull.liftOn_mk {M : Type u_1} [AddCommMonoid M] {α : Type u_2} (m : M) (s : ℕ+) (f : M → ℕ+ → α) (h : ∀ (m m' : M) (s s' : ℕ+), mk m s = mk m' s' → f m s = f m' s') : (mk m s).liftOn f h = f m s

def DivisibleHull.liftOn₂ {M : Type u_1} [AddCommMonoid M] {α : Type u_2} (x y : DivisibleHull M) (f : M → ℕ+ → M → ℕ+ → α) (h : ∀ (m n m' n' : M) (s t s' t' : ℕ+), mk m s = mk m' s' → mk n t = mk n' t' → f m s n t = f m' s' n' t') : α

If f : M → ℕ+ → M → ℕ+ → α respects the equivalence on localization, lift it to a function DivisibleHull M → DivisibleHull M → α.

Equations

• x.liftOn₂ y f h = LocalizedModule.liftOn₂ x y (fun (p q : M × ↥(nonZeroDivisors ℕ)) => f p.1 (PNat.equivNonZeroDivisorsNat.symm p.2) q.1 (PNat.equivNonZeroDivisorsNat.symm q.2)) ⋯

@[simp]

theorem DivisibleHull.liftOn₂_mk {M : Type u_1} [AddCommMonoid M] {α : Type u_2} (m m' : M) (s s' : ℕ+) (f : M → ℕ+ → M → ℕ+ → α) (h : ∀ (m n m' n' : M) (s t s' t' : ℕ+), mk m s = mk m' s' → mk n t = mk n' t' → f m s n t = f m' s' n' t') : (mk m s).liftOn₂ (mk m' s') f h = f m s m' s'

theorem DivisibleHull.mk_add_mk {M : Type u_1} [AddCommMonoid M] {m1 m2 : M} {s1 s2 : ℕ+} : mk m1 s1 + mk m2 s2 = mk (↑s2 • m1 + ↑s1 • m2) (s1 * s2)

theorem DivisibleHull.mk_add_mk_left {M : Type u_1} [AddCommMonoid M] {m1 m2 : M} {s : ℕ+} : mk m1 s + mk m2 s = mk (m1 + m2) s

@[simp]

theorem DivisibleHull.coe_add {M : Type u_1} [AddCommMonoid M] {m1 m2 : M} : ↑(m1 + m2) = ↑m1 + ↑m2

def DivisibleHull.coeAddMonoidHom (M : Type u_1) [AddCommMonoid M] : M →+ DivisibleHull M

Coercion from M to DivisibleHull M as an AddMonoidHom.

Equations

• DivisibleHull.coeAddMonoidHom M = { toFun := DivisibleHull.coe, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem DivisibleHull.coeAddMonoidHom_apply (M : Type u_1) [AddCommMonoid M] (m : M) : (coeAddMonoidHom M) m = ↑m

theorem DivisibleHull.nsmul_mk {M : Type u_1} [AddCommMonoid M] (a : ℕ) (m : M) (s : ℕ+) : a • mk m s = mk (a • m) s

theorem DivisibleHull.nnqsmul_mk {M : Type u_1} [AddCommMonoid M] (a : ℚ≥0) (m : M) (s : ℕ+) : a • mk m s = mk (a.num • m) (⟨a.den, ⋯⟩ * s)

theorem DivisibleHull.mk_eq_mk_iff_smul_eq_smul {M : Type u_1} [AddCommMonoid M] [IsAddTorsionFree M] {m m' : M} {s s' : ℕ+} : mk m s = mk m' s' ↔ ↑s' • m = ↑s • m'

theorem DivisibleHull.mk_left_injective {M : Type u_1} [AddCommMonoid M] [IsAddTorsionFree M] (s : ℕ+) : Function.Injective fun (m : M) => mk m s

theorem DivisibleHull.coe_injective {M : Type u_1} [AddCommMonoid M] [IsAddTorsionFree M] : Function.Injective coe

@[simp]

theorem DivisibleHull.coe_inj {M : Type u_1} [AddCommMonoid M] [IsAddTorsionFree M] {m m' : M} : ↑m = ↑m' ↔ m = m'

theorem DivisibleHull.neg_mk {M : Type u_2} [AddCommGroup M] (m : M) (s : ℕ+) : -mk m s = mk (-m) s

noncomputable instance DivisibleHull.instSMulRat {M : Type u_2} [AddCommGroup M] : SMul ℚ (DivisibleHull M)

Equations

• DivisibleHull.instSMulRat = { smul := fun (a : ℚ) (x : DivisibleHull M) => ↑(SignType.sign a) • (have this := ⟨|a|, ⋯⟩; this) • x }

theorem DivisibleHull.qsmul_def {M : Type u_2} [AddCommGroup M] (a : ℚ) (x : DivisibleHull M) : a • x = ↑(SignType.sign a) • (have this := ⟨|a|, ⋯⟩; this) • x

theorem DivisibleHull.zero_qsmul {M : Type u_2} [AddCommGroup M] (x : DivisibleHull M) : 0 • x = 0

theorem DivisibleHull.qsmul_of_nonneg {M : Type u_2} [AddCommGroup M] {a : ℚ} (h : 0 ≤ a) (x : DivisibleHull M) : a • x = (have this := ⟨a, h⟩; this) • x

theorem DivisibleHull.qsmul_of_nonpos {M : Type u_2} [AddCommGroup M] {a : ℚ} (h : a ≤ 0) (x : DivisibleHull M) : a • x = -((have this := ⟨-a, ⋯⟩; this) • x)

theorem DivisibleHull.qsmul_mk {M : Type u_2} [AddCommGroup M] (a : ℚ) (m : M) (s : ℕ+) : a • mk m s = mk (a.num • m) (⟨a.den, ⋯⟩ * s)

noncomputable instance DivisibleHull.instModuleRat {M : Type u_2} [AddCommGroup M] : Module ℚ (DivisibleHull M)

Equations

• DivisibleHull.instModuleRat = { toSMul := DivisibleHull.instSMulRat, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

theorem DivisibleHull.zsmul_mk {M : Type u_2} [AddCommGroup M] (a : ℤ) (m : M) (s : ℕ+) : a • mk m s = mk (a • m) s

instance DivisibleHull.instLE {M : Type u_2} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] : LE (DivisibleHull M)

Equations

• DivisibleHull.instLE = { le := fun (x y : DivisibleHull M) => x.liftOn₂ y (fun (m : M) (s : ℕ+) (n : M) (t : ℕ+) => ↑t • m ≤ ↑s • n) ⋯ }

@[simp]

theorem DivisibleHull.mk_le_mk {M : Type u_2} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] {m m' : M} {s s' : ℕ+} : mk m s ≤ mk m' s' ↔ ↑s' • m ≤ ↑s • m'

instance DivisibleHull.instLinearOrder {M : Type u_2} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] : LinearOrder (DivisibleHull M)

Equations

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

@[simp]

theorem DivisibleHull.mk_lt_mk {M : Type u_2} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] {m m' : M} {s s' : ℕ+} : mk m s < mk m' s' ↔ ↑s' • m < ↑s • m'

instance DivisibleHull.instIsOrderedCancelAddMonoid {M : Type u_2} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] : IsOrderedCancelAddMonoid (DivisibleHull M)

instance DivisibleHull.instIsStrictOrderedModuleNNRat {M : Type u_2} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] : IsStrictOrderedModule ℚ≥0 (DivisibleHull M)

instance DivisibleHull.instIsStrictOrderedModuleRat {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : IsStrictOrderedModule ℚ (DivisibleHull M)

def DivisibleHull.coeOrderAddMonoidHom (M : Type u_2) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : M →+o DivisibleHull M

Coercion from M to DivisibleHull M as an OrderAddMonoidHom.

Equations

• DivisibleHull.coeOrderAddMonoidHom M = { toAddMonoidHom := DivisibleHull.coeAddMonoidHom M, monotone' := ⋯ }

@[simp]

theorem DivisibleHull.coeOrderAddMonoidHom_apply (M : Type u_2) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (m : M) : (coeOrderAddMonoidHom M) m = ↑m

theorem DivisibleHull.archimedeanClassMk_mk_eq {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (m : M) (s s' : ℕ+) : ArchimedeanClass.mk (mk m s) = ArchimedeanClass.mk (mk m s')

ArchimedeanClass.mk of an element from DivisibleHull only depends on the numerator.

noncomputable def DivisibleHull.archimedeanClassOrderIso (M : Type u_2) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : ArchimedeanClass M ≃o ArchimedeanClass (DivisibleHull M)

The Archimedean classes of DivisibleHull M are the same as those of M.

Equations

• DivisibleHull.archimedeanClassOrderIso M = OrderIso.ofHomInv (DivisibleHull.archimedeanClassOrderHom✝ M) (DivisibleHull.archimedeanClassOrderHomInv✝ M) ⋯ ⋯

@[simp]

theorem DivisibleHull.archimedeanClassOrderIso_apply {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (a : ArchimedeanClass M) : (archimedeanClassOrderIso M) a = (ArchimedeanClass.orderHom (coeOrderAddMonoidHom M)) a

@[simp]

theorem DivisibleHull.archimedeanClassOrderIso_symm_apply {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (m : M) (s : ℕ+) : (archimedeanClassOrderIso M).symm (ArchimedeanClass.mk (mk m s)) = ArchimedeanClass.mk m