The ideal-indexed characteristic subgroup cΓ_v(I)

Wedhorn, Adic Spaces (arXiv:1910.05934v1), §7.1, Lemmas 7.2 and 7.4 and Definition 7.3.

For a valuation v and an ideal I satisfying the standing hypothesis of §7.1 — that I has the same radical as some finitely generated ideal — Wedhorn attaches to I a convex subgroup cΓ_v(I) of the value group by a case split: it is the characteristic subgroup cΓ_v when v(I) meets it, and otherwise the greatest convex subgroup for which every value of I is cofinal. Lemma 7.2 is what makes the second branch well posed, and Lemma 7.4 characterises when cΓ_v(I) is everything — the condition that cuts out Spv (A, I).

The engine throughout is Lemma 7.1 (TauCeti.RingTheory.Valuation.CofinalIdeal.Basic): the elements whose value is cofinal form a radical ideal. Being an ideal propagates cofinality from a generating set to the ideal it spans; being radical propagates it across √I = √J. Those are the two uses Wedhorn makes of it, and both appear here.

Main definitions

• Valuation.IdealCofinalFor v H I : every element of I has value cofinal for H.
• Valuation.IdealMeetsCharacteristicSubgroup v I : v(I) meets cΓ_v, the branch condition of Definition 7.3.
• Valuation.valueSet v I : the nonzero values of v on I.
• Valuation.characteristicSubgroupOfIdeal : Definition 7.3, cΓ_v(I).

Main results

• Valuation.idealMeetsCharacteristicSubgroup_iff and Valuation.idealMeetsCharacteristicSubgroup_of_one_le : the branch condition of Definition 7.3 restated on valueSet, and the introduction rule discharging it from a value ≥ 1.

• Valuation.idealCofinalFor_iff_forall_isCofinalElement : the ideal condition is cofinality of each nonzero value as an element of the value group; vanishing values are excluded rather than constrained, since 0 is cofinal for every subgroup.

• Valuation.idealCofinalFor_of_span, Valuation.le_closure_singleton_of_idealCofinalFor and Valuation.le_of_idealCofinalFor_of_mem_valueSet : the membership, maximality and minimality halves of Lemma 7.2, with Valuation.isLeast_of_idealCofinalFor the least-element form of the last.

• Valuation.idealCofinalFor_radical_iff : cofinality depends only on the radical.

• Valuation.exists_mem_max_restrict_ne_zero : a finite spanning set contains a nonvanishing value-maximising element whenever the ideal does not vanish identically.

• Valuation.isGreatestIdealCofinal_closure_singleton_of_span : Lemma 7.2's greatest-cofinal conclusion from a generating set, with exists_isGreatestIdealCofinal_of_not_meets its existence form, which is what Definition 7.3 presupposes.

• Valuation.exists_mem_valueSet_mem_characteristicSubgroupOfIdeal and Valuation.isLeast_characteristicSubgroupOfIdeal : Lemma 7.2's attainment and minimality conclusions for cΓ_v(I) — off the first branch and with v not identically zero on I, it contains a value of I and is the least convex subgroup that does.

• Valuation.characteristicSubgroup_le_characteristicSubgroupOfIdeal : cΓ_v(I) always contains cΓ_v.

• Valuation.characteristicSubgroupOfIdeal_eq_top_iff and Valuation.characteristicSubgroupOfIdeal_eq_top_iff_forall_span : Lemma 7.4, in the all-of-I and generating-set forms.

• Valuation.characteristicSubgroupOfIdeal_eq_top_congr_of_isEquiv : that criterion is an invariant of the valuation class, which is what lets Spv (A, I) be carved out of the valuation spectrum.

Implementation notes

