Module

Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff

19 declarations indexed from sourceView source ↗

Module documentation

Module exists ideal forall projective and rank At Stalk eq iff

Imports6

Mathlib.RingTheory.LocalProperties.FinitePresentation
Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Mathlib.Tactic.Abel
Mathlib.Tactic.ByContra
Mathlib.Tactic.Choose
Mathlib.Tactic.Ext

Imported by2

theorem

exists_equiv_prod_ker

L38 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff.FittingClosed.exists_equiv_prod_ker

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff
open scoped TensorProduct
open TensorProduct
namespace FittingClosed
section Modules
variable {A : Type} [CommRing A]

Lean source · statement

theorem exists_equiv_prod_ker {Q₁ Q₂ : Type} [AddCommGroup Q₁] [Module A Q₁] [AddCommGroup Q₂]
  [Module A Q₂]
    [Module.Projective A Q₂] (π : Q₁ →ₗ[A] Q₂) (hπ : Function.Surjective π) :
    ∃ e : Q₁ ≃ₗ[A] Q₂ × LinearMap.ker π, ∀ x, (e x).1 = π x

theorem

nontrivial_of_primeSpectrum

L54 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff.FittingClosed.nontrivial_of_primeSpectrum

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff
open scoped TensorProduct
open TensorProduct
namespace FittingClosed
section Modules
variable {A : Type} [CommRing A]

Lean source · statement

theorem nontrivial_of_primeSpectrum (q : PrimeSpectrum A) : Nontrivial A

def

syz

L64 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff.FittingClosed.syz

Documentation

The ideal generated by the coordinate projections of the relations of a finite presentation.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff
open scoped TensorProduct
open TensorProduct
namespace FittingClosed
section Core
variable {A : Type} [CommRing A] {M : Type} [AddCommGroup M] [Module A M] {r : ℕ}

Lean source · statement

def syz (ε : (Fin r → A) →ₗ[A] M) : Ideal A

theorem

apply_mem_syz

L67 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff.FittingClosed.apply_mem_syz

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff
open scoped TensorProduct
open TensorProduct
namespace FittingClosed
section Core
variable {A : Type} [CommRing A] {M : Type} [AddCommGroup M] [Module A M] {r : ℕ}

Lean source · statement

theorem apply_mem_syz (ε : (Fin r → A) →ₗ[A] M) {k : Fin r → A} (hk : ε k = 0) (i : Fin r) :
    k i ∈ syz ε

theorem

syz_le_iff

L72 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff.FittingClosed.syz_le_iff

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff
open scoped TensorProduct
open TensorProduct
namespace FittingClosed
section Core
variable {A : Type} [CommRing A] {M : Type} [AddCommGroup M] [Module A M] {r : ℕ}

Lean source · statement

theorem syz_le_iff (ε : (Fin r → A) →ₗ[A] M) (J : Ideal A) :
    syz ε ≤ J ↔ ∀ k : Fin r → A, ε k = 0 → ∀ i, k i ∈ J

theorem

piScalarRight_tmul

L84 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff.FittingClosed.piScalarRight_tmul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff
open scoped TensorProduct
open TensorProduct
namespace FittingClosed
section Core
variable {A : Type} [CommRing A] {M : Type} [AddCommGroup M] [Module A M] {r : ℕ}
variable (C : Type) [CommRing C] [Algebra A C]

Lean source · full declaration

theorem piScalarRight_tmul (c : C) (k : Fin r → A) :
    piScalarRight A C C (Fin r) (c ⊗ₜ[A] k) = fun i => algebraMap A C (k i) * c := by
  classical
  rw [piScalarRight_apply, piScalarRightHom_tmul]
  funext i
  rw [Algebra.smul_def]

theorem

core_equiv

L91 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff.FittingClosed.core_equiv

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff
open scoped TensorProduct
open TensorProduct
namespace FittingClosed
section Core
variable {A : Type} [CommRing A] {M : Type} [AddCommGroup M] [Module A M] {r : ℕ}
variable (C : Type) [CommRing C] [Algebra A C]

Lean source · full declaration

