Module

Module_exists_projective_complex_quasiIso_of_flat_complex.lean

Nyll.AlgebraicCurves.Foundations.HomologicalAlgebra.Module_exists_projective_complex_quasiIso_of_flat_complex

73 declarations indexed from sourceView source ↗

Module documentation

Module exists projective complex quasi Iso of flat complex

Imports7

Mathlib.LinearAlgebra.TensorProduct.Prod
Mathlib.RingTheory.Flat.EquationalCriterion
Mathlib.Tactic.Abel
Mathlib.Tactic.Choose
Mathlib.Tactic.Ext
Mathlib.Tactic.SplitIfs
Nyll.SchemeTheory.RingTheory.Flat.Kernel

Imported by4

def

W

L38 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.W

Documentation

The submodule of sequences supported below the given finite bound.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]

Lean source · full declaration

def W (R : Type u) [CommRing R] (m : ℕ) : Submodule R (ℕ → R) where
  carrier := {f | ∀ k, m ≤ k → f k = 0}
  zero_mem' := fun _ _ => rfl
  add_mem' := fun {f g} hf hg k hk => by
    change f k + g k = 0
    rw [hf k hk, hg k hk, add_zero]
  smul_mem' := fun a f hf k hk => by
    change a * f k = 0
    rw [hf k hk, mul_zero]

theorem

mem_W

L48 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.mem_W

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]

Lean source · statement

theorem mem_W {m : ℕ} {f : ℕ → R} : f ∈ W R m ↔ ∀ k, m ≤ k → f k = 0

def

πv

L51 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.πv

Documentation

Restriction of a sequence to its first finitely many coordinates.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]

Lean source · statement

def πv (m : ℕ) : (ℕ → R) →ₗ[R] (Fin m → R)

theorem

πv_apply

L53 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.πv_apply

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]

Lean source · statement

theorem πv_apply (m : ℕ) (f : ℕ → R) (k : Fin m) : πv m f k = f k

def

ιv

L56 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.ιv

Documentation

Extension of a finite tuple by zero outside its index range.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]

Lean source · statement

def ιv (m : ℕ) : (Fin m → R) →ₗ[R] (ℕ → R)

theorem

ιv_apply

L59 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.ιv_apply

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]

Lean source · full declaration

theorem ιv_apply (m : ℕ) (v : Fin m → R) (k : ℕ) :
    ιv m v k = if h : k < m then v ⟨k, h⟩ else 0 := by
  unfold ιv
  rw [LinearMap.pi_apply]
  split_ifs <;> rfl

theorem

ιv_apply_lt

L65 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.ιv_apply_lt

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]

Lean source · statement

theorem ιv_apply_lt (m : ℕ) (v : Fin m → R) (k : Fin m) : ιv m v k = v k

theorem

ιv_mem

L68 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.ιv_mem

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]

Lean source · statement

theorem ιv_mem (m : ℕ) (v : Fin m → R) : ιv m v ∈ W R m

theorem

πv_ιv

L71 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.πv_ιv

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]

Lean source · statement

theorem πv_ιv (m : ℕ) (v : Fin m → R) : πv m (ιv m v) = v

theorem

ιv_πv

L74 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.ιv_πv

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]

Lean source · statement

theorem ιv_πv (m : ℕ) {f : ℕ → R} (hf : f ∈ W R m) : ιv m (πv m f) = f

theorem

ιv_injective

L81 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.ιv_injective

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]

Lean source · statement

theorem ιv_injective (m : ℕ) : Function.Injective (ιv (R := R) m)

theorem

eq_zero_of_mem_W_zero

L84 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.eq_zero_of_mem_W_zero

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]

Lean source · statement

theorem eq_zero_of_mem_W_zero {f : ℕ → R} (hf : f ∈ W R 0) : f = 0

def

lc

L88 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.lc

Documentation

The linear combination map associated with a finite family of module elements.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]

Lean source · statement

def lc {M : Type u} [AddCommGroup M] [Module R M] {r : ℕ} (v : Fin r → M) : (Fin r → R) →ₗ[R] M

theorem

lc_apply

L91 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.lc_apply

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]

Lean source · statement

theorem lc_apply {M : Type u} [AddCommGroup M] [Module R M] {r : ℕ} (v : Fin r → M) (a : Fin r →
  R) :
    lc v a = ∑ k : Fin r, a k • v k