The §7.1 development here — Lemma 7.2's greatest-cofinal and attainment conclusions, the case split of Definition 7.3, and Lemma 7.4 — follows Wedhorn directly. The AINTLIB adic-spaces development (aintlib-adic-spaces, revision 37bbdaeb9) reaches the same section by a route that does not pass through these results: its Spv.IsInSpvAI (projects/AdicSpaces/Adic spaces/SpvAI.lean) defines Spv (A, I) by clause (ii) of Lemma 7.4, the disjunction (∀ a ∈ I, CofinalValue v a) ∨ IsMicrobial v, so it needs neither Definition 7.3's cΓ_v(I) nor Lemma 7.2's existence result, and states no Lemma 7.4. Those three are therefore without a formalised antecedent here; the equivalence between the two routes is what characteristicSubgroupOfIdeal_eq_top_iff supplies.

Two pieces do have antecedents: the convex-subgroup notion this rests on came from the same development (projects/AdicSpaces/Adic spaces/ValuationContinuity.lean, ConvexSubgroup and ConvexSubgroup.minContain) and reached this file through TauCeti.Algebra.Order.Group.ConvexSubgroup; and the cofinal-value predicate corresponds to its Valuation.CofinalValue in SpvAI.lean.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Lemma 7.1, Lemma 7.2, Definition 7.3, Lemma 7.4

def Valuation.IdealCofinalFor {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation A Γ₀) (H : TauCeti.ConvexSubgroup ↥(MonoidWithZeroHom.ofClass v).valueGroup) (I : Ideal A) : Prop

The predicate cut out by Wedhorn Lemma 7.2: every element of I has value cofinal for H.

Equations

• v.IdealCofinalFor H I = ∀ a ∈ I, v.CofinalValueFor H.toSubgroup a

