Cofinal elements of an ordered group

Cofinality following Wedhorn, Adic Spaces (arXiv:1910.05934v1), §1.4: an element is cofinal for a subgroup if its powers eventually fall below every member. The definition needs only a group with a strict order; the results relating cofinality to convex subgroups are stated for linearly ordered commutative groups. This is the order-theoretic input to the continuity criterion for valuations (Wedhorn §7.2) and the retraction r_I : Spv A → Spv(A, I) of §7.1.2.

Main definitions

• TauCeti.IsCofinalElement H γ : Powers of γ fall below every member of H (Wedhorn Definition 1.16). Unlike Mathlib's IsCofinal, which describes a set that is cofinal for the ambient order with respect to ≤, this is a property of an element with respect to the strict order, following Wedhorn.

Main results

• TauCeti.IsCofinalElement.comap : Cofinality transports backwards through an ordered monoid isomorphism.
• TauCeti.isCofinalElement_iff_subset_closure : For γ < 1, γ is cofinal for H iff the convex subgroup generated by γ contains H (Wedhorn Remark 1.19).
• TauCeti.IsCofinalElement.mul_of_lt_of_mem : Cofinal elements may be perturbed by members of any strictly smaller convex subgroup (Wedhorn Proposition 1.20).
• TauCeti.isGreatest_convexSubgroup_isCofinalElement : If a set of elements below 1 has a greatest element h, the convex subgroup generated by h is the greatest one for which every member of the set is cofinal (the order-theoretic content of Wedhorn Lemma 7.2).
• TauCeti.IsCofinalElement.quotientMk : A cofinal element stays cofinal in the quotient by a proper convex subgroup (Wedhorn Corollary 1.21).

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Definition 1.16, Remark 1.19, Proposition 1.20, Corollary 1.21, Lemma 7.2

Adapted from the AINTLIB development (Apache 2.0), file projects/AdicSpaces/Adic spaces/OrderedGroupConvex.lean (the cofinality half; its convex-subgroup half is the parent module), with the predicate restated over subgroups as in Wedhorn's Definition 1.16.

Cofinal elements

def TauCeti.IsCofinalElement {Γ : Type u_1} [Group Γ] [LT Γ] (H : Subgroup Γ) (γ : Γ) : Prop

An element γ is cofinal for the subgroup H if every member of H eventually dominates the powers of γ: ∀ h ∈ H, ∃ n, γ ^ n < h. This is the γ ∈ Γ case of Wedhorn Definition 1.16, which takes H to be any subgroup and lets the base range over Γ ∪ {0}; the adjoined base 0 is cofinal for every subgroup trivially, and the vanishing-base case belongs with the valuation-side theory, over a value group with zero, rather than here. Membership of γ in H is not required. Distinct from Mathlib's IsCofinal, a property of sets with respect to ≤.

Equations

• TauCeti.IsCofinalElement H γ = ∀ h ∈ H, ∃ (n : ℕ), γ ^ n < h

theorem TauCeti.isCofinalElement_def {Γ : Type u_1} [Group Γ] [LT Γ] {H : Subgroup Γ} {γ : Γ} : IsCofinalElement H γ ↔ ∀ h ∈ H, ∃ (n : ℕ), γ ^ n < h

The defining property of a cofinal element.

Deliberately not @[simp]: the right-hand side is the unfolded bounded quantifier, so tagging it rewrites uses of the named predicate into raw ∀ … ∃ … form. This mirrors Valuation.cofinalValueFor_def, which is not @[simp] for the same reason.

theorem TauCeti.IsCofinalElement.comap {Γ : Type u_2} {Γ' : Type u_1} [Group Γ] [Preorder Γ] [Group Γ'] [Preorder Γ'] {H : Subgroup Γ'} {γ : Γ} {e : Γ ≃*o Γ'} (hγ : IsCofinalElement H (e γ)) : IsCofinalElement (Subgroup.comap e.toMonoidHom H) γ

Cofinality transports backwards through an ordered monoid isomorphism, with the subgroup pulled back along the same isomorphism.

theorem TauCeti.IsCofinalElement.lt_one {Γ : Type u_1} [Group Γ] [LinearOrder Γ] [MulLeftMono Γ] {H : Subgroup Γ} {γ : Γ} (hγ : IsCofinalElement H γ) : γ < 1

No element ≥ 1 is cofinal for any subgroup (Wedhorn's remark after Definition 1.16): a cofinal element lies strictly below 1.

theorem TauCeti.isCofinalElement_iff_subset_closure {Γ : Type u_1} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] {H : Subgroup Γ} {γ : Γ} (hγ1 : γ < 1) : IsCofinalElement H γ ↔ ↑H ⊆ ↑(ConvexSubgroup.closure {γ})

Wedhorn Remark 1.19. For γ < 1, the element γ is cofinal for H iff the convex subgroup generated by γ contains H.

theorem TauCeti.IsCofinalElement.mul_of_lt_of_mem {Γ : Type u_1} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] {Γ' Δ : ConvexSubgroup Γ} {γ : Γ} (hγ : IsCofinalElement Γ'.toSubgroup γ) (hlt : Δ < Γ') {δ : Γ} (hδ : δ ∈ Δ) : IsCofinalElement Γ'.toSubgroup (δ * γ)

Wedhorn Proposition 1.20. If γ is cofinal for the convex subgroup Γ' and Δ < Γ' is a strictly smaller convex subgroup, then δ * γ is cofinal for Γ' for every δ ∈ Δ.

theorem TauCeti.isGreatest_convexSubgroup_isCofinalElement {Γ : Type u_1} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] {S : Set Γ} {h : Γ} (hh : IsGreatest S h) (hlt : h < 1) : IsGreatest {K : ConvexSubgroup Γ | ∀ γ ∈ S, IsCofinalElement K.toSubgroup γ} (ConvexSubgroup.closure {h})

The greatest convex subgroup with a prescribed cofinal set. If a set S of elements below 1 has a greatest element h, then the convex subgroups for which every member of S is cofinal are exactly those contained in the one generated by h, so that subgroup is the greatest of them.

Note the inversion: below 1 a smaller element generates a larger convex subgroup, so the greatest element of S yields the smallest of the generated subgroups, and it is that one which every member of S is cofinal for. This is the order-theoretic content of Wedhorn Lemma 7.2, where S is the set of values of a finite generating set of an ideal and h is the largest of them.

Cofinality in a quotient

theorem TauCeti.IsCofinalElement.quotientMk {Γ : Type u_1} [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ] {Δ : ConvexSubgroup Γ} (hΔ : Δ ≠ ⊤) {γ : Γ} (hγ : IsCofinalElement ⊤ γ) : IsCofinalElement ⊤ ((QuotientGroup.mk' Δ.toSubgroup) γ)

Wedhorn Corollary 1.21. A cofinal element stays cofinal in the quotient by a proper convex subgroup: if γ is cofinal for Γ and Δ ≠ ⊤, the class of γ is cofinal for Γ ⧸ Δ.

Properness is not a convenience hypothesis. For Δ = ⊤ the quotient is trivial, and the only element of a trivial group is 1, which is cofinal for nothing.

This is the order-theoretic core of Wedhorn Remark 7.11(2), which reads it as saying that a vertical generization v / H of a continuous valuation is again continuous.