theorem

lc_append_apply

L98 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.lc_append_apply

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]

Lean source · statement

theorem lc_append_apply {M : Type u} [AddCommGroup M] [Module R M] {r s : ℕ} (v : Fin r → M) (w :
  Fin s → M)
    (a : Fin r → R) (b : Fin s → R) :
    lc (Fin.append v w) (Fin.append a b) = (∑ k : Fin r, a k • v k) + ∑ l : Fin s, b l • w l

theorem

map_lc

L105 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.map_lc

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]

Lean source · full declaration

theorem map_lc {M N : Type u} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {r : ℕ}
    (g : M →ₗ[R] N) (v : Fin r → M) (a : Fin r → R) : g (lc v a) = lc (fun k => g (v k)) a := by
  rw [lc_apply, lc_apply, map_sum]
  simp only [map_smul]

structure

Stage

L114 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage

Documentation

A finite free approximation above a degree bound, inducing the required homology comparison.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  (d : ∀ i, C i →ₗ[R] C (i + 1)) (n : ℕ)

Lean source · full declaration

structure Stage (b : ℕ) where
  /-- The finite rank chosen at each degree. -/
  m : ℕ → ℕ
  /-- The differentials on the ambient sequence modules. -/
  gδ : ℕ → ((ℕ → R) →ₗ[R] (ℕ → R))
  /-- The comparison maps from ambient sequences to the original complex. -/
  gφ : ∀ j, (ℕ → R) →ₗ[R] C j
  /-- The ranks vanish above the original complex bound. -/
  bdd : ∀ j, n < j → m j = 0
  /-- The differentials preserve the finite-support bounds. -/
  maps : ∀ j, b ≤ j → ∀ f ∈ W R (m j), gδ j f ∈ W R (m (j + 1))
  /-- Two consecutive differentials compose to zero above the stage bound. -/
  dd : ∀ j, b ≤ j → ∀ f ∈ W R (m j), gδ (j + 1) (gδ j f) = 0
  /-- The comparison maps commute with the differentials above the stage bound. -/
  chain : ∀ j, b ≤ j → ∀ f ∈ W R (m j), d j (gφ j f) = gφ (j + 1) (gδ j f)
  /-- Cycles mapping to boundaries are boundaries in the approximation. -/
  inj : ∀ j, b ≤ j → ∀ f ∈ W R (m (j + 1)), gδ (j + 1) f = 0 →
    gφ (j + 1) f ∈ LinearMap.range (d j) → ∃ g ∈ W R (m j), gδ j g = f
  /-- Every original cycle is represented up to a boundary by an approximation cycle. -/
  surj : ∀ j, b ≤ j + 1 → ∀ y : C (j + 1), d (j + 1) y = 0 →
    ∃ f ∈ W R (m (j + 1)), gδ (j + 1) f = 0 ∧ gφ (j + 1) f - y ∈ LinearMap.range (d j)

def

base

L139 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.base

Documentation

The zero approximation above the bound where the original complex vanishes.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  (d : ∀ i, C i →ₗ[R] C (i + 1)) (n : ℕ)
variable {C d n}

Lean source · full declaration

def Stage.base (hbdd : ∀ i, n < i → Subsingleton (C i)) : Stage C d n (n + 1) where
  m := fun _ => 0
  gδ := fun _ => 0
  gφ := fun _ => 0
  bdd := fun _ _ => rfl
  maps := fun _ _ _ _ => by rw [LinearMap.zero_apply]; exact Submodule.zero_mem _
  dd := fun _ _ _ _ => by simp
  chain := fun _ _ _ _ => by simp
  inj := fun j _ f hf _ _ => ⟨0, Submodule.zero_mem _, by
    rw [LinearMap.zero_apply, eq_zero_of_mem_W_zero hf]⟩
  surj := fun j hj y _ => by
    have := hbdd (j + 1) (Nat.lt_of_succ_le hj)
    refine ⟨0, Submodule.zero_mem _, by rw [LinearMap.zero_apply], ?_⟩
    rw [LinearMap.zero_apply, Subsingleton.elim y 0, sub_zero]
    exact Submodule.zero_mem _

theorem

nonempty_step

L159 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.nonempty_step

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  (d : ∀ i, C i →ₗ[R] C (i + 1)) (n : ℕ)
variable {C d n}
section Step
variable [IsNoetherianRing R]

