Documentation

TauCeti.RingTheory.Valuation.Microbial

Microbial valuations #

Wedhorn's Definition 5.46(v) calls a valuation microbial when some convex subgroup of its value group has height-one quotient. This module records that condition.

What consumes it is the coarsening Valuation.coarsenByUnits of TauCeti/RingTheory/Valuation/Coarsen.lean, which is the vertical generization v/H of Wedhorn's Remark 4.12(1): the subgroup a microbial valuation supplies is exactly the one to coarsen by. That direction of use is downstream, so this module does not import the coarsening.

Height one, without a height theory #

"Height one" is not formalised as a number. A linearly ordered commutative group has height at most one exactly when its only convex subgroups are ⊥ and ⊤, and that is TauCeti.ConvexSubgroup.mulArchimedean_iff_forall_eq_bot_or_eq_top; height exactly one adds that the group is not trivial. So MulArchimedean together with Nontrivial is the height-one condition, and no rank or height development is needed.

Main definitions #

Main results #

Implementation notes #

Declared in the root Valuation namespace, not in TauCeti.Valuation, matching TauCeti/RingTheory/Valuation/Coarsen.lean. Valuation is a Mathlib type, so nesting it under TauCeti shadows it and dot-notation on a valuation stops elaborating; the repository's dot-notation guard rejects that.

The condition is stated over (v.ValueGroup₀)ˣ, the units of the value monoid v actually attains, which is Wedhorn's Γ_v. It is deliberately not stated over the ambient Γ₀ˣ: that reading depends only on the codomain and not on v, so a trivial valuation into a large enough Γ₀ would satisfy it while its own value group is trivial, hence not of height one.

Spelling Γ_v as (v.ValueGroup₀)ˣ rather than as v.valueGroup is what makes the witness directly usable. The two are identified by OrderMonoidIso.unitsWithZero, but only the former is a LinearOrderedCommGroupWithZero's unit group, so only it carries the ordered-monoid instances that ConvexSubgroup's quotient order needs; and it is exactly what Valuation.restrict takes values in, so the subgroup the definition supplies is the one the coarsening consumes, with no transport in between.

The characteristic subgroup cΓ_v of Wedhorn 4.13 is a different notion and lives in TauCeti/RingTheory/Valuation/CharacteristicGroup.lean, which says so explicitly.

References #

source
def Valuation.IsMicrobial {R : Type u_1} [Ring R] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) :
Prop

Wedhorn Definition 5.46(v): v is microbial when some convex subgroup H of its value group Γ_v has height-one quotient — nontrivial, and archimedean in the sense that ⊥ and ⊤ are its only convex subgroups.

Stated over (v.ValueGroup₀)ˣ, the values v actually attains, and not over the ambient Γ₀ˣ: the latter does not mention v, so a trivial valuation into a large enough Γ₀ would satisfy it although its own value group is trivial, hence not of height one.

Equations
Instances For
    source
    theorem Valuation.isMicrobial_iff {R : Type u_1} [Ring R] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} :
    v.IsMicrobial ↔ ∃ (H : TauCeti.ConvexSubgroup (↑v).ValueGroup₀ˣ), Nontrivial ((↑v).ValueGroup₀ˣ ⧸ H.toSubgroup) ∧ MulArchimedean ((↑v).ValueGroup₀ˣ ⧸ H.toSubgroup)

    The characteristic lemma for IsMicrobial: it is exactly its defining existential, so a consumer can obtain the convex subgroup from it, or supply one to build it, without unfolding the predicate. Since IsMicrobial is sealed, this is the whole of its introduction and elimination interface outside this module.

    Deliberately not @[simp]: the right-hand side is the strictly larger term, so rewriting in this direction takes a named predicate out of normal form rather than into it.

    source
    theorem Valuation.isMicrobial_of_cofinalValue {R : Type u_1} [Ring R] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} {b : R} (hb0 : v b ≠ 0) (hcof : v.CofinalValue b) :
    v.IsMicrobial

    A valuation with a nonzero cofinal value is microbial: the largest convex subgroup avoiding the corresponding value-group unit has nontrivial archimedean quotient.

    source
    theorem Valuation.not_isMicrobial_of_subsingleton {R : Type u_1} [Ring R] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} (h : Subsingleton (↑v).ValueGroup₀ˣ) :
    ¬v.IsMicrobial

    A valuation whose value group is trivial is not microbial. The definition is therefore not vacuously satisfied: it genuinely constrains v.

    This is the degenerate case that distinguishes IsMicrobial from the condition read on the ambient Γ₀ˣ, which a trivial valuation into a large enough Γ₀ would satisfy.

    source
    theorem Valuation.isMicrobial_of_mulArchimedean {R : Type u_1} [Ring R] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} [Nontrivial (↑v).ValueGroup₀ˣ] [MulArchimedean (↑v).ValueGroup₀ˣ] :
    v.IsMicrobial

    A rank-one valuation is microbial, witnessed by H = ⊥. "Rank one" is Γ_v nontrivial and archimedean, exactly as in the module docstring, so the quotient Γ_v ⧸ ⊥ ≃ Γ_v already has height one and no proper convex subgroup is needed.

    With not_isMicrobial_of_subsingleton this pins the predicate from both sides: it holds of every rank-one valuation and fails of every trivial one.