ofLocalizationSpan_iff_finite — Mathlib

English

For any property P of ring homomorphisms, having the localization-span property is equivalent to having the localization-span-finite property.

Русский

Для любой характеристики P гомоморфизмов колец локализация-области имеет эквивалентность между свойствами Span и FiniteSpan.

LaTeX

$$$\\forall P,\\; \\RingHom.OfLocalizationSpan P \\;\\Leftrightarrow \\RingHom.OfLocalizationFiniteSpan P$$$

Lean4

theorem ofLocalizationSpan_iff_finite : RingHom.OfLocalizationSpan @P ↔ RingHom.OfLocalizationFiniteSpan @P :=
  by
  delta RingHom.OfLocalizationSpan RingHom.OfLocalizationFiniteSpan
  apply forall₅_congr
  intros
  constructor
  · intro h s; exact h s
  · intro h s hs hs'
    obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hs
    exact h s' h₂ fun x => hs' ⟨_, h₁ x.prop⟩

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