ofLocalizationSpanTarget — Mathlib

English

Localization at a span-generated target preserves flatness: if f is flat and P is a span-generated target, then the localized target map is flat.

Русский

Локализация целевого кольца на порциях, порожденных окном, сохраняет плоскость: если f плоское и P порождает целое, то локализованный целевой переход плоский.

LaTeX

$$$$\text{OfLocalizationSpanTarget}(Flat).$$$$

Lean4

theorem ofLocalizationSpanTarget : OfLocalizationSpanTarget Flat :=
  by
  introv R hsp h
  algebraize_only  [f]
  refine Module.flat_of_isLocalized_span _ _ s hsp _ (fun r ↦ Algebra.linearMap S <| Localization.Away r.1) ?_
  dsimp only [RingHom.Flat] at h
  convert h; ext
  apply Algebra.smul_def

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