Lean source · statement

theorem Stage.nonempty_step
    (hfin : ∀ i, Module.Finite R
      (LinearMap.ker (d (i + 1)) ⧸ (LinearMap.range (d i)).comap (LinearMap.ker (d (i +
        1))).subtype))
    (p : ℕ) (hp : p < n) (S : Stage C d n (p + 1 + 1)) : Nonempty (Stage C d n (p + 1))

theorem

nonempty_descend

L288 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.nonempty_descend

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  (d : ∀ i, C i →ₗ[R] C (i + 1)) (n : ℕ)
variable {C d n}

Lean source · statement

theorem Stage.nonempty_descend [IsNoetherianRing R] (hbdd : ∀ i, n < i → Subsingleton (C i))
    (hfin : ∀ i, Module.Finite R
      (LinearMap.ker (d (i + 1)) ⧸ (LinearMap.range (d i)).comap (LinearMap.ker (d (i +
        1))).subtype)) :
    Nonempty (Stage C d n 1)

abbrev

K

L310 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.K

Documentation

The finite free module at the given degree of the approximation.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Small
variable (S : Stage C d n 1)

Lean source · statement

abbrev Stage.K (i : ℕ) : Type u

def

δs

L313 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.δs

Documentation

The stage differential restricted to the finite coordinate modules.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Small
variable (S : Stage C d n 1)

Lean source · statement

def Stage.δs (i : ℕ) : S.K i →ₗ[R] S.K (i + 1)

def

φs

L316 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.φs

Documentation

The comparison map from the finite coordinate module to the original complex.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Small
variable (S : Stage C d n 1)

Lean source · statement

def Stage.φs (i : ℕ) : S.K i →ₗ[R] C i

theorem

δs_apply

L318 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.δs_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Small
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.δs_apply (i : ℕ) (v : S.K i) : S.δs i v = πv (S.m (i + 1)) (S.gδ i (ιv (S.m i) v))

theorem

φs_apply

L321 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.φs_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Small
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.φs_apply (i : ℕ) (v : S.K i) : S.φs i v = S.gφ i (ιv (S.m i) v)

theorem

ιv_δs

L323 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.ιv_δs

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Small
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.ιv_δs {i : ℕ} (hi : 1 ≤ i) (v : S.K i) :
    ιv (S.m (i + 1)) (S.δs i v) = S.gδ i (ιv (S.m i) v)

theorem

δs_δs

L327 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.δs_δs

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Small
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.δs_δs {i : ℕ} (hi : 1 ≤ i) (v : S.K i) : S.δs (i + 1) (S.δs i v) = 0

theorem

d_φs

L330 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.d_φs

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Small
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.d_φs {i : ℕ} (hi : 1 ≤ i) (v : S.K i) : d i (S.φs i v) = S.φs (i + 1) (S.δs i v)

theorem

s_inj

L333 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.s_inj

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Small
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.s_inj {i : ℕ} (hi : 1 ≤ i) (v : S.K (i + 1)) (hδ : S.δs (i + 1) v = 0)
    (hφ : S.φs (i + 1) v ∈ LinearMap.range (d i)) : ∃ w : S.K i, S.δs i w = v

theorem

s_surj

L341 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.s_surj

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Small
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.s_surj (i : ℕ) (y : C (i + 1)) (hy : d (i + 1) y = 0) :
    ∃ v : S.K (i + 1), S.δs (i + 1) v = 0 ∧ S.φs (i + 1) v - y ∈ LinearMap.range (d i)

abbrev

G

L349 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.G

Documentation

The product of the next approximation module with the current original module.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Small
variable (S : Stage C d n 1)

Lean source · statement

abbrev Stage.G (i : ℕ) : Type u

def

Δ

L353 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.Δ

Documentation

The differential combining the stage differential with the difference of the comparison maps.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Small
variable (S : Stage C d n 1)

Lean source · statement

def Stage.Δ (i : ℕ) : S.G i →ₗ[R] S.G (i + 1)

theorem

Δ_apply

L357 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.Δ_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Small
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.Δ_apply (i : ℕ) (v : S.K (i + 1)) (c : C i) :
    S.Δ i (v, c) = (S.δs (i + 1) v, S.φs (i + 1) v - d i c)

