Convex subgroups of linearly ordered groups

A subgroup of a group with a linear order is convex if it contains every element lying between two of its members. That definition, the closure and preimage constructions and the elementary exclusion lemmas need no more than a group with a linear order. The results that make convex subgroups useful for valuation theory need the value-group setting, a linearly ordered commutative group: there any two convex subgroups are comparable, each has a largest convex subgroup avoiding a given element, and the quotient by one carries a linear order making it an ordered group again — so convex subgroups are exactly the kernels of the order-compatible quotients of a value group. This file develops the basic theory following Wedhorn, Adic Spaces (arXiv:1910.05934v1), §1.4 and §7.1; the convex subgroup cΓ_v(I) of Wedhorn Definition 7.3 is intended to be built from closure in the forthcoming valuation-spectrum development of Spv (A, I).

Main definitions

• TauCeti.ConvexSubgroup Γ : The type of order-convex subgroups of Γ.
• TauCeti.ConvexSubgroup.quotientLinearOrder : The linear order on Γ ⧸ H.toSubgroup induced by a convex subgroup H.
• TauCeti.ConvexSubgroup.quotientIsOrderedMonoid : That order is compatible with the quotient group structure.
• TauCeti.ConvexSubgroup.closure S : The smallest convex subgroup containing a set.
• TauCeti.ConvexSubgroup.maxAvoid hγ : The largest convex subgroup avoiding γ ≠ 1.
• TauCeti.ConvexSubgroup.comap : The preimage of a convex subgroup under a monotone monoid homomorphism.

Main results

• TauCeti.ConvexSubgroup.le_total : Convex subgroups are totally ordered by inclusion.
• TauCeti.ConvexSubgroup.mem_closure_singleton : The convex subgroup generated by one element consists of the elements whose absolute value is bounded by a power of it.
• TauCeti.ConvexSubgroup.closure_singleton_pow : An element and its nonzero powers generate the same convex subgroup.
• TauCeti.ConvexSubgroup.mem_closure_of_nonempty_of_mul_mem_of_one_le : For a nonempty set of elements ≥ 1 closed under multiplication, membership in the convex closure is boundedness by a single member.
• TauCeti.ConvexSubgroup.lt_closure_singleton : An element outside a convex subgroup generates a strictly larger one.
• TauCeti.ConvexSubgroup.mulArchimedean_iff_forall_eq_bot_or_eq_top : A linearly ordered commutative group is MulArchimedean exactly when its only convex subgroups are ⊥ and ⊤.
• TauCeti.ConvexSubgroup.nontrivial_quotient_maxAvoid and TauCeti.ConvexSubgroup.mulArchimedean_quotient_maxAvoid : quotienting by the largest convex subgroup avoiding a convex-generating element gives a nontrivial archimedean group.
• TauCeti.ConvexSubgroup.quotientBotOrderIso : The quotient by ⊥ is the group itself, as an order isomorphism, so order-theoretic properties transfer across it.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, §1.4, §7.1

Ported from the AINTLIB development projects/AdicSpaces/Adic spaces/OrderedGroupConvex.lean, adapted to the pinned Mathlib: the quotient order is obtained from Mathlib's condensation API (Quotient.instLinearOrder over order-connected fibers) rather than constructed by hand.

quotientMk_monotone and quotientMk_lt_one_of_notMem come from a different AINTLIB file: projects/AdicSpaces/Adic spaces/ValuationCoarsening.lean at commit 37bbdaeb, where they are the order facts the coarsening construction consumes.

structure TauCeti.ConvexSubgroup (Γ : Type u_1) [Group Γ] [LinearOrder Γ] extends Subgroup Γ : Type u_1

A convex subgroup of a group Γ with a linear order is a subgroup that is order-convex: if a ≤ x ≤ b and a, b ∈ H, then x ∈ H.

• carrier : Set Γ
• mul_mem' {a b : Γ} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier
• inv_mem' {x : Γ} : x ∈ self.carrier → x⁻¹ ∈ self.carrier
• ordConnected' : self.carrier.OrdConnected

@[instance_reducible]

