Adic Spaces — Lean blueprint

3. Convex subgroups and coarsening of valuations🔗

Definition3.1
uses 0
Used by 3
Reverse dependency previews
Preview
Definition 3.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A subgroup H of a linearly ordered commutative group \Gamma is convex if a, b \in H and a \le x \le b force x \in H. In Adic-Spaces this is the structure \texttt{ConvexSubgroup}, and \texttt{minContain}\,S is the smallest convex subgroup containing a set S. Convex subgroups of the value group control the coarsenings of a valuation. Following Wedhorn §7.1.

Lean code for Definition3.1●2 definitions
  • structure(extends 3, 5 fields)defined in «Adic spaces»/OrderedGroupConvex.lean
    complete
    structure ConvexSubgroup.{u_1} (Γ : Type u_1) [CommGroup Γ] [LinearOrder Γ] :
  Type u_1
    structure ConvexSubgroup.{u_1} (Γ : Type u_1)
  [CommGroup Γ] [LinearOrder Γ] : Type u_1
    A **convex subgroup** of a linearly ordered commutative group `Γ` is a subgroup
that is order-convex: if `a ≤ x ≤ b` and `a, b ∈ H`, then `x ∈ H`.

    Extends

    • Subgroup Γ

    Fields

    carrier : Set Γ
    Inherited from
    1. Subgroup
    2. Submonoid
    3. Subsemigroup
    mul_mem' : ∀ {a b : Γ}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
    Inherited from
    1. Subgroup
    2. Submonoid
    3. Subsemigroup
    one_mem' : 1 ∈ self.carrier
    Inherited from
    1. Subgroup
    2. Submonoid
    inv_mem' : ∀ {x : Γ}, x ∈ self.carrier → x⁻¹ ∈ self.carrier
    Inherited from
    1. Subgroup
    convex' : ∀ {a b x : Γ}, a ∈ self.carrier → b ∈ self.carrier → a ≤ x → x ≤ b → x ∈ self.carrier
  • defdefined in «Adic spaces»/OrderedGroupConvex.lean
    complete
    def ConvexSubgroup.minContain.{u_1} {Γ : Type u_1} [CommGroup Γ]
  [LinearOrder Γ] (S : Set Γ) : ConvexSubgroup Γ
    def ConvexSubgroup.minContain.{u_1}
  {Γ : Type u_1} [CommGroup Γ]
  [LinearOrder Γ] (S : Set Γ) :
  ConvexSubgroup Γ
    **Convex subgroup generated by a set.** The smallest convex subgroup of `Γ`
containing every element of `S`. Defined as the intersection of all convex
subgroups containing `S`.

This is the universal "containing" construction dual to `maxAvoid` (which is
the largest convex subgroup *avoiding* a single element). For our use, this
underwrites `cΓ_v(I)` from Wedhorn 7.3: the smallest convex subgroup
generated by `{v(a) : v(a) ≥ 1, a ∈ A} ∪ {v(b)⁻¹ : b ∈ I, v(b) > 0}`.
Definition3.2
uses 1used by 0✓L∃∀N

The coarsening of a valuation v : R \to \Gamma_0 by a convex subgroup H (Definition 3.1) is the composite R \xrightarrow{v} \Gamma_0 \xrightarrow{\pi} (\Gamma/H)_0 with the quotient projection. Coarser valuations have the same support but a smaller value group; passing to a maximal proper convex subgroup gives a height-one (rank-one) coarsening. In Adic-Spaces: \texttt{Valuation.coarsen}. Following Wedhorn §7.1.

Lean code for Definition3.2●1 definition
  • defdefined in «Adic spaces»/ValuationCoarsening.lean
    complete
    def Valuation.coarsen.{u_1, u_2} {R : Type u_1} [CommRing R] {Γ : Type u_2}
  [CommGroup Γ] [LinearOrder Γ] [IsOrderedMonoid Γ]
  (v : Valuation R (WithZero Γ)) (H : ConvexSubgroup Γ) :
  Valuation R (WithZero (Γ ⧸ H.toSubgroup))
    def Valuation.coarsen.{u_1, u_2}
  {R : Type u_1} [CommRing R]
  {Γ : Type u_2} [CommGroup Γ]
  [LinearOrder Γ] [IsOrderedMonoid Γ]
  (v : Valuation R (WithZero Γ))
  (H : ConvexSubgroup Γ) :
  Valuation R
    (WithZero (Γ ⧸ H.toSubgroup))
    **Coarsening** of a valuation by a convex subgroup `H` of its value group.
The coarsened valuation is the composition `R →ᵥ Γ₀ →π (Γ/H)₀` where `π` is the
quotient projection (§7.1 of Wedhorn).
Definition3.3
uses 1used by 0✓L∃∀N

For a valuation v and an ideal I Wedhorn singles out the convex subgroup c\Gamma_v generated by the values \ge 1 attained by v (\texttt{imageGeOne}), relative to I packaged as \texttt{cGammaIdeal}. This characteristic subgroup records the "microbial" part of the value group and is the technical device behind the \mathrm{Spv}(A,I) description of continuity (Definition 3.1). Following Wedhorn Definition 4.13.

Lean code for Definition3.3●2 definitions
  • defdefined in «Adic spaces»/CharacteristicSubgroup.lean
    complete
    def Valuation.cGammaIdeal.{u_1, u_2} {A : Type u_1} [CommRing A]
  {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀]
  (v : Valuation A Γ₀) (I : Ideal A) : ConvexSubgroup Γ₀ˣ
    def Valuation.cGammaIdeal.{u_1, u_2}
  {A : Type u_1} [CommRing A]
  {Γ₀ : Type u_2}
  [LinearOrderedCommGroupWithZero Γ₀]
  (v : Valuation A Γ₀) (I : Ideal A) :
  ConvexSubgroup Γ₀ˣ
    **Wedhorn 7.3: the convex subgroup `cΓ_v(I)`.** This is the smallest
convex subgroup of `Γ₀ˣ` containing the generators of `cGammaIdealUnits v I`,
constructed via `ConvexSubgroup.minContain`.

By construction:
* Every element of `cGammaIdealUnits v I` lies in `cGammaIdeal v I`
  (`subset_minContain`).
* `cGammaIdeal v I` is the smallest convex subgroup with this property
  (`minContain_le`).

Per Wedhorn 7.3, this captures "the convex subgroup making `v` continuous
in `Spv(A, I)`".
  • defdefined in «Adic spaces»/CharacteristicSubgroup.lean
    complete
    def Valuation.imageGeOne.{u_1, u_2} {A : Type u_1} [CommRing A]
  {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀]
  (v : Valuation A Γ₀) : Set Γ₀
    def Valuation.imageGeOne.{u_1, u_2}
  {A : Type u_1} [CommRing A]
  {Γ₀ : Type u_2}
  [LinearOrderedCommGroupWithZero Γ₀]
  (v : Valuation A Γ₀) : Set Γ₀
    The set `Γ_{v,≥1} ∩ im(v)` from Wedhorn 4.13 — values `≥ 1` that
are reached by `v`.