theorem

Δ_Δ

L363 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.Δ_Δ

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Small
variable (S : Stage C d n 1)
variable (hdd : ∀ i, d (i + 1) ∘ₗ d i = 0)
include hdd in

Lean source · statement

theorem Stage.Δ_Δ (i : ℕ) (x : S.G i) : S.Δ (i + 1) (S.Δ i x) = 0

theorem

Δ_exact

L371 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.Δ_exact

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Small
variable (S : Stage C d n 1)
variable (hdd : ∀ i, d (i + 1) ∘ₗ d i = 0)

Lean source · statement

theorem Stage.Δ_exact (i : ℕ) (x : S.G (i + 1)) (hx : S.Δ (i + 1) x = 0) : x ∈ LinearMap.range
  (S.Δ i)

theorem

flat_prod

L386 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.flat_prod

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Small
variable (S : Stage C d n 1)
variable (hdd : ∀ i, d (i + 1) ∘ₗ d i = 0)

Lean source · statement

theorem flat_prod (M N : Type u) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
    [Module.Flat R M] [Module.Flat R N] : Module.Flat R (M × N)

theorem

flat_ker_Δ

L408 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.flat_ker_Δ

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Small
variable (S : Stage C d n 1)
variable (hdd : ∀ i, d (i + 1) ∘ₗ d i = 0)
variable [IsNoetherianRing R] [∀ i, Module.Flat R (C i)]
include hdd in
omit [IsNoetherianRing R] in

Lean source · statement

theorem Stage.flat_ker_Δ (hbdd : ∀ i, n < i → Subsingleton (C i)) (i : ℕ) :
    Module.Flat R (LinearMap.ker (S.Δ i))

abbrev

Z0

L455 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.Z0

Documentation

The degree-zero kernel of the comparison complex.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

abbrev Stage.Z0 : Submodule R (S.G 0)

theorem

mem_Z0

L457 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.mem_Z0

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.mem_Z0 (v : S.K 1) (c : C 0) : (v, c) ∈ S.Z0 ↔ S.δs 1 v = 0 ∧ S.φs 1 v = d 0 c

theorem

finite_Z0

L460 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.finite_Z0

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.finite_Z0 [IsNoetherianRing R] (hfin0 : Module.Finite R (LinearMap.ker (d 0))) :
    Module.Finite R S.Z0

theorem

projective_Z0

L485 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.projective_Z0

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.projective_Z0 [IsNoetherianRing R] [∀ i, Module.Flat R (C i)]
    (hdd : ∀ i, d (i + 1) ∘ₗ d i = 0) (hbdd : ∀ i, n < i → Subsingleton (C i))
    (hfin0 : Module.Finite R (LinearMap.ker (d 0))) : Module.Projective R S.Z0

abbrev

U

L494 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.U

Documentation

The ambient product containing the module of the corrected approximation.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

abbrev Stage.U (i : ℕ) : Type u

def

Sfin

L497 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.Sfin

Documentation

The corrected approximation submodule, using the comparison kernel in degree zero.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · full declaration

def Stage.Sfin : (i : ℕ) → Submodule R (S.U i)
  | 0 => LinearMap.range (LinearMap.inr R (S.K 0) (S.G 0) ∘ₗ S.Z0.subtype)
  | (j + 1) => LinearMap.range (LinearMap.inl R (S.K (j + 1)) (S.G (j + 1)))

theorem

Sfin_zero

L501 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.Sfin_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.Sfin_zero : S.Sfin 0 = LinearMap.range (LinearMap.inr R (S.K 0) (S.G 0) ∘ₗ
  S.Z0.subtype)

theorem

Sfin_succ

L504 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.Sfin_succ

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.Sfin_succ (j : ℕ) : S.Sfin (j + 1) = LinearMap.range (LinearMap.inl R (S.K (j + 1))
  (S.G (j + 1)))

theorem

mem_Sfin_zero

L507 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.mem_Sfin_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.mem_Sfin_zero {x : S.U 0} : x ∈ S.Sfin 0 ↔ x.1 = 0 ∧ x.2 ∈ S.Z0

theorem

mem_Sfin_succ

L513 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.mem_Sfin_succ

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.mem_Sfin_succ {j : ℕ} {x : S.U (j + 1)} : x ∈ S.Sfin (j + 1) ↔ x.2 = 0

