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 toMultiplicative ℤ
.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)
:
theorem
Finset.card_Ico_add_right
{M : Type u_1}
[AddCancelCommMonoid M]
[LinearOrder M]
[IsOrderedAddMonoid M]
[LocallyFiniteOrder M]
[ExistsAddOfLE M]
(a b c : M)
:
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)
:
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)
:
def
LocallyFiniteOrder.addMonoidHom
(G : Type u_2)
[AddCommGroup G]
[LinearOrder G]
[IsOrderedAddMonoid G]
[LocallyFiniteOrder 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' := ⋯ }
Instances For
def
LocallyFiniteOrder.orderAddMonoidHom
(G : Type u_2)
[AddCommGroup G]
[LinearOrder G]
[IsOrderedAddMonoid G]
[LocallyFiniteOrder G]
:
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' := ⋯ }
Instances For
@[simp]
theorem
LocallyFiniteOrder.orderAddMonoidHom_toAddMonoidHom
{G : Type u_2}
[AddCommGroup G]
[LinearOrder G]
[IsOrderedAddMonoid G]
[LocallyFiniteOrder G]
:
@[simp]
theorem
LocallyFiniteOrder.orderAddMonoidHom_apply
{G : Type u_2}
[AddCommGroup G]
[LinearOrder G]
[IsOrderedAddMonoid G]
[LocallyFiniteOrder G]
(x : G)
:
theorem
LocallyFiniteOrder.orderAddMonoidHom_strictMono
{G : Type u_2}
[AddCommGroup G]
[LinearOrder G]
[IsOrderedAddMonoid G]
[LocallyFiniteOrder G]
:
theorem
LocallyFiniteOrder.orderAddMonoidHom_bijective
{G : Type u_2}
[AddCommGroup G]
[LinearOrder G]
[IsOrderedAddMonoid G]
[LocallyFiniteOrder G]
[Nontrivial G]
:
noncomputable def
LocallyFiniteOrder.orderAddMonoidEquiv
(G : Type u_2)
[AddCommGroup G]
[LinearOrder G]
[IsOrderedAddMonoid G]
[LocallyFiniteOrder G]
[Nontrivial G]
:
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.
Instances For
theorem
LocallyFiniteOrder.orderAddMonoidEquiv_apply
{G : Type u_2}
[AddCommGroup G]
[LinearOrder G]
[IsOrderedAddMonoid G]
[LocallyFiniteOrder G]
[Nontrivial G]
(x : G)
:
noncomputable def
LocallyFiniteOrder.orderMonoidEquiv
(G : Type u_3)
[CommGroup G]
[LinearOrder G]
[IsOrderedMonoid G]
[LocallyFiniteOrder G]
[Nontrivial G]
:
Any linearly ordered abelian group that is locally finite embeds to Multiplicative ℤ
.
Equations
Instances For
noncomputable def
LocallyFiniteOrder.orderMonoidHom
(G : Type u_3)
[CommGroup G]
[LinearOrder G]
[IsOrderedMonoid G]
[LocallyFiniteOrder G]
:
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' := ⋯ }
Instances For
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ˣ]
:
Any nontrivial linearly ordered abelian group with zero that is locally finite
is isomorphic to ℤᵐ⁰
.
Equations
Instances For
noncomputable def
LocallyFiniteOrder.orderMonoidWithZeroHom
(G : Type u_3)
[LinearOrderedCommGroupWithZero G]
[LocallyFiniteOrder Gˣ]
:
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.
Instances For
theorem
LocallyFiniteOrder.orderMonoidWithZeroHom_strictMono
{G : Type u_3}
[LinearOrderedCommGroupWithZero G]
[LocallyFiniteOrder Gˣ]
: