English
The family γ ↦ v.ltAddSubgroup(γ) for γ ∈ Γ₀ˣ forms a basis of open subgroups for the topology on the ring R.
Русский
Семейство γ ↦ v.ltAddSubgroup(γ) образует базис открытых подгрупп для топологии кольца R.
LaTeX
$$\text{The collection } \{ v.ltAddSubgroup(\gamma) : \gamma \in Γ₀^{\times} \} \text{ is a basis of open subgroups for } R.$$
Lean4
/-- The basis of open subgroups for the topology on a ring determined by a valuation. -/
theorem subgroups_basis : RingSubgroupsBasis fun γ : Γ₀ˣ => (v.ltAddSubgroup γ : AddSubgroup R) :=
{ inter := by
rintro γ₀ γ₁
use min γ₀ γ₁
simp only [ltAddSubgroup, Units.min_val, lt_inf_iff, le_inf_iff, AddSubgroup.mk_le_mk, AddSubmonoid.mk_le_mk,
AddSubsemigroup.mk_le_mk, setOf_subset_setOf]
tauto
mul := by
rintro γ
obtain ⟨γ₀, h⟩ := exists_square_le γ
use γ₀
rintro - ⟨r, r_in, s, s_in, rfl⟩
simp only [ltAddSubgroup, AddSubgroup.coe_set_mk, AddSubmonoid.coe_set_mk, AddSubsemigroup.coe_set_mk,
mem_setOf_eq] at r_in s_in
calc
(v (r * s) : Γ₀) = v r * v s := Valuation.map_mul _ _ _
_ < γ₀ * γ₀ := by gcongr <;> exact zero_le'
_ ≤ γ := mod_cast h
leftMul := by
rintro x γ
rcases GroupWithZero.eq_zero_or_unit (v x) with (Hx | ⟨γx, Hx⟩)
· use (1 : Γ₀ˣ)
rintro y _
change v (x * y) < _
rw [Valuation.map_mul, Hx, zero_mul]
exact Units.zero_lt γ
· use γx⁻¹ * γ
rintro y (vy_lt : v y < ↑(γx⁻¹ * γ))
change (v (x * y) : Γ₀) < γ
rw [Valuation.map_mul, Hx, mul_comm]
rw [Units.val_mul, mul_comm] at vy_lt
simpa using mul_inv_lt_of_lt_mul₀ vy_lt
rightMul := by
rintro x γ
rcases GroupWithZero.eq_zero_or_unit (v x) with (Hx | ⟨γx, Hx⟩)
· use 1
rintro y _
change v (y * x) < _
rw [Valuation.map_mul, Hx, mul_zero]
exact Units.zero_lt γ
· use γx⁻¹ * γ
rintro y (vy_lt : v y < ↑(γx⁻¹ * γ))
change (v (y * x) : Γ₀) < γ
rw [Valuation.map_mul, Hx]
rw [Units.val_mul, mul_comm] at vy_lt
simpa using mul_inv_lt_of_lt_mul₀ vy_lt }