theorem core_equiv (ε : (Fin r → A) →ₗ[A] M) (hε : Function.Surjective ε)
    (h : ∀ a ∈ syz ε, algebraMap A C a = 0) :
    ∃ e : (C ⊗[A] M) ≃ₗ[C] (Fin r → C),
      ∀ k : Fin r → A, e ((1 : C) ⊗ₜ[A] ε k) = fun i => algebraMap A C (k i) := by
  classical
  set g : C ⊗[A] (Fin r → A) →ₗ[C] C ⊗[A] M := ε.baseChange C with hg
  have hgs : Function.Surjective g := by
    rw [hg, LinearMap.baseChange_eq_ltensor]
    exact LinearMap.lTensor_surjective C hε
  have hex : Function.Exact ((LinearMap.ker ε).subtype.lTensor C) (ε.lTensor C) :=
    lTensor_exact C (LinearMap.exact_subtype_ker_map ε) hε
  have hzero : (LinearMap.ker ε).subtype.lTensor C = 0 := by
    apply TensorProduct.ext'
    intro c k
    rw [LinearMap.lTensor_tmul, LinearMap.zero_apply]
    apply (piScalarRight A C C (Fin r)).injective
    rw [map_zero, piScalarRight_tmul]
    funext i
    rw [Pi.zero_apply, Submodule.subtype_apply, h _ (apply_mem_syz ε (LinearMap.mem_ker.mp k.2) i),
      zero_mul]
  have hgi : Function.Injective g := by
    rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']
    intro x hx
    have hx' : (ε.lTensor C) x = 0 := by
      rw [← LinearMap.baseChange_eq_ltensor]; exact hx
    obtain ⟨y, hy⟩ := (hex x).mp hx'
    rw [← hy, hzero, LinearMap.zero_apply]
  let E : C ⊗[A] (Fin r → A) ≃ₗ[C] C ⊗[A] M := LinearEquiv.ofBijective g ⟨hgi, hgs⟩
  refine ⟨E.symm ≪≫ₗ piScalarRight A C C (Fin r), fun k => ?_⟩
  have hk : E ((1 : C) ⊗ₜ[A] k) = (1 : C) ⊗ₜ[A] ε k := by
    change g ((1 : C) ⊗ₜ[A] k) = _
    rw [hg, LinearMap.baseChange_tmul]
  rw [LinearEquiv.trans_apply, ← hk, LinearEquiv.symm_apply_apply, piScalarRight_tmul]
  funext i
  rw [mul_one]

theorem

core_vanish

L127 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff.FittingClosed.core_vanish

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff
open scoped TensorProduct
open TensorProduct
namespace FittingClosed
section Core
variable {A : Type} [CommRing A] {M : Type} [AddCommGroup M] [Module A M] {r : ℕ}
variable (C : Type) [CommRing C] [Algebra A C]

Lean source · statement

theorem core_vanish (ε : (Fin r → A) →ₗ[A] M) (hε : Function.Surjective ε)
    [Module.Projective C (C ⊗[A] M)] (hrank : ∀ q : PrimeSpectrum C, Module.rankAtStalk (C ⊗[A] M)
      q = r) :
    ∀ a ∈ syz ε, algebraMap A C a = 0

def

pres

L182 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff.FittingClosed.pres

Documentation

The presentation map after scalar extension associated with the chosen finite family of generators.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff
open scoped TensorProduct
open TensorProduct
namespace FittingClosed
section Chart

Lean source · statement