abbrev

KK

L520 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.KK

Documentation

The module underlying the corrected approximation submodule.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

abbrev Stage.KK (i : ℕ) : Type u

def

AΔ

L523 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.AΔ

Documentation

The ambient differential used to construct the corrected approximation.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

def Stage.AΔ (i : ℕ) : S.U i →ₗ[R] S.U (i + 1)

theorem

AΔ_apply

L527 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.AΔ_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.AΔ_apply (i : ℕ) (x : S.U i) : S.AΔ i x = (S.δs i x.1 + x.2.1, 0)

theorem

AΔ_mem

L529 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.AΔ_mem

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.AΔ_mem (i : ℕ) (x : S.U i) : S.AΔ i x ∈ S.Sfin (i + 1)

def

δK

L533 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.δK

Documentation

The ambient differential restricted to the corrected approximation submodules.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

def Stage.δK (i : ℕ) : S.KK i →ₗ[R] S.KK (i + 1)

theorem

δK_val

L536 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.δK_val

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.δK_val (i : ℕ) (x : S.KK i) : ((S.δK i x : S.KK (i + 1)) : S.U (i + 1)) = (S.δs i
  x.1.1 + x.1.2.1, 0)

def

Aφ

L540 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.Aφ

Documentation

The ambient comparison map obtained by adding the two original-complex components.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

def Stage.Aφ (i : ℕ) : S.U i →ₗ[R] C i

def

φK

L544 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.φK

Documentation

The comparison map restricted to the corrected approximation module.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

def Stage.φK (i : ℕ) : S.KK i →ₗ[R] C i

theorem

φK_apply

L546 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.φK_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.φK_apply (i : ℕ) (x : S.KK i) : S.φK i x = S.φs i x.1.1 + x.1.2.2

theorem

finite_KK

L548 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.finite_KK

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.finite_KK [IsNoetherianRing R] (hfin0 : Module.Finite R (LinearMap.ker (d 0))) (i :
  ℕ) :
    Module.Finite R (S.KK i)

theorem

projective_KK

L560 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.projective_KK

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.projective_KK [IsNoetherianRing R] [∀ i, Module.Flat R (C i)]
    (hdd : ∀ i, d (i + 1) ∘ₗ d i = 0) (hbdd : ∀ i, n < i → Subsingleton (C i))
    (hfin0 : Module.Finite R (LinearMap.ker (d 0))) (i : ℕ) : Module.Projective R (S.KK i)

theorem

subsingleton_KK

L574 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.subsingleton_KK

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.subsingleton_KK {i : ℕ} (hi : n < i) : Subsingleton (S.KK i)

theorem

δK_δK_zero

L584 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.δK_δK_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.δK_δK_zero (x : S.KK 0) : S.δK 1 (S.δK 0 x) = 0

theorem

δK_δK_succ

L595 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.δK_δK_succ

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.δK_δK_succ (j : ℕ) (x : S.KK (j + 1)) : S.δK (j + 1 + 1) (S.δK (j + 1) x) = 0

theorem

δK_δK

L605 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.δK_δK

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.δK_δK (i : ℕ) : S.δK (i + 1) ∘ₗ S.δK i = 0

theorem

d_φK_zero

L612 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.d_φK_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.d_φK_zero (x : S.KK 0) : d 0 (S.φK 0 x) = S.φK 1 (S.δK 0 x)

theorem

d_φK_succ

L620 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.d_φK_succ

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.d_φK_succ (j : ℕ) (x : S.KK (j + 1)) :
    d (j + 1) (S.φK (j + 1) x) = S.φK (j + 1 + 1) (S.δK (j + 1) x)

theorem

d_φK

L629 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.d_φK

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.d_φK (i : ℕ) : d i ∘ₗ S.φK i = S.φK (i + 1) ∘ₗ S.δK i

theorem

h0inj

L636 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.h0inj

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.h0inj (x : S.KK 0) (hδ : S.δK 0 x = 0) (hφ : S.φK 0 x = 0) : x = 0

theorem

h0surj

L648 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.h0surj

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.h0surj (y : C 0) (hy : d 0 y = 0) : ∃ x : S.KK 0, S.δK 0 x = 0 ∧ S.φK 0 x = y

theorem

hKinj_aux

