NYLL
Module

OpenLocus.lean

Nyll.SchemeTheory.RingTheory.Flat.OpenLocus
16 declarations indexed from sourceView source ↗

Module documentation

Openness of the flat locus

Tensor-kernel torsion criteria characterize flatness at a prime and its behavior under specialization. For the stated noetherian and finite-presentation hypotheses, the locus of flat prime localizations is open.

Imports19
  • Mathlib.LinearAlgebra.TensorProduct.RightExactness
  • Mathlib.LinearAlgebra.TensorProduct.Tower
  • Mathlib.RingTheory.FiniteType
  • Mathlib.RingTheory.FiniteStability
  • Mathlib.RingTheory.Flat.Basic
  • Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
  • Mathlib.RingTheory.Ideal.Operations
  • Mathlib.RingTheory.Ideal.Quotient.Noetherian
  • Mathlib.RingTheory.Localization.AtPrime.Basic
  • Mathlib.RingTheory.Localization.BaseChange
  • Mathlib.RingTheory.Localization.Basic
  • Mathlib.RingTheory.Localization.Submodule
  • Mathlib.RingTheory.Noetherian.Basic
  • Mathlib.RingTheory.Spectrum.Prime.Basic
  • Mathlib.RingTheory.Spectrum.Prime.Topology
  • Mathlib.RingTheory.TensorProduct.Basic
  • Mathlib.RingTheory.TensorProduct.Finite
  • Nyll.SchemeTheory.RingTheory.Flat.GenericFlatness
  • Nyll.SchemeTheory.RingTheory.Flat.LocalCriterion
Imported by3

Declarations

def

K

L61 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_isOpen_setOf_flat_localization_atPrime.OpenFlatLocus.K
Documentation

The kernel of f after tensoring with the algebra B.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_isOpen_setOf_flat_localization_atPrime
open TensorProduct
noncomputable section
namespace OpenFlatLocus
section Tors
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
variable (S : Submonoid B) (Bs : Type*) [CommRing Bs] [Algebra B Bs] [Algebra A Bs]
  [IsScalarTower A B Bs] [IsLocalization S Bs]
