finiteType_ofLocalizationSpanTarget

English

Finite presentation can be checked on a standard covering of the target as in the SpanTarget criterion.

Русский

Конечное презентование можно проверить по стандартному покрытию цели как в критерии SpanTarget.

LaTeX

$$$\text{OfLocalizationSpanTarget }\operatorname{FiniteType}$$$

Lean4

theorem finiteType_ofLocalizationSpanTarget : OfLocalizationSpanTarget @FiniteType :=
  by
  introv R hs H
  algebraize [f]
  replace H : ∀ r ∈ s, Algebra.FiniteType R (Localization.Away (r : S)) :=
    by
    intro r hr; simp_rw [RingHom.FiniteType] at H; convert H ⟨r, hr⟩; ext
    simp_rw [Algebra.smul_def]; rfl
  exact Algebra.FiniteType.of_span_eq_top_target s hs H

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