iff_flat_and_comap_surjective — Mathlib

English

FaithfullyFlat is equivalent to flatness plus surjectivity of the comap map.

Русский

FaithfullyFlat эквивалентен плоскости, дополнительно с сюръективностью отображения specComap.

LaTeX

$$$\\operatorname{FaithfullyFlat}(f) \\iff \\bigl(f\\text{ is Flat} \\wedge \\operatorname{Surjective}(f.specComap)\\bigr)$$$

Lean4

theorem iff_flat_and_comap_surjective : f.FaithfullyFlat ↔ f.Flat ∧ Function.Surjective f.specComap :=
  by
  algebraize [f]
  rw [← algebraMap_toAlgebra f, faithfullyFlat_algebraMap_iff, flat_algebraMap_iff]
  exact
    ⟨fun h ↦ ⟨inferInstance, PrimeSpectrum.specComap_surjective_of_faithfullyFlat⟩, fun ⟨h, hf⟩ ↦
      .of_specComap_surjective hf⟩

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