generalizingMap — Mathlib

English

Every flat morphism is generalizing on the base.

Русский

Каждый плоский морфизм является обобщающим на основании.

LaTeX

$$$[\text{Flat}(f)] \Rightarrow \text{GeneralizingMap}(f.base).$$$

Lean4

/-- Any flat morphism is generalizing. -/
theorem generalizingMap [Flat f] : GeneralizingMap f.base :=
  by
  have := HasRingHomProperty.of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget.{u} (topologically GeneralizingMap)
  change topologically GeneralizingMap f
  rw [HasRingHomProperty.iff_appLE (P := topologically GeneralizingMap)]
  intro U V e
  algebraize [(f.appLE U V e).hom]
  apply Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap.mp
  convert Algebra.HasGoingDown.of_flat
  exact HasRingHomProperty.appLE (@Flat) f ‹_› U V e

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