specComap_surjective_of_faithfullyFlat

English

If B is faithfully flat A-algebra, the map on prime spectra Spec(B) → Spec(A) is surjective.

Русский

Если B — faithfully flat A-алгебра, переход по спектрам Spec(B) → Spec(A) сюръективен.

LaTeX

$$Function.Surjective((algebraMap A B).specComap)$$

Lean4

/-- If `B` is a faithfully flat `A`-algebra, the induced map on the prime spectrum is
surjective. -/
theorem specComap_surjective_of_faithfullyFlat : Function.Surjective (algebraMap A B).specComap := fun I ↦
  (PrimeSpectrum.mem_range_comap_iff (algebraMap A B)).mpr I.asIdeal.comap_map_eq_self_of_faithfullyFlat

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