instance TauCeti.ConvexSubgroup.instSetLike {Γ : Type u_1} [Group Γ] [LinearOrder Γ] : SetLike (ConvexSubgroup Γ) Γ

Equations

• TauCeti.ConvexSubgroup.instSetLike = { coe := fun (H : TauCeti.ConvexSubgroup Γ) => H.carrier, coe_injective := ⋯ }

instance TauCeti.ConvexSubgroup.instSubgroupClass {Γ : Type u_1} [Group Γ] [LinearOrder Γ] : SubgroupClass (ConvexSubgroup Γ) Γ

theorem TauCeti.ConvexSubgroup.ext {Γ : Type u_1} [Group Γ] [LinearOrder Γ] {H₁ H₂ : ConvexSubgroup Γ} (h : ∀ (x : Γ), x ∈ H₁ ↔ x ∈ H₂) : H₁ = H₂

theorem TauCeti.ConvexSubgroup.ext_iff {Γ : Type u_1} [Group Γ] [LinearOrder Γ] {H₁ H₂ : ConvexSubgroup Γ} : H₁ = H₂ ↔ ∀ (x : Γ), x ∈ H₁ ↔ x ∈ H₂

theorem TauCeti.ConvexSubgroup.ordConnected {Γ : Type u_1} [Group Γ] [LinearOrder Γ] (H : ConvexSubgroup Γ) : (↑H).OrdConnected

A convex subgroup is an order-connected subset.

theorem TauCeti.ConvexSubgroup.convex {Γ : Type u_1} [Group Γ] [LinearOrder Γ] (H : ConvexSubgroup Γ) {a b x : Γ} (ha : a ∈ H) (hb : b ∈ H) (h₁ : a ≤ x) (h₂ : x ≤ b) : x ∈ H

Convexity: if a, b ∈ H and a ≤ x ≤ b, then x ∈ H.

theorem TauCeti.ConvexSubgroup.mem_of_one_le_le {Γ : Type u_1} [Group Γ] [LinearOrder Γ] {H : ConvexSubgroup Γ} {x h : Γ} (hh : h ∈ H) (h1 : 1 ≤ x) (hx : x ≤ h) : x ∈ H

A convex subgroup contains every element between 1 and one of its members.

theorem TauCeti.ConvexSubgroup.mem_of_le_le_one {Γ : Type u_1} [Group Γ] [LinearOrder Γ] {H : ConvexSubgroup Γ} {x h : Γ} (hh : h ∈ H) (hx : h ≤ x) (h1 : x ≤ 1) : x ∈ H

A convex subgroup contains every element between one of its members and 1.

@[instance_reducible]

instance TauCeti.ConvexSubgroup.instBot {Γ : Type u_1} [Group Γ] [LinearOrder Γ] : Bot (ConvexSubgroup Γ)

The trivial subgroup {1} is convex.

Equations

