comap_surjective_of_faithfullyFlat

English

If B is a faithfully flat A-algebra, every ideal I in A is the comap of some ideal in B.

Русский

Если B является доверительно плоским A-алгеброй, каждый идеал I в A является обобщением образа через некоторый идеал в B.

LaTeX

$$Function.Surjective(Ideal.comap(algebraMap A B))$$

Lean4

/-- If `B` is a faithfully-flat `A`-algebra, every ideal in `A` is the preimage of some ideal
in `B`. -/
theorem comap_surjective_of_faithfullyFlat : Function.Surjective (Ideal.comap (algebraMap A B)) := fun I ↦
  ⟨I.map (algebraMap A B), comap_map_eq_self_of_faithfullyFlat I⟩

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