finitePresentation_ofLocalizationSpanTarget

English

Finite presentation can be checked on a localization span target: if localizations at a spanning set are FP, then the whole is FP.

Русский

Конечное презентование можно проверить по локализациям, образующим охват целевого кольца: если локализации по охвату FP, значит и всё кольцо FP.

LaTeX

$$$\text{If } s \subset S \text{ spans top, and each } \operatorname{Localization.Away}(s) \text{ is FP, then } S \text{ is FP.}$$$

Lean4

/-- Finite-presentation can be checked on a standard covering of the target. -/
theorem finitePresentation_ofLocalizationSpanTarget : OfLocalizationSpanTarget @FinitePresentation :=
  by
  introv R hs H
  algebraize [f]
  replace H : ∀ r ∈ s, Algebra.FinitePresentation R (Localization.Away (r : S)) :=
    by
    intro r hr; simp_rw [RingHom.FinitePresentation] at H; convert H ⟨r, hr⟩; ext
    simp_rw [Algebra.smul_def]; rfl
  exact Algebra.FinitePresentation.of_span_eq_top_target s hs H

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