Module

DoubleComplex_Convergence_finite_E2_q0.lean

Nyll.SchemeTheory.HomologicalAlgebra.DoubleComplex_Convergence_finite_E2_q0

4 declarations indexed from sourceView source ↗

Module documentation

Finiteness in the zero row of the second page of a convergent double complex.

Imports3

Mathlib.RingTheory.Noetherian.Basic
Mathlib.RingTheory.Finiteness.Basic
Nyll.SchemeTheory.Cohomology.Sheaves.DoubleComplex

Imported by2

theorem

subquot_finite

L38 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_Convergence_finite_E2_q0.DoubleComplex.subquot_finite

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_Convergence_finite_E2_q0
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Extract
variable {R : Type u} [CommRing R]

Lean source · statement

theorem subquot_finite [IsNoetherianRing R]
    {M : Type u} [AddCommGroup M] [Module R M] [Module.Finite R M]
    (s : SubQuot R M) : Module.Finite R s.carrier

theorem

filt_finite

L45 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_Convergence_finite_E2_q0.DoubleComplex.filt_finite

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_Convergence_finite_E2_q0
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Extract
variable {R : Type u} [CommRing R]

Lean source · statement

theorem filt_finite [IsNoetherianRing R]
    {M : Type u} [AddCommGroup M] [Module R M] {N : ℕ} (F : Fin (N + 1) → Submodule R M)
    (hF₀ : F 0 = ⊥) (hFmono : Monotone F)
    (hFgr : ∀ i : Fin N,
      Module.Finite R (↥(F i.succ) ⧸ (F i.castSucc).comap (F i.succ).subtype)) :
    ∀ i, Module.Finite R ↥(F i)

theorem

finite_E2_q0

L66 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_Convergence_finite_E2_q0.DoubleComplex.Convergence.finite_E2_q0

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_Convergence_finite_E2_q0
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Extract
variable {R : Type u} [CommRing R]
open scoped _root_.DoubleComplex.Convergence in

Lean source · statement

theorem Convergence.finite_E2_q0 [IsNoetherianRing R]
    {E₂ : ℕ → ℕ → Type u} [∀ p q, AddCommGroup (E₂ p q)] [∀ p q, Module R (E₂ p q)]
    {H : ℕ → Type u} [∀ n, AddCommGroup (H n)] [∀ n, Module R (H n)] {N : ℕ}
    (conv : Convergence R E₂ H N)
    (hH : ∀ n, Module.Finite R (H n)) (hE₂ : ∀ p q, 1 ≤ q → Module.Finite R (E₂ p q))
    (p : ℕ) (hp : p ≤ N) : Module.Finite R (E₂ p 0)

theorem

finite_E2_q0

L103 ↗

DoubleComplex.Convergence.finite_E2_q0

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_Convergence_finite_E2_q0
universe u
noncomputable section

Lean source · statement

theorem _root_.DoubleComplex.Convergence.finite_E2_q0 {R : Type u} [CommRing R] [IsNoetherianRing R]
    {E₂ : ℕ → ℕ → Type u} [∀ p q, AddCommGroup (E₂ p q)] [∀ p q, Module R (E₂ p q)]
    {H : ℕ → Type u} [∀ n, AddCommGroup (H n)] [∀ n, Module R (H n)] {N : ℕ}
    (conv : DoubleComplex.Convergence R E₂ H N)
    (hH : ∀ n, Module.Finite R (H n)) (hE₂ : ∀ p q, 1 ≤ q → Module.Finite R (E₂ p q))
    (p : ℕ) (hp : p ≤ N) : Module.Finite R (E₂ p 0)

Module documentation

Declarations

subquot_finite

filt_finite

finite_E2_q0

finite_E2_q0