def pres (A : Type) [CommRing A] {M : Type} [AddCommGroup M] [Module A M] {r : ℕ}
    (A' : Type) [CommRing A'] [Algebra A A'] (m : Fin r → M) : (Fin r → A') →ₗ[A'] A' ⊗[A] M

def

chartIdeal

L187 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff.FittingClosed.chartIdeal

Documentation

The ideal generated by the coordinate relations of the presentation after scalar extension.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff
open scoped TensorProduct
open TensorProduct
namespace FittingClosed
section Chart

Lean source · statement

def chartIdeal (A : Type) [CommRing A] {M : Type} [AddCommGroup M] [Module A M] {r :
  ℕ}
    (A' : Type) [CommRing A'] [Algebra A A'] (m : Fin r → M) : Ideal A'

def

IsChart

L193 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff.FittingClosed.IsChart

Documentation

The condition that the chosen family generates the module after scalar extension.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff
open scoped TensorProduct
open TensorProduct
namespace FittingClosed
section Chart

Lean source · statement

def IsChart (A : Type) [CommRing A] {M : Type} [AddCommGroup M] [Module A M] {r : ℕ}
    (A' : Type) [CommRing A'] [Algebra A A'] (m : Fin r → M) : Prop

theorem

pres_surjective

L199 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff.FittingClosed.pres_surjective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff
open scoped TensorProduct
open TensorProduct
namespace FittingClosed
section Chart
variable {A : Type} [CommRing A] {M : Type} [AddCommGroup M] [Module A M] {r : ℕ}

Lean source · statement

theorem pres_surjective {A' : Type} [CommRing A'] [Algebra A A'] {m : Fin r → M} (hm : IsChart A A'
  m) :
    Function.Surjective (pres A A' m)

theorem

chart_equiv

L205 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff.FittingClosed.chart_equiv

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff
open scoped TensorProduct
open TensorProduct
namespace FittingClosed
section Chart
variable {A : Type} [CommRing A] {M : Type} [AddCommGroup M] [Module A M] {r : ℕ}

Lean source · statement

theorem chart_equiv {A' : Type} [CommRing A'] [Algebra A A'] {m : Fin r → M}
    (C : Type) [CommRing C] [Algebra A C] [Algebra A' C] [IsScalarTower A A' C]
    (hm : IsChart A A' m) (h : ∀ a ∈ chartIdeal A A' m, algebraMap A' C a = 0) :
    Nonempty ((C ⊗[A] M) ≃ₗ[C] (Fin r → C))

theorem

chart_vanish

L212 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff.FittingClosed.chart_vanish

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff
open scoped TensorProduct
open TensorProduct
namespace FittingClosed
section Chart
variable {A : Type} [CommRing A] {M : Type} [AddCommGroup M] [Module A M] {r : ℕ}

Lean source · statement

theorem chart_vanish {A' : Type} [CommRing A'] [Algebra A A'] {m : Fin r → M}
    (C : Type) [CommRing C] [Algebra A C] [Algebra A' C] [IsScalarTower A A' C]
    (hm : IsChart A A' m) [Module.Projective C (C ⊗[A] M)]
    (hrank : ∀ q : PrimeSpectrum C, Module.rankAtStalk (C ⊗[A] M) q = r) :
    ∀ a ∈ chartIdeal A A' m, algebraMap A' C a = 0

theorem

span_one_tmul_eq_top

L231 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff.FittingClosed.span_one_tmul_eq_top

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff
open scoped TensorProduct
open TensorProduct
namespace FittingClosed
section LocalGen
variable (A : Type) [CommRing A] (M : Type) [AddCommGroup M] [Module A M] [Module.Finite A M] (r :
  ℕ)
omit [Module.Finite A M] in

Lean source · full declaration

theorem span_one_tmul_eq_top (L : Type) [CommRing L] [Algebra A L] :
    Submodule.span L (Set.range fun x : M => (1 : L) ⊗ₜ[A] x) = ⊤ := by
  have h := Submodule.baseChange_top (R := A) (M := M) L
  rw [Submodule.baseChange_eq_span, Submodule.map_top, LinearMap.coe_range] at h
  exact h

theorem

exists_chart

L237 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff.FittingClosed.exists_chart

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff
open scoped TensorProduct
open TensorProduct
namespace FittingClosed
section LocalGen
variable (A : Type) [CommRing A] (M : Type) [AddCommGroup M] [Module A M] [Module.Finite A M] (r :
  ℕ)

Lean source · statement

theorem exists_chart (p : PrimeSpectrum A)
    (hr : Module.finrank p.asIdeal.ResidueField (p.asIdeal.ResidueField ⊗[A] M) ≤ r) :
    ∃ f : A, f ∉ p.asIdeal ∧ ∃ m : Fin r → M, IsChart A (Localization.Away f) m

theorem

compat

L332 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff.FittingClosed.compat

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff
open scoped TensorProduct
open TensorProduct
namespace FittingClosed
section Compat
variable {A : Type} [CommRing A] {M : Type} [AddCommGroup M] [Module A M] {r : ℕ}

Lean source · statement

theorem compat (g g' : A) (m m' : Fin r → M) (hm : IsChart A (Localization.Away g) m)
    (hm' : IsChart A (Localization.Away g') m') (a : A)
    (ha : algebraMap A (Localization.Away g) a ∈ chartIdeal A (Localization.Away g) m) :
    ∃ N : ℕ, algebraMap A (Localization.Away g') (a * g ^ N) ∈ chartIdeal A (Localization.Away g')
      m'

theorem

main

L385 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff.FittingClosed.main

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff
open scoped TensorProduct
open TensorProduct
namespace FittingClosed
section Glue
variable (A : Type) [CommRing A] (M : Type) [AddCommGroup M] [Module A M] [Module.Finite A M] (r :
  ℕ)

Lean source · statement

theorem main
    (hr : ∀ p : PrimeSpectrum A,
      Module.finrank p.asIdeal.ResidueField (p.asIdeal.ResidueField ⊗[A] M) ≤ r) :
    ∃ 𝔞 : Ideal A, ∀ (B : Type) [CommRing B] [Algebra A B],
      (Module.Projective B (B ⊗[A] M) ∧ ∀ q : PrimeSpectrum B, Module.rankAtStalk (B ⊗[A] M) q = r)
        ↔
        ∀ a ∈ 𝔞, algebraMap A B a = 0

theorem

exists_ideal_forall_projective_and_rankAtStalk_eq_iff

L513 ↗

Module.exists_ideal_forall_projective_and_rankAtStalk_eq_iff

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff
open scoped TensorProduct
open TensorProduct

Lean source · statement

theorem _root_.Module.exists_ideal_forall_projective_and_rankAtStalk_eq_iff
    (A : Type) [CommRing A] (M : Type) [AddCommGroup M] [Module A M] [Module.Finite A M] (r : ℕ)
    (hr : ∀ p : PrimeSpectrum A,
      Module.finrank p.asIdeal.ResidueField (p.asIdeal.ResidueField ⊗[A] M) ≤ r) :
    ∃ 𝔞 : Ideal A, ∀ (B : Type) [CommRing B] [Algebra A B],
      (Module.Projective B (B ⊗[A] M) ∧ ∀ q : PrimeSpectrum B, Module.rankAtStalk (B ⊗[A] M) q = r)
        ↔
        ∀ a ∈ 𝔞, algebraMap A B a = 0

Module documentation

Module exists ideal forall projective and rank At Stalk eq iff

Declarations