NYLL
Module

FaithfullyFlatOnOpenImage.lean

Nyll.SchemeTheory.RingTheory.Descent.FaithfullyFlatOnOpenImage
2 declarations indexed from sourceView source ↗

Module documentation

Faithfully flat base change on an open spectral image

The spectral image of a flat finitely presented algebra is represented by an ideal. A base change on which this ideal becomes the unit ideal makes the tensor-product algebra faithfully flat.

Imports7
  • Mathlib.LinearAlgebra.Basis.VectorSpace
  • Mathlib.LinearAlgebra.TensorProduct.Tower
  • Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
  • Mathlib.RingTheory.Flat.Stability
  • Mathlib.RingTheory.LocalRing.ResidueField.Ideal
  • Mathlib.RingTheory.Spectrum.Prime.Chevalley
  • Mathlib.RingTheory.Spectrum.Prime.RingHom
Imported by3

Declarations

theorem

exists_ideal_range_comap_of_flat_of_finitePresentation

L36 ↗
PrimeSpectrum.exists_ideal_range_comap_of_flat_of_finitePresentation
Documentation

The image of a flat finitely presented algebra is the complement of the zero locus of an ideal of the base.

Source context 1 command

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

open TensorProduct PrimeSpectrum
Lean source · statement
theorem PrimeSpectrum.exists_ideal_range_comap_of_flat_of_finitePresentation
    {A₀ B₀ : Type*} [CommRing A₀] [CommRing B₀] [Algebra A₀ B₀]
    [Module.Flat A₀ B₀] [Algebra.FinitePresentation A₀ B₀] :
    ∃ 𝔞 : Ideal A₀, ∀ p : PrimeSpectrum A₀,
      p ∈ Set.range (comap (algebraMap A₀ B₀)) ↔ ¬ 𝔞 ≤ p.asIdeal
theorem

faithfullyFlat_baseChange_of_map_eq_top

L52 ↗
Module.Flat.faithfullyFlat_baseChange_of_map_eq_top
Documentation

A flat algebra becomes faithfully flat after a base change whose spectrum lands in the open image represented by the ideal 𝔞. The image-containment hypothesis is explicit; finite presentation is not needed for this step.

Source context 1 command

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

open TensorProduct PrimeSpectrum
Lean source · statement
theorem Module.Flat.faithfullyFlat_baseChange_of_map_eq_top
    {A₀ B₀ : Type*} [CommRing A₀] [CommRing B₀] [Algebra A₀ B₀]
    [Module.Flat A₀ B₀] (𝔞 : Ideal A₀)
    (h𝔞 : ∀ p : PrimeSpectrum A₀, ¬ 𝔞 ≤ p.asIdeal →
      p ∈ Set.range (comap (algebraMap A₀ B₀)))
    (A' : Type*) [CommRing A'] [Algebra A₀ A'] (htop : 𝔞.map (algebraMap A₀ A') = ⊤) :
    Module.FaithfullyFlat A' (A' ⊗[A₀] B₀)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.