variable {Y' Y : Type*} [AddCommGroup Y'] [Module A Y'] [AddCommGroup Y] [Module A Y]
  (f : Y' →ₗ[A] Y)
Lean source · statement
def K : Submodule B (B ⊗[A] Y')
lemma

mem_K

L63 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_isOpen_setOf_flat_localization_atPrime.OpenFlatLocus.mem_K
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_isOpen_setOf_flat_localization_atPrime
open TensorProduct
noncomputable section
namespace OpenFlatLocus
section Tors
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
variable (S : Submonoid B) (Bs : Type*) [CommRing Bs] [Algebra B Bs] [Algebra A Bs]
  [IsScalarTower A B Bs] [IsLocalization S Bs]
variable {Y' Y : Type*} [AddCommGroup Y'] [Module A Y'] [AddCommGroup Y] [Module A Y]
  (f : Y' →ₗ[A] Y)
Lean source · statement
lemma mem_K (k : B ⊗[A] Y') : k ∈ K f ↔ LinearMap.lTensor B f k = 0
theorem

injective_lTensor_iff

L66 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_isOpen_setOf_flat_localization_atPrime.OpenFlatLocus.injective_lTensor_iff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_isOpen_setOf_flat_localization_atPrime
open TensorProduct
noncomputable section
namespace OpenFlatLocus
section Tors
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
variable (S : Submonoid B) (Bs : Type*) [CommRing Bs] [Algebra B Bs] [Algebra A Bs]
  [IsScalarTower A B Bs] [IsLocalization S Bs]
variable {Y' Y : Type*} [AddCommGroup Y'] [Module A Y'] [AddCommGroup Y] [Module A Y]
  (f : Y' →ₗ[A] Y)
Lean source · statement
theorem injective_lTensor_iff :
    Function.Injective (LinearMap.lTensor Bs f) ↔ ∀ k ∈ K (B := B) f, ∃ s ∈ S, s • k = 0
lemma

injective_rTensor_iff

L101 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_isOpen_setOf_flat_localization_atPrime.OpenFlatLocus.injective_rTensor_iff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_isOpen_setOf_flat_localization_atPrime
open TensorProduct
noncomputable section
namespace OpenFlatLocus
section Tors
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
variable (S : Submonoid B) (Bs : Type*) [CommRing Bs] [Algebra B Bs] [Algebra A Bs]
  [IsScalarTower A B Bs] [IsLocalization S Bs]
variable {Y' Y : Type*} [AddCommGroup Y'] [Module A Y'] [AddCommGroup Y] [Module A Y]
  (f : Y' →ₗ[A] Y)
Lean source · statement
lemma injective_rTensor_iff : Function.Injective (LinearMap.rTensor Bs f) ↔
    Function.Injective (LinearMap.lTensor Bs f)
def

Tors

L118 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_isOpen_setOf_flat_localization_atPrime.OpenFlatLocus.Tors
Documentation

Every element of the tensor kernel is annihilated by an element outside the prime Q.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_isOpen_setOf_flat_localization_atPrime
open TensorProduct
noncomputable section
namespace OpenFlatLocus
section FlatIff
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
def Tors (Q : PrimeSpectrum B) {Y' Y : Type*} [AddCommGroup Y'] [Module A Y'] [AddCommGroup Y]
    [Module A Y] (f : Y' →ₗ[A] Y) : Prop
lemma

mono

L122 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_isOpen_setOf_flat_localization_atPrime.OpenFlatLocus.Tors.mono
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_isOpen_setOf_flat_localization_atPrime
open TensorProduct
noncomputable section
namespace OpenFlatLocus
section FlatIff
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
lemma Tors.mono {Q Q' : PrimeSpectrum B} (h : Q'.asIdeal ≤ Q.asIdeal) {Y' Y : Type*}
    [AddCommGroup Y'] [Module A Y'] [AddCommGroup Y] [Module A Y] {f : Y' →ₗ[A] Y}
    (hQ : Tors Q f) : Tors Q' f
theorem

tors_of_flat

L128 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_isOpen_setOf_flat_localization_atPrime.OpenFlatLocus.tors_of_flat
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_isOpen_setOf_flat_localization_atPrime
open TensorProduct
noncomputable section
namespace OpenFlatLocus
section FlatIff
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
theorem tors_of_flat (Q : PrimeSpectrum B) [Module.Flat A (Localization.AtPrime Q.asIdeal)]
    {Y' Y : Type*} [AddCommGroup Y'] [Module A Y'] [AddCommGroup Y] [Module A Y]
    (f : Y' →ₗ[A] Y) (hf : Function.Injective f) : Tors Q f
theorem

flat_of_tors

L134 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_isOpen_setOf_flat_localization_atPrime.OpenFlatLocus.flat_of_tors
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_isOpen_setOf_flat_localization_atPrime
open TensorProduct
noncomputable section
namespace OpenFlatLocus
section FlatIff
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
theorem flat_of_tors [IsNoetherianRing A] [IsNoetherianRing B] (Q : PrimeSpectrum B)
    (p : Ideal A) (hp : Q.asIdeal.comap (algebraMap A B) = p)
    (hQ : Tors (A := A) (Y' := ↥p) (Y := A) Q p.subtype) :
    Module.Flat A (Localization.AtPrime Q.asIdeal)
theorem

flat_of_le

L148 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_isOpen_setOf_flat_localization_atPrime.OpenFlatLocus.flat_of_le
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_isOpen_setOf_flat_localization_atPrime
open TensorProduct
noncomputable section
namespace OpenFlatLocus
section FlatIff
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
theorem flat_of_le [IsNoetherianRing A] [IsNoetherianRing B] {Q Q' : PrimeSpectrum B}
    (h : Q'.asIdeal ≤ Q.asIdeal) [Module.Flat A (Localization.AtPrime Q.asIdeal)] :
    Module.Flat A (Localization.AtPrime Q'.asIdeal)
theorem

isOpen_of_nagata

L161 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_isOpen_setOf_flat_localization_atPrime.OpenFlatLocus.isOpen_of_nagata
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_isOpen_setOf_flat_localization_atPrime
open TensorProduct
noncomputable section
namespace OpenFlatLocus
section Nagata
variable {B : Type*} [CommRing B] [IsNoetherianRing B]
Lean source · statement
theorem isOpen_of_nagata (U : Set (PrimeSpectrum B))
    (hgen : ∀ Q Q' : PrimeSpectrum B, Q'.asIdeal ≤ Q.asIdeal → Q ∈ U → Q' ∈ U)
    (hnbhd : ∀ Q ∈ U, ∃ g : B, g ∉ Q.asIdeal ∧
      ∀ Q' : PrimeSpectrum B, Q.asIdeal ≤ Q'.asIdeal → g ∉ Q'.asIdeal → Q' ∈ U) :
    IsOpen U
theorem

exists_uniform_killer

L222 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_isOpen_setOf_flat_localization_atPrime.OpenFlatLocus.exists_uniform_killer
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_isOpen_setOf_flat_localization_atPrime
open TensorProduct
noncomputable section
namespace OpenFlatLocus
section Fibre
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
theorem exists_uniform_killer {N : Type*} [AddCommGroup N] [Module B N] (S : Submonoid B)
    (K : Submodule B N) (hK : K.FG) (h : ∀ k ∈ K, ∃ s ∈ S, s • k = 0) :
    ∃ s ∈ S, ∀ k ∈ K, s • k = 0
theorem

flat_fibre_away

L249 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_isOpen_setOf_flat_localization_atPrime.OpenFlatLocus.flat_fibre_away
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_isOpen_setOf_flat_localization_atPrime
open TensorProduct
noncomputable section
namespace OpenFlatLocus
section Fibre
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
section FibreAway
variable (p : Ideal A) (a : A)
local notation "A'" => A ⧸ p
local notation "C" => (A ⧸ p) ⊗[A] B
local notation "Ba" => Localization.Away (algebraMap A B a)
local notation "F" => (A ⧸ p) ⊗[A] Localization.Away (algebraMap A B a)
Lean source · statement
theorem flat_fibre_away
    (hflat : Module.Flat (A ⧸ p) (Localization (Submonoid.powers
      (algebraMap (A ⧸ p) ((A ⧸ p) ⊗[A] B) (Ideal.Quotient.mk p a))))) :
    Module.Flat (A ⧸ p) F
theorem

injective_lTensor_away

L344 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_isOpen_setOf_flat_localization_atPrime.OpenFlatLocus.injective_lTensor_away
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_isOpen_setOf_flat_localization_atPrime
open TensorProduct
noncomputable section
namespace OpenFlatLocus
section Fibre
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
section FibreAway
variable (p : Ideal A) (a : A)
local notation "A'" => A ⧸ p
local notation "C" => (A ⧸ p) ⊗[A] B
local notation "Ba" => Localization.Away (algebraMap A B a)
local notation "F" => (A ⧸ p) ⊗[A] Localization.Away (algebraMap A B a)
Lean source · statement
theorem injective_lTensor_away (X : Ideal (A ⧸ p)) [Module.Flat (A ⧸ p) F] :
    Function.Injective (LinearMap.lTensor Ba (X.subtype.restrictScalars A))
theorem

fibre_step

L383 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_isOpen_setOf_flat_localization_atPrime.OpenFlatLocus.fibre_step
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_isOpen_setOf_flat_localization_atPrime
open TensorProduct
noncomputable section
namespace OpenFlatLocus
section Fibre
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
section Step
variable [IsNoetherianRing A] [Algebra.FiniteType A B]
Lean source · statement
theorem fibre_step (Q : PrimeSpectrum B) [Module.Flat A (Localization.AtPrime Q.asIdeal)] :
    ∃ g : B, g ∉ Q.asIdeal ∧ ∀ Q' : PrimeSpectrum B, Q.asIdeal ≤ Q'.asIdeal → g ∉ Q'.asIdeal →
      Module.Flat A (Localization.AtPrime Q'.asIdeal)
theorem

isOpen_flatLocus

L465 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_isOpen_setOf_flat_localization_atPrime.OpenFlatLocus.isOpen_flatLocus
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_isOpen_setOf_flat_localization_atPrime
open TensorProduct
noncomputable section
namespace OpenFlatLocus
Lean source · statement
theorem isOpen_flatLocus {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] [IsNoetherianRing A]
    [Algebra.FiniteType A B] :
    IsOpen {Q : PrimeSpectrum B | Module.Flat A (Localization.AtPrime Q.asIdeal)}
theorem

isOpen_setOf_flat_localization_atPrime

L479 ↗
Module.Flat.isOpen_setOf_flat_localization_atPrime
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_isOpen_setOf_flat_localization_atPrime
open TensorProduct
Lean source · statement
theorem _root_.Module.Flat.isOpen_setOf_flat_localization_atPrime
    {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] [IsNoetherianRing A]
    [Algebra.FiniteType A B] :
    IsOpen {Q : PrimeSpectrum B | Module.Flat A (Localization.AtPrime Q.asIdeal)}

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