Module

FiniteProductFaithfullyFlat.lean

Nyll.SchemeTheory.RingTheory.FiniteProductFaithfullyFlat

1 declaration indexed from sourceView source ↗

Module documentation

Faithfully flat products over a Dedekind domain

A finite family of domain algebras over a Dedekind domain gives a faithfully flat product when the structure maps are injective and their spectra cover the base. This applies to finite affine covers of arithmetic schemes: the prime over a given base point is pulled back along one product projection.

Imports2

Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Mathlib.RingTheory.Flat.TorsionFree

Imported by2

theorem

pi_of_dedekind_spectrum_cover

L25 ↗

Module.FaithfullyFlat.pi_of_dedekind_spectrum_cover

Documentation

A finite family of domain algebras with injective structure maps and jointly surjective spectra has faithfully flat product over a Dedekind domain.

Source context 2 commands

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

namespace Module.FaithfullyFlat
universe u v w

Lean source · statement

theorem pi_of_dedekind_spectrum_cover
    (R : Type u) [CommRing R] [IsDedekindDomain R]
    {ι : Type v} [Finite ι] (A : ι → Type w)
    [∀ i, CommRing (A i)] [∀ i, IsDomain (A i)] [∀ i, Algebra R (A i)]
    (hinj : ∀ i, Function.Injective (algebraMap R (A i)))
    (hcover : ∀ p : PrimeSpectrum R,
      ∃ (i : ι) (q : PrimeSpectrum (A i)),
        PrimeSpectrum.comap (algebraMap R (A i)) q = p) :
    Module.FaithfullyFlat R (∀ i, A i)

Module documentation

Faithfully flat products over a Dedekind domain

Declarations

pi_of_dedekind_spectrum_cover