• TauCeti.ConvexSubgroup.instBot = { bot := let __Subgroup := ⊥; { toSubgroup := __Subgroup, ordConnected' := ⋯ } }

@[instance_reducible]

instance TauCeti.ConvexSubgroup.instTop {Γ : Type u_1} [Group Γ] [LinearOrder Γ] : Top (ConvexSubgroup Γ)

The full group is a convex subgroup.

Equations

• TauCeti.ConvexSubgroup.instTop = { top := let __Subgroup := ⊤; { toSubgroup := __Subgroup, ordConnected' := ⋯ } }

@[simp]

theorem TauCeti.ConvexSubgroup.mem_bot {Γ : Type u_1} [Group Γ] [LinearOrder Γ] {x : Γ} : x ∈ ⊥ ↔ x = 1

@[simp]

theorem TauCeti.ConvexSubgroup.mem_top {Γ : Type u_1} [Group Γ] [LinearOrder Γ] {x : Γ} : x ∈ ⊤

@[instance_reducible]

instance TauCeti.ConvexSubgroup.instPartialOrder {Γ : Type u_1} [Group Γ] [LinearOrder Γ] : PartialOrder (ConvexSubgroup Γ)

Convex subgroups are ordered by inclusion.

Equations

• TauCeti.ConvexSubgroup.instPartialOrder = PartialOrder.ofSetLike (TauCeti.ConvexSubgroup Γ)

@[instance_reducible]

instance TauCeti.ConvexSubgroup.instOrderBot {Γ : Type u_1} [Group Γ] [LinearOrder Γ] : OrderBot (ConvexSubgroup Γ)

Equations

• TauCeti.ConvexSubgroup.instOrderBot = { toBot := TauCeti.ConvexSubgroup.instBot, bot_le := ⋯ }

@[instance_reducible]

instance TauCeti.ConvexSubgroup.instOrderTop {Γ : Type u_1} [Group Γ] [LinearOrder Γ] : OrderTop (ConvexSubgroup Γ)

Equations

• TauCeti.ConvexSubgroup.instOrderTop = { toTop := TauCeti.ConvexSubgroup.instTop, le_top := ⋯ }

The underlying subgroup

Membership, the underlying set, the order and the two lattice ends all agree with their Subgroup counterparts definitionally. Naming them lets proofs move between a convex subgroup and H.toSubgroup by rewriting.

@[simp]

theorem TauCeti.ConvexSubgroup.mem_toSubgroup {Γ : Type u_1} [Group Γ] [LinearOrder Γ] {H : ConvexSubgroup Γ} {x : Γ} : x ∈ H.toSubgroup ↔ x ∈ H

Membership in the underlying subgroup is membership in the convex subgroup.

@[simp]

theorem TauCeti.ConvexSubgroup.coe_toSubgroup {Γ : Type u_1} [Group Γ] [LinearOrder Γ] (H : ConvexSubgroup Γ) : ↑H.toSubgroup = ↑H

The underlying subgroup has the same underlying set.

@[simp]

theorem TauCeti.ConvexSubgroup.toSubgroup_le {Γ : Type u_1} [Group Γ] [LinearOrder Γ] {H K : ConvexSubgroup Γ} : H.toSubgroup ≤ K.toSubgroup ↔ H ≤ K

Inclusion of convex subgroups is inclusion of the underlying subgroups.

@[simp]

theorem TauCeti.ConvexSubgroup.toSubgroup_lt {Γ : Type u_1} [Group Γ] [LinearOrder Γ] {H K : ConvexSubgroup Γ} : H.toSubgroup < K.toSubgroup ↔ H < K

Strict inclusion of convex subgroups is strict inclusion of the underlying subgroups.

theorem TauCeti.ConvexSubgroup.toSubgroup_injective {Γ : Type u_1} [Group Γ] [LinearOrder Γ] : Function.Injective toSubgroup

A convex subgroup is determined by the subgroup underlying it: convexity is a property, not extra data.

@[simp]

theorem TauCeti.ConvexSubgroup.toSubgroup_inj {Γ : Type u_1} [Group Γ] [LinearOrder Γ] {H K : ConvexSubgroup Γ} : H.toSubgroup = K.toSubgroup ↔ H = K

Two convex subgroups are equal exactly when their underlying subgroups are.

@[simp]

theorem TauCeti.ConvexSubgroup.bot_toSubgroup {Γ : Type u_1} [Group Γ] [LinearOrder Γ] : ⊥.toSubgroup = ⊥

The underlying subgroup of the trivial convex subgroup is the trivial subgroup.

@[simp]

theorem TauCeti.ConvexSubgroup.top_toSubgroup {Γ : Type u_1} [Group Γ] [LinearOrder Γ] : ⊤.toSubgroup = ⊤

The underlying subgroup of the full convex subgroup is the full subgroup.

Elements outside a convex subgroup

theorem TauCeti.ConvexSubgroup.lt_of_notMem_of_le_one {Γ : Type u_1} [Group Γ] [LinearOrder Γ] (H : ConvexSubgroup Γ) {γ : Γ} (hγ : γ ∉ H) (hγ1 : γ ≤ 1) {h : Γ} (hh : h ∈ H) : γ < h

If γ ∉ H and γ ≤ 1, then γ lies strictly below every member of H.

theorem TauCeti.ConvexSubgroup.lt_of_notMem_of_one_le {Γ : Type u_1} [Group Γ] [LinearOrder Γ] (H : ConvexSubgroup Γ) {γ : Γ} (hγ : γ ∉ H) (hγ1 : 1 ≤ γ) {h : Γ} (hh : h ∈ H) : h < γ

If γ ∉ H and 1 ≤ γ, then γ lies strictly above every member of H.

theorem TauCeti.ConvexSubgroup.notMem_of_notMem_of_one_le_le {Γ : Type u_1} [Group Γ] [LinearOrder Γ] (H : ConvexSubgroup Γ) {γ : Γ} (hγ : γ ∉ H) (hγ1 : 1 ≤ γ) {x : Γ} (hγx : γ ≤ x) : x ∉ H

If γ ∉ H and 1 ≤ γ, then no element above γ lies in H.

theorem TauCeti.ConvexSubgroup.notMem_of_notMem_of_le_le_one {Γ : Type u_1} [Group Γ] [LinearOrder Γ] (H : ConvexSubgroup Γ) {γ : Γ} (hγ : γ ∉ H) (hγ1 : γ ≤ 1) {x : Γ} (hxγ : x ≤ γ) : x ∉ H

If γ ∉ H and γ ≤ 1, then no element below γ lies in H.

The smallest convex subgroup containing a set

def TauCeti.ConvexSubgroup.closure {Γ : Type u_1} [Group Γ] [LinearOrder Γ] (S : Set Γ) : ConvexSubgroup Γ

The smallest convex subgroup containing a set S, as the intersection of all convex subgroups containing S. The convex subgroup cΓ_v(I) of Wedhorn Definition 7.3 will be an instance of this construction.

Equations

• TauCeti.ConvexSubgroup.closure S = { carrier := {x : Γ | ∀ (H : TauCeti.ConvexSubgroup Γ), S ⊆ ↑H → x ∈ H}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯, ordConnected' := ⋯ }

theorem TauCeti.ConvexSubgroup.mem_closure {Γ : Type u_1} [Group Γ] [LinearOrder Γ] {S : Set Γ} {x : Γ} : x ∈ closure S ↔ ∀ (H : ConvexSubgroup Γ), S ⊆ ↑H → x ∈ H

Membership in the convex closure: membership in every convex subgroup containing the generating set. Deliberately not a simp lemma — as a normal form it would rewrite every x ∈ closure S into the defining intersection, exposing the construction. closure_le is the universal property simp should use instead.

theorem TauCeti.ConvexSubgroup.subset_closure {Γ : Type u_1} [Group Γ] [LinearOrder Γ] (S : Set Γ) : S ⊆ ↑(closure S)

The generating set is contained in its convex closure.

@[simp]

theorem TauCeti.ConvexSubgroup.closure_le {Γ : Type u_1} [Group Γ] [LinearOrder Γ] {S : Set Γ} {H : ConvexSubgroup Γ} : closure S ≤ H ↔ S ⊆ ↑H

Universal property: closure S lies inside a convex subgroup iff the generating set does.

@[simp]

theorem TauCeti.ConvexSubgroup.closure_inv {Γ : Type u_1} [Group Γ] [LinearOrder Γ] (S : Set Γ) : closure S⁻¹ = closure S

The convex subgroup generated by a set is generated by its inverse image.

@[simp]

theorem TauCeti.ConvexSubgroup.closure_singleton_inv {Γ : Type u_1} [Group Γ] [LinearOrder Γ] (y : Γ) : closure {y⁻¹} = closure {y}

The convex subgroup generated by an element equals the one generated by its inverse.

Preimages of convex subgroups

def TauCeti.ConvexSubgroup.comap {Γ : Type u_1} [Group Γ] [LinearOrder Γ] {Δ : Type u_2} {F : Type u_3} [Group Δ] [LinearOrder Δ] [FunLike F Γ Δ] [MonoidHomClass F Γ Δ] [OrderHomClass F Γ Δ] (f : F) (K : ConvexSubgroup Δ) : ConvexSubgroup Γ

The preimage of a convex subgroup under an ordered group homomorphism is a convex subgroup. This lifts convex subgroups from quotient value groups back to the original value group.

Equations

• TauCeti.ConvexSubgroup.comap f K = { toSubgroup := Subgroup.comap (↑f) K.toSubgroup, ordConnected' := ⋯ }

@[simp]

theorem TauCeti.ConvexSubgroup.mem_comap {Γ : Type u_1} [Group Γ] [LinearOrder Γ] {Δ : Type u_2} {F : Type u_3} [Group Δ] [LinearOrder Δ] [FunLike F Γ Δ] [MonoidHomClass F Γ Δ] [OrderHomClass F Γ Δ] {f : F} {K : ConvexSubgroup Δ} {x : Γ} : x ∈ comap f K ↔ f x ∈ K

def TauCeti.ConvexSubgroup.comapUnitsWithZero {Γ : Type u_1} [Group Γ] [LinearOrder Γ] (K : ConvexSubgroup Γ) : ConvexSubgroup (WithZero Γ)ˣ

The comap of a convex subgroup along the identification (WithZero Γ)ˣ ≃*o Γ.

This is what carries a convex subgroup of a value group over to the units of the value monoid containing it, which is the form a restriction of a valuation consumes.

Equations

• K.comapUnitsWithZero = TauCeti.ConvexSubgroup.comap OrderMonoidIso.unitsWithZero K

@[simp]

theorem TauCeti.ConvexSubgroup.mem_comapUnitsWithZero {Γ : Type u_1} [Group Γ] [LinearOrder Γ] {K : ConvexSubgroup Γ} {u : (WithZero Γ)ˣ} : u ∈ K.comapUnitsWithZero ↔ OrderMonoidIso.unitsWithZero u ∈ K

Membership in the transported subgroup is membership of the corresponding value group element: the unit u is carried across by OrderMonoidIso.unitsWithZero.

Total ordering of convex subgroups

theorem TauCeti.ConvexSubgroup.le_total {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] (H₁ H₂ : ConvexSubgroup Γ) : H₁ ≤ H₂ ∨ H₂ ≤ H₁

Any two convex subgroups are comparable.

@[instance_reducible]

noncomputable instance TauCeti.ConvexSubgroup.instLinearOrder {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] : LinearOrder (ConvexSubgroup Γ)

Equations

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

The largest convex subgroup avoiding an element

theorem TauCeti.ConvexSubgroup.mem_of_mabs_le_mabs {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] {H : ConvexSubgroup Γ} {x h : Γ} (hh : h ∈ H) (hx : |x|ₘ ≤ |h|ₘ) : x ∈ H

An element bounded in absolute value by a member of a convex subgroup is a member.

noncomputable def TauCeti.ConvexSubgroup.maxAvoid {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] {γ : Γ} (hγ : γ ≠ 1) : ConvexSubgroup Γ

The largest convex subgroup avoiding an element γ ≠ 1: Mathlib's Archimedean open ball at the class of γ, that is, the elements of strictly larger Archimedean class. Reusing MulArchimedeanClass.ballSubgroup rather than building the directed union of all convex subgroups avoiding γ gives the same subgroup with the group structure already in place.

Equations

• TauCeti.ConvexSubgroup.maxAvoid hγ = { toSubgroup := (MulArchimedeanClass.mk γ).ballSubgroup, ordConnected' := ⋯ }

@[simp]

theorem TauCeti.ConvexSubgroup.mem_maxAvoid_iff {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] {γ : Γ} {hγ : γ ≠ 1} {x : Γ} : x ∈ maxAvoid hγ ↔ MulArchimedeanClass.mk γ < MulArchimedeanClass.mk x

Membership in maxAvoid hγ: a strictly larger Archimedean class than γ.

theorem TauCeti.ConvexSubgroup.notMem_maxAvoid {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] {γ : Γ} (hγ : γ ≠ 1) : γ ∉ maxAvoid hγ

The avoided element is not a member.

@[simp]

theorem TauCeti.ConvexSubgroup.le_maxAvoid {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] {γ : Γ} {hγ : γ ≠ 1} {H : ConvexSubgroup Γ} : H ≤ maxAvoid hγ ↔ γ ∉ H

Universal property: a convex subgroup lies inside maxAvoid hγ iff it excludes γ.

The convex subgroup generated by a multiplicatively closed set

@[simp]

theorem TauCeti.ConvexSubgroup.mem_closure_of_nonempty_of_mul_mem_of_one_le {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] {S : Set Γ} (hne : S.Nonempty) (hmul : ∀ x ∈ S, ∀ y ∈ S, x * y ∈ S) (hge : ∀ x ∈ S, 1 ≤ x) {x : Γ} : x ∈ closure S ↔ ∃ g ∈ S, g⁻¹ ≤ x ∧ x ≤ g

For a nonempty, multiplicatively closed set of elements ≥ 1, membership in the convex closure is boundedness by a single member.

This is what one needs whenever a convex subgroup is generated by the values a multiplicative map attains — for instance the characteristic subgroup cΓ_v of a valuation, generated by the attained values ≥ 1, where it says that a single attained value already bounds.

The convex subgroup generated by one element

@[simp]

theorem TauCeti.ConvexSubgroup.mem_closure_singleton {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] {y x : Γ} : x ∈ closure {y} ↔ ∃ (n : ℕ), |x|ₘ ≤ |y|ₘ ^ n

The convex subgroup generated by a single element consists of the elements whose absolute value is bounded by a power of |y|ₘ — the closed archimedean ball of y.

@[simp]

theorem TauCeti.ConvexSubgroup.closure_singleton_pow {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] {γ : Γ} {n : ℕ} (hn : n ≠ 0) : closure {γ ^ n} = closure {γ}

An element and its nonzero natural powers generate the same convex subgroup. No nontriviality is required — at γ = 1 both sides are ⊥.

Wedhorn needs this in Lemma 7.2: the largest value is attained on a finitely generated ideal J with √I = √J, so it is only some power of it that is attained on I itself.

theorem TauCeti.ConvexSubgroup.lt_closure_singleton {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] {C : ConvexSubgroup Γ} {h : Γ} (hC : h ∉ C) : C < closure {h}

An element outside a convex subgroup generates a strictly larger convex subgroup. Wedhorn needs this in the proof of Lemma 7.2 to know cΓ_v ⊊ H before Lemma 7.1 may be applied to the subgroup H generated by the largest value of a generating set. No side condition on h is needed.

The Archimedean characterization

theorem TauCeti.ConvexSubgroup.eq_bot_or_eq_top_of_mulArchimedean {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] [MulArchimedean Γ] (H : ConvexSubgroup Γ) : H = ⊥ ∨ H = ⊤

In a MulArchimedean group every convex subgroup is ⊥ or ⊤.

theorem TauCeti.ConvexSubgroup.mulArchimedean_of_forall_eq_bot_or_eq_top {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] (h : ∀ (H : ConvexSubgroup Γ), H = ⊥ ∨ H = ⊤) : MulArchimedean Γ

If every convex subgroup is ⊥ or ⊤, the group is MulArchimedean.

theorem TauCeti.ConvexSubgroup.mulArchimedean_iff_forall_eq_bot_or_eq_top {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] : MulArchimedean Γ ↔ ∀ (H : ConvexSubgroup Γ), H = ⊥ ∨ H = ⊤

The Archimedean characterization. A linearly ordered commutative group is MulArchimedean iff its only convex subgroups are ⊥ and ⊤.

The quotient linear order

@[instance_reducible]

noncomputable instance TauCeti.ConvexSubgroup.quotientLinearOrder {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] (H : ConvexSubgroup Γ) : LinearOrder (Γ ⧸ H.toSubgroup)

The quotient of Γ by a convex subgroup H is linearly ordered, as the condensation of Γ along the order-connected cosets. The body is not exposed: consumers work through quotient_le_iff rather than by unfolding the condensation.

Equations

• H.quotientLinearOrder = Quotient.instLinearOrder

@[simp]

theorem TauCeti.ConvexSubgroup.quotient_le_iff {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] (H : ConvexSubgroup Γ) (a b : Γ) : ↑a ≤ ↑b ↔ b⁻¹ * a ≤ 1 ∨ b⁻¹ * a ∈ H.toSubgroup

The defining unfolding of ≤ on the quotient by a convex subgroup: [a] ≤ [b] iff b⁻¹ * a ≤ 1 or b⁻¹ * a ∈ H.

instance TauCeti.ConvexSubgroup.quotientIsOrderedMonoid {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] (H : ConvexSubgroup Γ) : IsOrderedMonoid (Γ ⧸ H.toSubgroup)

The quotient linear order is compatible with the group operation.

theorem TauCeti.ConvexSubgroup.quotientMk_monotone {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] (H : ConvexSubgroup Γ) : Monotone ⇑(QuotientGroup.mk' H.toSubgroup)

The quotient map Γ →* Γ ⧸ H.toSubgroup is monotone.

theorem TauCeti.ConvexSubgroup.quotientMk_lt_one_of_notMem {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] (H : ConvexSubgroup Γ) {a : Γ} (ha : a ≤ 1) (haH : a ∉ H) : (QuotientGroup.mk' H.toSubgroup) a < 1

An element at most 1 and outside H has class strictly below 1 in the quotient.

A height-one quotient

theorem TauCeti.ConvexSubgroup.nontrivial_quotient_maxAvoid {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] {γ : Γ} (hγ : γ ≠ 1) : Nontrivial (Γ ⧸ (maxAvoid hγ).toSubgroup)

The quotient by the largest convex subgroup avoiding γ ≠ 1 is nontrivial: the class of γ is different from 1.

Together with mulArchimedean_quotient_maxAvoid, this is the elementary ordered-group input to the fact that a valuation with a nonzero cofinal value is microbial.

theorem TauCeti.ConvexSubgroup.mulArchimedean_quotient_maxAvoid {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] {γ : Γ} (hγ : γ ≠ 1) (hclosure : closure {γ} = ⊤) : MulArchimedean (Γ ⧸ (maxAvoid hγ).toSubgroup)

If γ generates the whole group as a convex subgroup, the quotient by the largest convex subgroup avoiding γ is archimedean. Equivalently, it has height at most one.

noncomputable def TauCeti.ConvexSubgroup.quotientBotOrderIso {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] : Γ ⧸ ⊥.toSubgroup ≃*o Γ

The quotient by ⊥ is the group itself, as an ordered group. This is the reusable object of this section: it carries order-theoretic properties such as Nontrivial and MulArchimedean across the identification.

Its body is sealed. Consumers work through quotientBotOrderIso_mk and quotientBotOrderIso_symm_apply rather than by unfolding the construction, exactly as they do for quotientLinearOrder.

Equations

• TauCeti.ConvexSubgroup.quotientBotOrderIso = { toMulEquiv := TauCeti.ConvexSubgroup.quotientBotMulEquiv✝, map_le_map_iff' := ⋯ }

theorem TauCeti.ConvexSubgroup.quotientBotOrderIso_mk {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] (a : Γ) : quotientBotOrderIso ↑a = a

quotientBotOrderIso sends the class of a to a.

Deliberately not @[simp], and the same holds for every application lemma in this group. Each mentions Γ ⧸ (⊥ : ConvexSubgroup Γ).toSubgroup, and bot_toSubgroup is itself a simp lemma rewriting (⊥ : ConvexSubgroup Γ).toSubgroup to (⊥ : Subgroup Γ). So simp normalises that subterm — in the coercion's type arguments, which come from the isomorphism's own domain, not just in the argument — and a left-hand side spelled this way could never match afterwards. Marking these @[simp] would add rules that can never fire.

The normal form is not reachable either: quotientLinearOrder has head LinearOrder (Γ ⧸ ?H.toSubgroup), so synthesis cannot invert the projection and LinearOrder (Γ ⧸ (⊥ : Subgroup Γ)) does not exist — there is no ordered quotient to state the simp-normal form over. These therefore stay explicit rewrites, which is what lets consumers avoid unfolding the sealed construction.

theorem TauCeti.ConvexSubgroup.quotientBotOrderIso_symm_apply {Γ : Type u_2} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] (a : Γ) : quotientBotOrderIso.symm a = ↑a

quotientBotOrderIso.symm sends a to its class. Not @[simp]; see quotientBotOrderIso_mk.