ofComapInteger — Mathlib

English

The comap of the valuations preserves integer membership when comparing two valuations with a comap map.

Русский

Сохранение целочисленности при сопоставлении двух оценок через сопоставление.

LaTeX

$$$ Subring.comap (algebraMap K A) vA.integer = vK.integer $$$

Lean4

/-- When `K` is a field, if the preimage of the valuation integers of `A` equals to the valuation
integers of `K`, then the valuation on `A` is an extension of the valuation on `K`.
-/
theorem ofComapInteger (h : vA.integer.comap (algebraMap K A) = vK.integer) : vK.HasExtension vA where
  val_isEquiv_comap := by
    rw [isEquiv_iff_val_le_one]
    intro x
    simp_rw [← Valuation.mem_integer_iff, ← h, Subring.mem_comap, mem_integer_iff, comap_apply]

Похожие утверждения