theorem Valuation.idealCofinalFor_def {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {H : TauCeti.ConvexSubgroup ↥(MonoidWithZeroHom.ofClass v).valueGroup} {I : Ideal A} : v.IdealCofinalFor H I ↔ ∀ a ∈ I, v.CofinalValueFor H.toSubgroup a

The defining property of ideal-wide cofinality. Needed because the definition's body is not exposed, so consumers cannot apply IdealCofinalFor as a ∀ directly. Mirrors cofinalValueFor_def.

theorem Valuation.IdealCofinalFor.mono {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {H : TauCeti.ConvexSubgroup ↥(MonoidWithZeroHom.ofClass v).valueGroup} {I J : Ideal A} (h : v.IdealCofinalFor H J) (hIJ : I ≤ J) : v.IdealCofinalFor H I

The condition is antitone in the ideal.

theorem Valuation.idealCofinalFor_iff_le_cofinalIdeal {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {H : TauCeti.ConvexSubgroup ↥(MonoidWithZeroHom.ofClass v).valueGroup} (hH : v.characteristicSubgroup < H) {I : Ideal A} : v.IdealCofinalFor H I ↔ I ≤ v.cofinalIdeal hH

Below the strict-containment threshold, the ideal condition says exactly that I is contained in the cofinality ideal of Lemma 7.1.

def Valuation.IdealMeetsCharacteristicSubgroup {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation A Γ₀) (I : Ideal A) : Prop

The values of I meet the characteristic subgroup: the first branch of Wedhorn Definition 7.3.

Equations

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

theorem Valuation.lt_one_of_not_idealMeetsCharacteristicSubgroup {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {I : Ideal A} (hdisj : ¬v.IdealMeetsCharacteristicSubgroup I) {a : A} (haI : a ∈ I) : v a < 1

An attained value ≥ 1 always meets the characteristic subgroup — so under Wedhorn's disjointness hypothesis every element of I has value strictly below 1, the observation recorded after Lemma 7.2.

theorem Valuation.IdealCofinalFor.mono_subgroup {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {H K : TauCeti.ConvexSubgroup ↥(MonoidWithZeroHom.ofClass v).valueGroup} {I : Ideal A} (h : v.IdealCofinalFor K I) (hHK : H ≤ K) : v.IdealCofinalFor H I

The ideal condition inherits that monotonicity.

Reduction to the value set

def Valuation.valueSet {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation A Γ₀) (I : Ideal A) : Set ↥(MonoidWithZeroHom.ofClass v).valueGroup

The nonzero values attained by v on an ideal, as a subset of the value group. It carries the attainment hypothesis of Lemma 7.2 and the maximality half; note that no maximum is taken over it — Wedhorn maximises over a finite generating set, which is why the standing finite-generation hypothesis is needed at all.

Equations

• v.valueSet I = {γ : ↥(MonoidWithZeroHom.ofClass v).valueGroup | ∃ a ∈ I, v.restrict a = ↑γ}

@[simp]

theorem Valuation.mem_valueSet {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {I : Ideal A} {γ : ↥(MonoidWithZeroHom.ofClass v).valueGroup} : γ ∈ v.valueSet I ↔ ∃ a ∈ I, v.restrict a = ↑γ

theorem Valuation.idealMeetsCharacteristicSubgroup_iff {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {I : Ideal A} : v.IdealMeetsCharacteristicSubgroup I ↔ ∃ γ ∈ v.valueSet I, γ ∈ v.characteristicSubgroup

The branch condition of Definition 7.3, restated on valueSet: v(I) meets cΓ_v. The definition quantifies over ring elements, this form over the values they attain; they carry the same data through Valuation.restrict_eq_mk.

theorem Valuation.idealMeetsCharacteristicSubgroup_of_one_le {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {I : Ideal A} {a : A} (haI : a ∈ I) (ha : 1 ≤ v a) : v.IdealMeetsCharacteristicSubgroup I

An element of I with value at least 1 puts v(I) into cΓ_v. This is the positive counterpart of lt_one_of_not_idealMeetsCharacteristicSubgroup, and the introduction rule that callers use to discharge the first branch of Definition 7.3.

theorem Valuation.idealCofinalFor_iff_forall_isCofinalElement {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {H : TauCeti.ConvexSubgroup ↥(MonoidWithZeroHom.ofClass v).valueGroup} {I : Ideal A} : v.IdealCofinalFor H I ↔ ∀ γ ∈ v.valueSet I, TauCeti.IsCofinalElement H.toSubgroup γ

The bridge from the ideal to the group. An ideal is cofinal for H exactly when every one of its nonzero values is a cofinal element of the value group. The vanishing values need no condition, since 0 is cofinal for every subgroup — which is why they are excluded from valueSet rather than constrained.

The membership, maximality and minimality halves of Wedhorn Lemma 7.2

theorem Valuation.le_closure_singleton_of_idealCofinalFor {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {I : Ideal A} {K : TauCeti.ConvexSubgroup ↥(MonoidWithZeroHom.ofClass v).valueGroup} {h : ↥(MonoidWithZeroHom.ofClass v).valueGroup} (hh : h ∈ v.valueSet I) (hlt : h < 1) (hK : v.IdealCofinalFor K I) : K ≤ TauCeti.ConvexSubgroup.closure {h}

Maximality half. Any convex subgroup for which I is cofinal is contained in the one generated by a single attained value below 1. Only membership of h in the value set is needed — not that h dominates it.

theorem Valuation.le_of_idealCofinalFor_of_mem_valueSet {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {I : Ideal A} {H K : TauCeti.ConvexSubgroup ↥(MonoidWithZeroHom.ofClass v).valueGroup} (hcof : v.IdealCofinalFor H I) {γ : ↥(MonoidWithZeroHom.ofClass v).valueGroup} (hγ : γ ∈ v.valueSet I) (hγK : γ ∈ K) : H ≤ K

Minimality half. A convex subgroup for which I is cofinal sits below every convex subgroup containing so much as one value of I. No domination hypothesis is needed.

theorem Valuation.isLeast_of_idealCofinalFor {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {I : Ideal A} {H : TauCeti.ConvexSubgroup ↥(MonoidWithZeroHom.ofClass v).valueGroup} (hcof : v.IdealCofinalFor H I) (hmeet : ∃ γ ∈ v.valueSet I, γ ∈ H) : IsLeast {K : TauCeti.ConvexSubgroup ↥(MonoidWithZeroHom.ofClass v).valueGroup | ∃ γ ∈ v.valueSet I, γ ∈ K} H

Minimality, as a least-element statement. Any convex subgroup for which I is cofinal and which contains a value of I is the least convex subgroup meeting v(I).

theorem Valuation.idealCofinalFor_of_span {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {H : TauCeti.ConvexSubgroup ↥(MonoidWithZeroHom.ofClass v).valueGroup} (hH : v.characteristicSubgroup < H) {T : Set A} {I : Ideal A} (hspan : Ideal.span T = I) (hT : ∀ t ∈ T, v.CofinalValueFor H.toSubgroup t) : v.IdealCofinalFor H I

Membership half. It suffices to check cofinality on a generating set: if every element of T has cofinal value, so does every element of the ideal T spans.

Note what this does not say: the values on I need not be bounded by the values on T, since v (c * t) = v c * v t can exceed v t when 1 < v c. The hypothesis constrains the generators only, not the ideal's values.

theorem Valuation.isGreatestIdealCofinal_top_of_forall_eq_zero {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {I : Ideal A} (h : ∀ a ∈ I, (MonoidWithZeroHom.ofClass v) a = 0) : IsGreatest {K : TauCeti.ConvexSubgroup ↥(MonoidWithZeroHom.ofClass v).valueGroup | v.IdealCofinalFor K I} ⊤

If v vanishes on the whole of I then every convex subgroup works, so the greatest one is ⊤. This is Wedhorn's "if v(I) = {0}, we may choose H = Γv".

Reduction along the radical

From here commutativity is needed: the radical of an ideal is Mathlib's Ideal.radical, which is defined over a commutative semiring. Everything above needs only a ring.

theorem Valuation.idealCofinalFor_radical_iff {A : Type u_3} [CommRing A] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {H : TauCeti.ConvexSubgroup ↥(MonoidWithZeroHom.ofClass v).valueGroup} (hH : v.characteristicSubgroup < H) {I : Ideal A} : v.IdealCofinalFor H I.radical ↔ v.IdealCofinalFor H I

Cofinality of an ideal depends only on its radical. This is what allows I to be replaced by a finitely generated ideal with the same radical — the standing hypothesis of §7.1.

theorem Valuation.idealCofinalFor_congr_of_radical_eq {A : Type u_3} [CommRing A] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {H : TauCeti.ConvexSubgroup ↥(MonoidWithZeroHom.ofClass v).valueGroup} (hH : v.characteristicSubgroup < H) {I J : Ideal A} (hIJ : I.radical = J.radical) : v.IdealCofinalFor H I ↔ v.IdealCofinalFor H J

Two ideals with the same radical are cofinal for exactly the same convex subgroups.

Assembling Lemma 7.2's greatest-cofinal conclusion

theorem Valuation.isGreatestIdealCofinal_closure_singleton_of_span {A : Type u_3} [CommRing A] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {I J : Ideal A} {T : Set A} {h : ↥(MonoidWithZeroHom.ofClass v).valueGroup} {n : ℕ} (hH : v.characteristicSubgroup < TauCeti.ConvexSubgroup.closure {h}) (hspan : Ideal.span T = J) (hrad : I.radical = J.radical) (hlt : h < 1) (hn : n ≠ 0) (hdom : ∀ t ∈ T, v.restrict t ≤ ↑h) (hatt : h ^ n ∈ v.valueSet I) : IsGreatest {K : TauCeti.ConvexSubgroup ↥(MonoidWithZeroHom.ofClass v).valueGroup | v.IdealCofinalFor K I} (TauCeti.ConvexSubgroup.closure {h})

Wedhorn Lemma 7.2, in the form the standing hypothesis of §7.1 supplies it.

Given a generating set T of an ideal J with the same radical as I, and a value h < 1 dominating the values on T and attained (up to a power) on I, the convex subgroup generated by h is the greatest one for which I is cofinal.

Domination is stated on ValueGroup₀, so generators lying in the support are allowed: a vanishing value is cofinal for free. Attainment is required only up to a power, because h lives on J rather than on I.

theorem Valuation.exists_mem_max_restrict_ne_zero {A : Type u_3} [CommRing A] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {I J : Ideal A} {T : Finset A} (hT : Ideal.span ↑T = J) (hrad : I.radical = J.radical) {a₀ : A} (ha₀I : a₀ ∈ I) (ha₀0 : (MonoidWithZeroHom.ofClass v) a₀ ≠ 0) : ∃ t₀ ∈ T, (MonoidWithZeroHom.ofClass v) t₀ ≠ 0 ∧ ∀ t ∈ T, v.restrict t ≤ v.restrict t₀

A generator of greatest value, not in the support. If I and Ideal.span T have the same radical and v does not vanish identically on I, then some t₀ ∈ T maximises v.restrict over T and has v t₀ ≠ 0.

Nonvanishing is what needs the radical hypothesis: were every generator in the support, so would be everything of I, contradicting the witness. Maximality is then Finset.exists_max_image, and the maximiser inherits nonvanishing because it dominates every generator.

theorem Valuation.exists_isGreatestIdealCofinal_of_not_meets {A : Type u_3} [CommRing A] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {I : Ideal A} (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) (hdisj : ¬v.IdealMeetsCharacteristicSubgroup I) : ∃ (H : TauCeti.ConvexSubgroup ↥(MonoidWithZeroHom.ofClass v).valueGroup), IsGreatest {K : TauCeti.ConvexSubgroup ↥(MonoidWithZeroHom.ofClass v).valueGroup | v.IdealCofinalFor K I} H ∧ v.characteristicSubgroup ≤ H ∧ ((∃ a ∈ I, (MonoidWithZeroHom.ofClass v) a ≠ 0) → ∃ γ ∈ v.valueSet I, γ ∈ H)

Wedhorn Lemma 7.2's greatest-cofinal conclusion, as Definition 7.3 uses it. Only the standing hypothesis of §7.1 and the disjointness v(I) ∩ cΓ_v = ∅ are needed: the case where v vanishes identically on I is covered separately by ⊤.

The last conjunct — that the subgroup meets v(I) — is guarded by the nonvanishing hypothesis rather than asserted outright, because it is false in the ⊤ branch: there valueSet v I is empty, so no subgroup whatever meets it.

Wedhorn Definition 7.3

noncomputable def Valuation.characteristicSubgroupOfIdeal {A : Type u_3} [CommRing A] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation A Γ₀) (I : Ideal A) (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) : TauCeti.ConvexSubgroup ↥(MonoidWithZeroHom.ofClass v).valueGroup

Wedhorn Definition 7.3: cΓ_v(I). It is cΓ_v when v(I) meets the characteristic subgroup, and otherwise the greatest convex subgroup for which every value of I is cofinal — which exists by Lemma 7.2, and is why the standing hypothesis of §7.1 is carried here.

Note that this is a case split, not the convex subgroup generated by cΓ_v together with v(I); those differ.

Equations

• v.characteristicSubgroupOfIdeal I hfg = if h : v.IdealMeetsCharacteristicSubgroup I then v.characteristicSubgroup else ⋯.choose

@[simp]

theorem Valuation.characteristicSubgroupOfIdeal_of_meets {A : Type u_3} [CommRing A] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {I : Ideal A} (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) (h : v.IdealMeetsCharacteristicSubgroup I) : v.characteristicSubgroupOfIdeal I hfg = v.characteristicSubgroup

First branch of Definition 7.3.

theorem Valuation.isGreatestIdealCofinal_characteristicSubgroupOfIdeal {A : Type u_3} [CommRing A] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {I : Ideal A} (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) (h : ¬v.IdealMeetsCharacteristicSubgroup I) : IsGreatest {K : TauCeti.ConvexSubgroup ↥(MonoidWithZeroHom.ofClass v).valueGroup | v.IdealCofinalFor K I} (v.characteristicSubgroupOfIdeal I hfg)

Second branch of Definition 7.3: off the first branch, cΓ_v(I) really is the greatest convex subgroup for which I is cofinal.

theorem Valuation.characteristicSubgroup_le_characteristicSubgroupOfIdeal {A : Type u_3} [CommRing A] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation A Γ₀) (I : Ideal A) (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) : v.characteristicSubgroup ≤ v.characteristicSubgroupOfIdeal I hfg

cΓ_v(I) always contains cΓ_v — the sentence Wedhorn records immediately after Definition 7.3.

theorem Valuation.exists_mem_valueSet_mem_characteristicSubgroupOfIdeal {A : Type u_3} [CommRing A] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {I : Ideal A} (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) (h : ¬v.IdealMeetsCharacteristicSubgroup I) (hne : ∃ a ∈ I, (MonoidWithZeroHom.ofClass v) a ≠ 0) : ∃ γ ∈ v.valueSet I, γ ∈ v.characteristicSubgroupOfIdeal I hfg

cΓ_v(I) meets v(I) — the attainment half of Wedhorn Lemma 7.2, on the branch where Definition 7.3 invokes it: some value of I lies in cΓ_v(I).

Nonvanishing cannot be dropped: if v vanishes identically on I then valueSet v I is empty and nothing meets it.

theorem Valuation.isLeast_characteristicSubgroupOfIdeal {A : Type u_3} [CommRing A] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {I : Ideal A} (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) (h : ¬v.IdealMeetsCharacteristicSubgroup I) (hne : ∃ a ∈ I, (MonoidWithZeroHom.ofClass v) a ≠ 0) : IsLeast {K : TauCeti.ConvexSubgroup ↥(MonoidWithZeroHom.ofClass v).valueGroup | ∃ γ ∈ v.valueSet I, γ ∈ K} (v.characteristicSubgroupOfIdeal I hfg)

cΓ_v(I) is the least convex subgroup meeting v(I) — the minimality conclusion of Wedhorn Lemma 7.2, on the branch where Definition 7.3 invokes it.

Nonvanishing cannot be dropped: with valueSet v I empty nothing meets it, so the set has no least element.

Wedhorn Lemma 7.4

theorem Valuation.characteristicSubgroupOfIdeal_eq_top_iff {A : Type u_3} [CommRing A] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {I : Ideal A} (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) : v.characteristicSubgroupOfIdeal I hfg = ⊤ ↔ (∀ a ∈ I, v.CofinalValue a) ∨ v.characteristicSubgroup = ⊤

Wedhorn Lemma 7.4, (i) ⟺ (ii). cΓ_v(I) = Γ_v exactly when either every value of I is cofinal for the whole value group, or Γ_v = cΓ_v already.

The disjuncts are not exclusive: when v(I) meets cΓ_v, the left one implies the right.

theorem Valuation.characteristicSubgroupOfIdeal_eq_top_iff_forall_span {A : Type u_3} [CommRing A] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} {I : Ideal A} (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) {J : Ideal A} {T : Set A} (hspan : Ideal.span T = J) (hrad : I.radical = J.radical) : v.characteristicSubgroupOfIdeal I hfg = ⊤ ↔ (∀ t ∈ T, v.CofinalValue t) ∨ v.characteristicSubgroup = ⊤

Wedhorn Lemma 7.4, (i) ⟺ (iii). Clause (iii) checks cofinality only on a generating set T of any ideal with the same radical — the form the Spv (A, I) development uses, since it turns a condition on all of I into a condition on generators. (T carries no finiteness hypothesis here; finiteness comes from the standing hypothesis of §7.1 when the caller supplies a finitely generated J.)

The generating set may be taken for any ideal J sharing a radical with I, not for I itself.

theorem Valuation.characteristicSubgroupOfIdeal_eq_top_congr_of_isEquiv {A : Type u_3} [CommRing A] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] {Γ₀' : Type u_5} [LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation A Γ₀} {w : Valuation A Γ₀'} (h : v.IsEquiv w) {I : Ideal A} (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) : v.characteristicSubgroupOfIdeal I hfg = ⊤ ↔ w.characteristicSubgroupOfIdeal I hfg = ⊤

The Spv (A, I) criterion is an invariant of the valuation class. This is what lets Spv (A, I) be carved out of Spv A, whose points are equivalence classes.

Note that it is the criterion that transports, not cΓ_v(I) itself: equivalent valuations have different value groups, so their ideal-indexed subgroups are not comparable.