ofLocalizationSpanTarget_iff_finite

English

Similarly, the span target version yields an equivalence with its finite-span-target counterpart for localization properties.

Русский

Аналогично, версия со SpanTarget эквивалентна своей конечной версии для локализаций.

LaTeX

$$$\\forall P,\\; \\RingHom.OfLocalizationSpanTarget P \\;\\Leftrightarrow \\RingHom.OfLocalizationFiniteSpanTarget P$$$

Lean4

theorem ofLocalizationSpanTarget_iff_finite :
    RingHom.OfLocalizationSpanTarget @P ↔ RingHom.OfLocalizationFiniteSpanTarget @P :=
  by
  delta RingHom.OfLocalizationSpanTarget RingHom.OfLocalizationFiniteSpanTarget
  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⟩

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