Module

FaithfullyFlatIntegrallyClosed.lean

Nyll.EtaleFundamentalGroups.Purity.Descent.FaithfullyFlatIntegrallyClosed

1 declaration indexed from sourceView source ↗

Module documentation

Faithfully-flat descent of integral closedness

Integral closedness descends along a faithfully-flat map of domains without any Noetherian hypothesis. For an integral fraction a / b of the base, integral closedness upstairs says that its image belongs to the target domain. Hence the image of a belongs to the principal ideal generated by the image of b. Faithful flatness contracts that extended ideal back to the original principal ideal, so b ∣ a already in the base domain.

Imports3

Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Mathlib.RingTheory.Localization.FractionRing

Imported by2

theorem

isIntegrallyClosed_of_faithfullyFlat

L36 ↗

EtaleFundamentalGroups.isIntegrallyClosed_of_faithfullyFlat

Documentation

Integral closedness descends along a faithfully-flat map of domains.

This is the ideal-theoretic faithfully-flat descent proof: a fraction which becomes an element of B makes its numerator belong to the extension of its denominator ideal; Ideal.comap_map_eq_self_of_faithfullyFlat returns that divisibility to A.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups
universe u v

Lean source · statement

theorem isIntegrallyClosed_of_faithfullyFlat
    (A : Type u) (B : Type v)
    [CommRing A] [IsDomain A]
    [CommRing B] [IsDomain B]
    [Algebra A B] [Module.FaithfullyFlat A B]
    [IsIntegrallyClosed B] :
    IsIntegrallyClosed A

Module documentation

Faithfully-flat descent of integral closedness

Declarations

isIntegrallyClosed_of_faithfullyFlat