exists_factor_valuationRing — Mathlib

English

For a local ring map f: R → K there exist a valuation subring A of K and a relation h so that the codomain restriction is local.

Русский

Для локального кольцевого отображения f: R → K существует оценочное подкольцо A ⊆ K и отношение h, чтобы ограничение кодомонора было локальным.

LaTeX

$$$\\exists A:\\mathrm{ValuationSubring}(K), \\; \\exists h, \\; \\text{IsLocalHom}(f^{\\mathrm{codRestrict}})$.$$

Lean4

theorem exists_factor_valuationRing [IsLocalRing R] (f : R →+* K) :
    ∃ (A : ValuationSubring K) (h : _), IsLocalHom (f.codRestrict A.toSubring h) :=
  by
  obtain ⟨B, hB⟩ := (LocalSubring.range f).exists_le_valuationSubring
  refine ⟨B, fun x ↦ hB.1 ⟨x, rfl⟩, ?_⟩
  exact @RingHom.isLocalHom_comp _ _ _ _ _ _ _ _ hB.2 (.of_surjective _ f.rangeRestrict_surjective)

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