Normal domains descend along faithfully flat maps

If A → B is faithfully flat and B is an integrally closed domain, then A is integrally closed. The map is injective, so A is a domain (Mathlib's IsDomain.of_faithfulSMul). If a / b is integral over A, its image is integral over B, hence a ∈ bB; faithful flatness gives bB ∩ A = bA (Ideal.comap_map_eq_self_of_faithfullyFlat), so a ∈ bA and a / b ∈ A.

Main results

• TauCeti.IsIntegrallyClosed.of_faithfullyFlat: if B is an integrally closed domain that is faithfully flat over A, then A is integrally closed.

References

• Stacks Project, Lemma 10.164.3.

theorem TauCeti.IsIntegrallyClosed.of_faithfullyFlat (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] [Module.FaithfullyFlat A B] [IsDomain B] [IsIntegrallyClosed B] : IsIntegrallyClosed A

Normality descends along faithfully flat maps. If B is an integrally closed domain that is faithfully flat over A, then A is integrally closed. Stacks, Lemma 10.164.3 (033G), for domains.