Locally Finite Linearly Ordered Abelian Groups

Main results

• LocallyFiniteOrder.orderAddMonoidEquiv: Any nontrivial linearly ordered additive abelian group that is locally finite is isomorphic to ℤ.
• LocallyFiniteOrder.orderMonoidEquiv: Any nontrivial linearly ordered abelian group that is locally finite is isomorphic to Multiplicative ℤ.
• LocallyFiniteOrder.orderMonoidWithZeroEquiv: Any nontrivial linearly ordered abelian group with zero that is locally finite is isomorphic to ℤᵐ⁰.

theorem Finset.card_Ico_mul_right {M : Type u_1} [CancelCommMonoid M] [LinearOrder M] [IsOrderedMonoid M] [LocallyFiniteOrder M] [ExistsMulOfLE M] (a b c : M) : (Ico (a * c) (b * c)).card = (Ico a b).card

theorem Finset.card_Ico_add_right {M : Type u_1} [AddCancelCommMonoid M] [LinearOrder M] [IsOrderedAddMonoid M] [LocallyFiniteOrder M] [ExistsAddOfLE M] (a b c : M) : (Ico (a + c) (b + c)).card = (Ico a b).card

theorem card_Ico_one_mul {M : Type u_1} [CancelCommMonoid M] [LinearOrder M] [IsOrderedMonoid M] [LocallyFiniteOrder M] [ExistsMulOfLE M] (a b : M) (ha : 1 ≤ a) (hb : 1 ≤ b) : (Finset.Ico 1 (a * b)).card = (Finset.Ico 1 a).card + (Finset.Ico 1 b).card

theorem card_Ico_zero_add {M : Type u_1} [AddCancelCommMonoid M] [LinearOrder M] [IsOrderedAddMonoid M] [LocallyFiniteOrder M] [ExistsAddOfLE M] (a b : M) (ha : 0 ≤ a) (hb : 0 ≤ b) : (Finset.Ico 0 (a + b)).card = (Finset.Ico 0 a).card + (Finset.Ico 0 b).card

def LocallyFiniteOrder.addMonoidHom (G : Type u_2) [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [LocallyFiniteOrder G] : G →+ ℤ

The canonical embedding (as a monoid hom) from a linearly ordered cancellative additive monoid into ℤ. This is either surjective or zero.

Equations

• LocallyFiniteOrder.addMonoidHom G = { toFun := fun (a : G) => ↑(Finset.Ico 0 a).card - ↑(Finset.Ico 0 (-a)).card, map_zero' := ⋯, map_add' := ⋯ }

def LocallyFiniteOrder.orderAddMonoidHom (G : Type u_2) [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [LocallyFiniteOrder G] : G →+o ℤ

The canonical embedding (as an ordered monoid hom) from a linearly ordered cancellative group into ℤ. This is either surjective or zero.

Equations

• LocallyFiniteOrder.orderAddMonoidHom G = { toAddMonoidHom := LocallyFiniteOrder.addMonoidHom G, monotone' := ⋯ }

@[simp]

theorem LocallyFiniteOrder.orderAddMonoidHom_toAddMonoidHom {G : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [LocallyFiniteOrder G] : ↑(orderAddMonoidHom G) = addMonoidHom G

@[simp]

theorem LocallyFiniteOrder.orderAddMonoidHom_apply {G : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [LocallyFiniteOrder G] (x : G) : (orderAddMonoidHom G) x = (addMonoidHom G) x

theorem LocallyFiniteOrder.orderAddMonoidHom_strictMono {G : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [LocallyFiniteOrder G] : StrictMono ⇑(orderAddMonoidHom G)

theorem LocallyFiniteOrder.orderAddMonoidHom_bijective {G : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [LocallyFiniteOrder G] [Nontrivial G] : Function.Bijective ⇑(orderAddMonoidHom G)

noncomputable def LocallyFiniteOrder.orderAddMonoidEquiv (G : Type u_2) [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [LocallyFiniteOrder G] [Nontrivial G] : G ≃+o ℤ

Any nontrivial linearly ordered abelian group that is locally finite is isomorphic to ℤ.

Equations

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

theorem LocallyFiniteOrder.orderAddMonoidEquiv_apply {G : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [LocallyFiniteOrder G] [Nontrivial G] (x : G) : (orderAddMonoidEquiv G) x = (addMonoidHom G) x

noncomputable def LocallyFiniteOrder.orderMonoidEquiv (G : Type u_3) [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [LocallyFiniteOrder G] [Nontrivial G] : G ≃*o Multiplicative ℤ

Any linearly ordered abelian group that is locally finite embeds to Multiplicative ℤ.

Equations

• LocallyFiniteOrder.orderMonoidEquiv G = OrderAddMonoidIso.toMultiplicative (LocallyFiniteOrder.orderAddMonoidEquiv (Additive G))

noncomputable def LocallyFiniteOrder.orderMonoidHom (G : Type u_3) [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [LocallyFiniteOrder G] : G →*o Multiplicative ℤ

Any linearly ordered abelian group that is locally finite embeds into Multiplicative ℤ.

Equations

• LocallyFiniteOrder.orderMonoidHom G = { toMonoidHom := AddMonoidHom.toMultiplicative (LocallyFiniteOrder.orderAddMonoidHom (Additive G)).toAddMonoidHom, monotone' := ⋯ }

theorem LocallyFiniteOrder.orderMonoidHom_strictMono {G : Type u_3} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [LocallyFiniteOrder G] : StrictMono ⇑(orderMonoidHom G)

noncomputable def LocallyFiniteOrder.orderMonoidWithZeroEquiv (G : Type u_3) [LinearOrderedCommGroupWithZero G] [LocallyFiniteOrder Gˣ] [Nontrivial Gˣ] : G ≃*o WithZero (Multiplicative ℤ)

Any nontrivial linearly ordered abelian group with zero that is locally finite is isomorphic to ℤᵐ⁰.

Equations

• LocallyFiniteOrder.orderMonoidWithZeroEquiv G = OrderMonoidIso.withZeroUnits.symm.trans (OrderMonoidIso.withZero (LocallyFiniteOrder.orderMonoidEquiv Gˣ))

noncomputable def LocallyFiniteOrder.orderMonoidWithZeroHom (G : Type u_3) [LinearOrderedCommGroupWithZero G] [LocallyFiniteOrder Gˣ] : G →*₀o WithZero (Multiplicative ℤ)

Any linearly ordered abelian group with zero that is locally finite embeds into ℤᵐ⁰.

Equations

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

theorem LocallyFiniteOrder.orderMonoidWithZeroHom_strictMono {G : Type u_3} [LinearOrderedCommGroupWithZero G] [LocallyFiniteOrder Gˣ] : StrictMono ⇑(orderMonoidWithZeroHom G)