L657 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.hKinj_aux

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.hKinj_aux (i : ℕ) (x : S.KK (i + 1)) (hδ : S.δK (i + 1) x = 0) :
    x.1.2 = 0 ∧ S.δs (i + 1) x.1.1 = 0 ∧ S.φK (i + 1) x = S.φs (i + 1) x.1.1

theorem

hKinj_zero

L668 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.hKinj_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.hKinj_zero (x : S.KK 1) (hδ : S.δK 1 x = 0)
    (hφ : S.φK 1 x ∈ LinearMap.range (d 0)) : x ∈ LinearMap.range (S.δK 0)

theorem

hKinj_succ

L680 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.hKinj_succ

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.hKinj_succ (j : ℕ) (x : S.KK (j + 1 + 1)) (hδ : S.δK (j + 1 + 1) x = 0)
    (hφ : S.φK (j + 1 + 1) x ∈ LinearMap.range (d (j + 1))) : x ∈ LinearMap.range (S.δK (j + 1))

theorem

hKinj

L692 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.hKinj

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.hKinj (i : ℕ) (x : S.KK (i + 1)) (hδ : S.δK (i + 1) x = 0)
    (hφ : S.φK (i + 1) x ∈ LinearMap.range (d i)) : x ∈ LinearMap.range (S.δK i)

theorem

hKsurj

L698 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement.MumfordModel.Stage.hKsurj

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
namespace MumfordModel
variable {R : Type u} [CommRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  {d : ∀ i, C i →ₗ[R] C (i + 1)} {n : ℕ}
section Final
variable (S : Stage C d n 1)

Lean source · statement

theorem Stage.hKsurj (i : ℕ) (y : C (i + 1)) (hy : d (i + 1) y = 0) :
    ∃ x : S.KK (i + 1), S.δK (i + 1) x = 0 ∧ S.φK (i + 1) x - y ∈ LinearMap.range (d i)

theorem

exists_projective_complex_quasiIso_of_flat_complex

L714 ↗

Module.exists_projective_complex_quasiIso_of_flat_complex

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.ProjectiveReplacement
universe u
open TensorProduct
open MumfordModel in

Lean source · statement

theorem _root_.Module.exists_projective_complex_quasiIso_of_flat_complex
    (R : Type u) [CommRing R] [IsNoetherianRing R]
    (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)] [∀ i, Module.Flat R (C i)]
    (d : ∀ i, C i →ₗ[R] C (i + 1)) (hdd : ∀ i, d (i + 1) ∘ₗ d i = 0)
    (n : ℕ) (hbdd : ∀ i, n < i → Subsingleton (C i))
    (hfin0 : Module.Finite R (LinearMap.ker (d 0)))
    (hfin : ∀ i, Module.Finite R
      (LinearMap.ker (d (i + 1)) ⧸ (LinearMap.range (d i)).comap (LinearMap.ker (d (i +
        1))).subtype)) :
    ∃ (K : ℕ → Type u) (_ : ∀ i, AddCommGroup (K i)) (_ : ∀ i, Module R (K i))
      (_ : ∀ i, Module.Finite R (K i)) (_ : ∀ i, Module.Projective R (K i))
      (δ : ∀ i, K i →ₗ[R] K (i + 1)) (_ : ∀ i, δ (i + 1) ∘ₗ δ i = 0) (_ : ∀ i, n < i →
        Subsingleton (K i))
      (φ : ∀ i, K i →ₗ[R] C i) (_ : ∀ i, d i ∘ₗ φ i = φ (i + 1) ∘ₗ δ i),
      (∀ x : K 0, δ 0 x = 0 → φ 0 x = 0 → x = 0) ∧
      (∀ y : C 0, d 0 y = 0 → ∃ x : K 0, δ 0 x = 0 ∧ φ 0 x = y) ∧
      (∀ (i : ℕ) (x : K (i + 1)), δ (i + 1) x = 0 → φ (i + 1) x ∈ LinearMap.range (d i) →
        x ∈ LinearMap.range (δ i)) ∧
      (∀ (i : ℕ) (y : C (i + 1)), d (i + 1) y = 0 →
        ∃ x : K (i + 1), δ (i + 1) x = 0 ∧ φ (i + 1) x - y ∈ LinearMap.range (d i))

Module documentation

Module exists projective complex quasi Iso of flat complex

Declarations