Module

Module_finitePresentation_of_rankAtStalk_eq.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Module_finitePresentation_of_rankAtStalk_eq

8 declarations indexed from sourceView source ↗

Module documentation

Finite presentation from constant rank at stalks

Relates localization and constant stalk rank to finite presentation.

Imports1

Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Imported by4

theorem

localized'_eq_top_iff

L38 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_finitePresentation_of_rankAtStalk_eq.FPRank.localized'_eq_top_iff

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_finitePresentation_of_rankAtStalk_eq
universe u v
open Module
namespace FPRank
section localizedTop
variable {R : Type*} [CommRing R] (S : Submonoid R) (A : Type*) [CommRing A] [Algebra R A]
  [IsLocalization S A] {M : Type*} [AddCommGroup M] [Module R M] {Mₛ : Type*}
  [AddCommGroup Mₛ] [Module R Mₛ] [Module A Mₛ] [IsScalarTower R A Mₛ] (f : M →ₗ[R] Mₛ)
  [IsLocalizedModule S f]

Lean source · statement

theorem localized'_eq_top_iff (N : Submodule R M) :
    N.localized' A S f = ⊤ ↔ ∀ x : M, ∃ t : S, (t : R) • x ∈ N

theorem

localized'_eq_top_iff_subsingleton

L57 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_finitePresentation_of_rankAtStalk_eq.FPRank.localized'_eq_top_iff_subsingleton

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_finitePresentation_of_rankAtStalk_eq
universe u v
open Module
namespace FPRank
section localizedTop
variable {R : Type*} [CommRing R] (S : Submonoid R) (A : Type*) [CommRing A] [Algebra R A]
  [IsLocalization S A] {M : Type*} [AddCommGroup M] [Module R M] {Mₛ : Type*}
  [AddCommGroup Mₛ] [Module R Mₛ] [Module A Mₛ] [IsScalarTower R A Mₛ] (f : M →ₗ[R] Mₛ)
  [IsLocalizedModule S f]

Lean source · statement

theorem localized'_eq_top_iff_subsingleton (N : Submodule R M) :
    N.localized' A S f = ⊤ ↔ Subsingleton (LocalizedModule S (M ⧸ N))

theorem

injective_of_surjective_of_rankAtStalk_eq

L79 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_finitePresentation_of_rankAtStalk_eq.FPRank.injective_of_surjective_of_rankAtStalk_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_finitePresentation_of_rankAtStalk_eq
universe u v
open Module
namespace FPRank
section surjection
variable {A : Type*} [CommRing A] {P : Type*} [AddCommGroup P] [Module A P]
  [Module.Finite A P] [Module.Flat A P] {n : ℕ}

Lean source · statement

theorem injective_of_surjective_of_rankAtStalk_eq
    (h : ∀ p : PrimeSpectrum A, rankAtStalk P p = n)
    (ψ : (Fin n → A) →ₗ[A] P) (hψ : Function.Surjective ψ) : Function.Injective ψ

theorem

finitePresentation_of_surjective_of_rankAtStalk_eq

L106 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_finitePresentation_of_rankAtStalk_eq.FPRank.finitePresentation_of_surjective_of_rankAtStalk_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_finitePresentation_of_rankAtStalk_eq
universe u v
open Module
namespace FPRank
section surjection
variable {A : Type*} [CommRing A] {P : Type*} [AddCommGroup P] [Module A P]
  [Module.Finite A P] [Module.Flat A P] {n : ℕ}

Lean source · statement

theorem finitePresentation_of_surjective_of_rankAtStalk_eq
    (h : ∀ p : PrimeSpectrum A, rankAtStalk P p = n)
    (ψ : (Fin n → A) →ₗ[A] P) (hψ : Function.Surjective ψ) : Module.FinitePresentation A P

theorem

finitePresentation_of_localizationSpan

L120 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_finitePresentation_of_rankAtStalk_eq.FPRank.finitePresentation_of_localizationSpan

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_finitePresentation_of_rankAtStalk_eq
universe u v
open Module
namespace FPRank
section localToGlobal
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

theorem finitePresentation_of_localizationSpan (s : Set R) (hs : Ideal.span s = ⊤)
    (H : ∀ r : s, Module.FinitePresentation (Localization.Away (r : R))
      (LocalizedModule (Submonoid.powers (r : R)) M)) :
    Module.FinitePresentation R M

theorem

exists_finitePresentation_away

L147 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_finitePresentation_of_rankAtStalk_eq.FPRank.exists_finitePresentation_away

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_finitePresentation_of_rankAtStalk_eq
universe u v
open Module
namespace FPRank
section mainProof
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
  [Module.Finite R M] [Module.Flat R M] {n : ℕ}

Lean source · statement

theorem exists_finitePresentation_away (h : ∀ p : PrimeSpectrum R, rankAtStalk M p = n)
    (p : PrimeSpectrum R) :
    ∃ r : R, r ∉ p.asIdeal ∧ Module.FinitePresentation (Localization.Away r)
      (LocalizedModule (Submonoid.powers r) M)

theorem

finitePresentation_of_rankAtStalk_eq

L198 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_finitePresentation_of_rankAtStalk_eq.FPRank.finitePresentation_of_rankAtStalk_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_finitePresentation_of_rankAtStalk_eq
universe u v
open Module
namespace FPRank
section main
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
  [Module.Finite R M] [Module.Flat R M] {n : ℕ}

Lean source · statement

theorem finitePresentation_of_rankAtStalk_eq (h : ∀ p : PrimeSpectrum R, rankAtStalk M p = n) :
    Module.FinitePresentation R M

theorem

finitePresentation_of_rankAtStalk_eq

L212 ↗

Module.finitePresentation_of_rankAtStalk_eq

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_finitePresentation_of_rankAtStalk_eq
universe u v
open Module

Lean source · statement

theorem _root_.Module.finitePresentation_of_rankAtStalk_eq {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Flat R M] (n : ℕ)
    (h : ∀ p : PrimeSpectrum R, Module.rankAtStalk M p = n) : Module.FinitePresentation R M

Module documentation

Finite presentation from constant rank at stalks

Declarations