Module

Module_exists_mumfordTruncation_of_flat_complex.lean

Nyll.AlgebraicCurves.Foundations.HomologicalAlgebra.Module_exists_mumfordTruncation_of_flat_complex

32 declarations indexed from sourceView source ↗

Module documentation

Module exists mumford Truncation of flat complex

Imports4

Imported by2

theorem

subtype_baseChange_injective

L49 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.subtype_baseChange_injective

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section ThreeStep
variable {R : Type u} [CommRing R]
variable {C0 C1 C2 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2]
variable (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hsq : d1 ∘ₗ d0 = 0)
variable [Module.Finite R (C2 ⧸ LinearMap.range d1)]

Lean source · statement

theorem subtype_baseChange_injective [Module.Flat R C2] (A : Type u) [CommRing A] [Algebra R A] :
    Function.Injective ((K0 d1).subtype.baseChange A)

theorem

prodRight_apply_eq_baseChange

L55 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.prodRight_apply_eq_baseChange

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section ThreeStep
variable {R : Type u} [CommRing R]
variable {C0 C1 C2 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2]
variable (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hsq : d1 ∘ₗ d0 = 0)
variable [Module.Finite R (C2 ⧸ LinearMap.range d1)]

Lean source · statement

theorem prodRight_apply_eq_baseChange (A : Type u) [CommRing A] [Algebra R A] {M N : Type u}
    [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (w : A ⊗[R] (M × N)) :
    (TensorProduct.prodRight R A A M N) w
      = (((LinearMap.fst R M N).baseChange A) w, ((LinearMap.snd R M N).baseChange A) w)

theorem

prodRight_subtype_baseChange

L63 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.prodRight_subtype_baseChange

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section ThreeStep
variable {R : Type u} [CommRing R]
variable {C0 C1 C2 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2]
variable (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hsq : d1 ∘ₗ d0 = 0)
variable [Module.Finite R (C2 ⧸ LinearMap.range d1)]

Lean source · statement

theorem prodRight_subtype_baseChange (A : Type u) [CommRing A] [Algebra R A] (z : A ⊗[R] K0 d1) :
    (TensorProduct.prodRight R A A C1 (Fin (rank d1) → R)) (((K0 d1).subtype.baseChange A) z)
      = (((ι0 d1).baseChange A) z, ((dK d1).baseChange A) z)

theorem

coprod_baseChange_apply

L75 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.coprod_baseChange_apply

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section ThreeStep
variable {R : Type u} [CommRing R]
variable {C0 C1 C2 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2]
variable (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hsq : d1 ∘ₗ d0 = 0)
variable [Module.Finite R (C2 ⧸ LinearMap.range d1)]

Lean source · statement

theorem coprod_baseChange_apply (A : Type u) [CommRing A] [Algebra R A]
    (w : A ⊗[R] (C1 × (Fin (rank d1) → R))) :
    ((d1.coprod (lift d1)).baseChange A) w
      = (d1.baseChange A) ((TensorProduct.prodRight R A A C1 (Fin (rank d1) → R)) w).1
        + ((lift d1).baseChange A) ((TensorProduct.prodRight R A A C1 (Fin (rank d1) → R)) w).2

def

stepDiff

L86 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.stepDiff

Documentation

The differential of the truncation step, with codomain restricted to the comparison kernel.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section ThreeStep
variable {R : Type u} [CommRing R]
variable {C0 C1 C2 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2]
variable (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hsq : d1 ∘ₗ d0 = 0)
variable [Module.Finite R (C2 ⧸ LinearMap.range d1)]

Lean source · statement

def stepDiff : C0 →ₗ[R] K0 d1

theorem

stepDiff_coe

L92 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.stepDiff_coe

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section ThreeStep
variable {R : Type u} [CommRing R]
variable {C0 C1 C2 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2]
variable (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hsq : d1 ∘ₗ d0 = 0)
variable [Module.Finite R (C2 ⧸ LinearMap.range d1)]

Lean source · statement

theorem stepDiff_coe (y : C0) :
    ((stepDiff d0 d1 hsq y : K0 d1) : C1 × (Fin (rank d1) → R)) = (d0 y, 0)

theorem

subtype_comp_stepDiff

L95 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.subtype_comp_stepDiff

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section ThreeStep
variable {R : Type u} [CommRing R]
variable {C0 C1 C2 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2]
variable (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hsq : d1 ∘ₗ d0 = 0)
variable [Module.Finite R (C2 ⧸ LinearMap.range d1)]

Lean source · statement

theorem subtype_comp_stepDiff : (K0 d1).subtype ∘ₗ stepDiff d0 d1 hsq = (LinearMap.inl R C1 _) ∘ₗ
  d0

theorem

dK_comp_stepDiff

L98 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.dK_comp_stepDiff

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section ThreeStep
variable {R : Type u} [CommRing R]
variable {C0 C1 C2 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2]
variable (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hsq : d1 ∘ₗ d0 = 0)
variable [Module.Finite R (C2 ⧸ LinearMap.range d1)]

Lean source · statement

theorem dK_comp_stepDiff : dK d1 ∘ₗ stepDiff d0 d1 hsq = 0

theorem

stepDiff_ker

L101 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.stepDiff_ker

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section ThreeStep
variable {R : Type u} [CommRing R]
variable {C0 C1 C2 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2]
variable (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hsq : d1 ∘ₗ d0 = 0)
variable [Module.Finite R (C2 ⧸ LinearMap.range d1)]

Lean source · statement

theorem stepDiff_ker : LinearMap.ker (stepDiff d0 d1 hsq) = LinearMap.ker d0

theorem

stepDiff_ker_baseChange

L107 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.stepDiff_ker_baseChange

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section ThreeStep
variable {R : Type u} [CommRing R]
variable {C0 C1 C2 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2]
variable (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hsq : d1 ∘ₗ d0 = 0)
variable [Module.Finite R (C2 ⧸ LinearMap.range d1)]

Lean source · statement

theorem stepDiff_ker_baseChange [Module.Flat R C2] (A : Type u) [CommRing A] [Algebra R A] :
    LinearMap.ker ((stepDiff d0 d1 hsq).baseChange A) = LinearMap.ker (d0.baseChange A)

theorem

ker_dK_baseChange_le

L120 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.ker_dK_baseChange_le

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section ThreeStep
variable {R : Type u} [CommRing R]
variable {C0 C1 C2 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2]
variable (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hsq : d1 ∘ₗ d0 = 0)
variable [Module.Finite R (C2 ⧸ LinearMap.range d1)]

Lean source · statement

theorem ker_dK_baseChange_le [Module.Flat R C2] (A : Type u) [CommRing A] [Algebra R A]
    (hA : LinearMap.ker (d1.baseChange A) ≤ LinearMap.range (d0.baseChange A)) :
    LinearMap.ker ((dK d1).baseChange A) ≤ LinearMap.range ((stepDiff d0 d1 hsq).baseChange A)

def

kerToK0

L139 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.kerToK0

Documentation

The map from the original kernel into the kernel used in the truncation step.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section ThreeStep
variable {R : Type u} [CommRing R]
variable {C0 C1 C2 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2]
variable (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hsq : d1 ∘ₗ d0 = 0)
variable [Module.Finite R (C2 ⧸ LinearMap.range d1)]

Lean source · statement

def kerToK0 : LinearMap.ker d1 →ₗ[R] K0 d1

theorem

dK_comp_kerToK0

L147 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.dK_comp_kerToK0

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section ThreeStep
variable {R : Type u} [CommRing R]
variable {C0 C1 C2 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2]
variable (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hsq : d1 ∘ₗ d0 = 0)
variable [Module.Finite R (C2 ⧸ LinearMap.range d1)]

Lean source · statement

theorem dK_comp_kerToK0 : dK d1 ∘ₗ kerToK0 d1 = 0

def

h1ToCoker

L152 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.h1ToCoker

Documentation

The induced map from the original homology quotient to the cokernel of the truncation differential.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section ThreeStep
variable {R : Type u} [CommRing R]
variable {C0 C1 C2 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2]
variable (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hsq : d1 ∘ₗ d0 = 0)
variable [Module.Finite R (C2 ⧸ LinearMap.range d1)]

Lean source · statement

def h1ToCoker :
    (LinearMap.ker d1 ⧸ (LinearMap.range d0).comap (LinearMap.ker d1).subtype) →ₗ[R]
      (K0 d1 ⧸ LinearMap.range (stepDiff d0 d1 hsq))

def

cokerToFree

L163 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.cokerToFree

Documentation

The map from the truncation cokernel to the selected finite free module.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section ThreeStep
variable {R : Type u} [CommRing R]
variable {C0 C1 C2 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2]
variable (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hsq : d1 ∘ₗ d0 = 0)
variable [Module.Finite R (C2 ⧸ LinearMap.range d1)]

Lean source · statement

def cokerToFree : (K0 d1 ⧸ LinearMap.range (stepDiff d0 d1 hsq)) →ₗ[R] (Fin (rank d1) → R)

theorem

h1ToCoker_exact

L166 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.h1ToCoker_exact

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section ThreeStep
variable {R : Type u} [CommRing R]
variable {C0 C1 C2 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2]
variable (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hsq : d1 ∘ₗ d0 = 0)
variable [Module.Finite R (C2 ⧸ LinearMap.range d1)]

Lean source · statement

theorem h1ToCoker_exact :
    LinearMap.range (h1ToCoker d0 d1 hsq) = LinearMap.ker (cokerToFree d0 d1 hsq)

theorem

stepDiff_coker_finite

L190 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.stepDiff_coker_finite

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section ThreeStep
variable {R : Type u} [CommRing R]
variable {C0 C1 C2 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2]
variable (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hsq : d1 ∘ₗ d0 = 0)
variable [Module.Finite R (C2 ⧸ LinearMap.range d1)]
variable [IsNoetherianRing R]

Lean source · statement

theorem stepDiff_coker_finite
    [Module.Finite R (LinearMap.ker d1 ⧸ (LinearMap.range d0).comap (LinearMap.ker d1).subtype)] :
    Module.Finite R (K0 d1 ⧸ LinearMap.range (stepDiff d0 d1 hsq))

structure

TruncInvariant

L214 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.TruncInvariant

Documentation

A flat replacement at one degree preserving the differential kernel after every algebra base change.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section Downward
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)] [∀ i, Module.Flat R (C i)]
variable (d : ∀ i, C i →ₗ[R] C (i + 1)) (hdd : ∀ i, d (i + 1) ∘ₗ d i = 0)
variable (hfin : ∀ i, Module.Finite R
    (LinearMap.ker (d (i + 1)) ⧸ (LinearMap.range (d i)).comap (LinearMap.ker (d (i + 1))).subtype))

Lean source · full declaration

structure TruncInvariant (p : ℕ) where
  /-- The replacement module at this degree. -/
  K : Type u
  /-- The additive group structure on the replacement module. -/
  [K_acg : AddCommGroup K]
  /-- The module structure on the replacement. -/
  [K_mod : Module R K]
  /-- Flatness of the replacement module. -/
  [K_flat : Module.Flat R K]
  /-- The replacement differential. -/
  d' : C p →ₗ[R] K
  /-- Finite generation of the cokernel of the replacement differential. -/
  [coker_fin : Module.Finite R (K ⧸ LinearMap.range d')]
  /-- Equality of the replacement kernel with the original differential kernel. -/
  hker : LinearMap.ker d' = LinearMap.ker (d p)
  /-- Preservation of the kernel comparison after every algebra base change. -/
  hkerA : ∀ (A : Type u) [CommRing A] [Algebra R A],
    LinearMap.ker (d'.baseChange A) = LinearMap.ker ((d p).baseChange A)

def

truncInvariantBase

L237 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.truncInvariantBase

Documentation

The truncation invariant at the degree where the following term is zero.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section Downward
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)] [∀ i, Module.Flat R (C i)]
variable (d : ∀ i, C i →ₗ[R] C (i + 1)) (hdd : ∀ i, d (i + 1) ∘ₗ d i = 0)
variable (hfin : ∀ i, Module.Finite R
    (LinearMap.ker (d (i + 1)) ⧸ (LinearMap.range (d i)).comap (LinearMap.ker (d (i + 1))).subtype))
attribute [scoped instance] TruncInvariant.K_acg TruncInvariant.K_mod TruncInvariant.K_flat
  TruncInvariant.coker_fin

Lean source · full declaration

def truncInvariantBase (N : ℕ) [Subsingleton (C (N + 1))] : TruncInvariant C d N where
  K := C (N + 1)
  d' := d N
  coker_fin := Module.Finite.of_surjective (LinearMap.range (d N)).mkQ (Submodule.mkQ_surjective _)
  hker := rfl
  hkerA := fun _ _ _ => rfl

def

truncInvariantStep

L246 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.truncInvariantStep

Documentation

The preceding-degree truncation invariant obtained from the next-degree replacement.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section Downward
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)] [∀ i, Module.Flat R (C i)]
variable (d : ∀ i, C i →ₗ[R] C (i + 1)) (hdd : ∀ i, d (i + 1) ∘ₗ d i = 0)
variable (hfin : ∀ i, Module.Finite R
    (LinearMap.ker (d (i + 1)) ⧸ (LinearMap.range (d i)).comap (LinearMap.ker (d (i + 1))).subtype))
attribute [scoped instance] TruncInvariant.K_acg TruncInvariant.K_mod TruncInvariant.K_flat
  TruncInvariant.coker_fin
include hdd hfin in

Lean source · statement

def truncInvariantStep (p : ℕ) (hP : TruncInvariant C d (p + 1)) : TruncInvariant C d p

def

truncInvariantFrom

L273 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.truncInvariantFrom

Documentation

The truncation invariant constructed by descending induction from a vanishing degree.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section Downward
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)] [∀ i, Module.Flat R (C i)]
variable (d : ∀ i, C i →ₗ[R] C (i + 1)) (hdd : ∀ i, d (i + 1) ∘ₗ d i = 0)
variable (hfin : ∀ i, Module.Finite R
    (LinearMap.ker (d (i + 1)) ⧸ (LinearMap.range (d i)).comap (LinearMap.ker (d (i + 1))).subtype))
attribute [scoped instance] TruncInvariant.K_acg TruncInvariant.K_mod TruncInvariant.K_flat
  TruncInvariant.coker_fin
include hdd hfin in

Lean source · statement

def truncInvariantFrom (N : ℕ) [Subsingleton (C (N + 1))] (q : ℕ) (hq : q ≤ N) : TruncInvariant C d
  q

def

epsK

L290 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.epsK

Documentation

The comparison map restricted to the selected finite free summand.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section LastStep
variable {R : Type u} [CommRing R]
variable {C0 K1 F : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup K1] [Module R K1]
  [AddCommGroup F] [Module R F]
variable (δ : C0 →ₗ[R] K1) (ε : K1 →ₗ[R] F) (hεδ : ε ∘ₗ δ = 0)
variable [Module.Finite R (K1 ⧸ LinearMap.range δ)]

Lean source · statement

def epsK : (Fin (rank δ) → R) →ₗ[R] F

theorem

epsK_comp_dK

L293 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.epsK_comp_dK

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section LastStep
variable {R : Type u} [CommRing R]
variable {C0 K1 F : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup K1] [Module R K1]
  [AddCommGroup F] [Module R F]
variable (δ : C0 →ₗ[R] K1) (ε : K1 →ₗ[R] F) (hεδ : ε ∘ₗ δ = 0)
variable [Module.Finite R (K1 ⧸ LinearMap.range δ)]
include hεδ in

Lean source · statement

theorem epsK_comp_dK : epsK δ ε ∘ₗ dK δ = 0

theorem

mem_range_subtype_baseChange

L296 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.mem_range_subtype_baseChange

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section LastStep
variable {R : Type u} [CommRing R]
variable {C0 K1 F : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup K1] [Module R K1]
  [AddCommGroup F] [Module R F]
variable (δ : C0 →ₗ[R] K1) (ε : K1 →ₗ[R] F) (hεδ : ε ∘ₗ δ = 0)
variable [Module.Finite R (K1 ⧸ LinearMap.range δ)]

Lean source · statement

theorem mem_range_subtype_baseChange (A : Type u) [CommRing A] [Algebra R A]
    (w : A ⊗[R] (C0 × (Fin (rank δ) → R))) :
    ((δ.coprod (lift δ)).baseChange A) w = 0 ↔ ∃ z, ((K0 δ).subtype.baseChange A) z = w

theorem

ker_epsK_baseChange_le

L307 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.ker_epsK_baseChange_le

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section LastStep
variable {R : Type u} [CommRing R]
variable {C0 K1 F : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup K1] [Module R K1]
  [AddCommGroup F] [Module R F]
variable (δ : C0 →ₗ[R] K1) (ε : K1 →ₗ[R] F) (hεδ : ε ∘ₗ δ = 0)
variable [Module.Finite R (K1 ⧸ LinearMap.range δ)]

Lean source · statement

theorem ker_epsK_baseChange_le (A : Type u) [CommRing A] [Algebra R A]
    (hA : LinearMap.ker (ε.baseChange A) ≤ LinearMap.range (δ.baseChange A)) :
    LinearMap.ker ((epsK δ ε).baseChange A) ≤ LinearMap.range ((dK δ).baseChange A)

theorem

kerMap_bijective

L327 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.kerMap_bijective

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section LastStep
variable {R : Type u} [CommRing R]
variable {C0 K1 F : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup K1] [Module R K1]
  [AddCommGroup F] [Module R F]
variable (δ : C0 →ₗ[R] K1) (ε : K1 →ₗ[R] F) (hεδ : ε ∘ₗ δ = 0)
variable [Module.Finite R (K1 ⧸ LinearMap.range δ)]

Lean source · statement

theorem kerMap_bijective : Function.Bijective (kerMap (dK δ) δ (ι0 δ) (ι1 δ) (comm δ))

def

kerMapEquiv

L340 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.kerMapEquiv

Documentation

The kernel equivalence induced by the comparison map in the truncation step.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section LastStep
variable {R : Type u} [CommRing R]
variable {C0 K1 F : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup K1] [Module R K1]
  [AddCommGroup F] [Module R F]
variable (δ : C0 →ₗ[R] K1) (ε : K1 →ₗ[R] F) (hεδ : ε ∘ₗ δ = 0)
variable [Module.Finite R (K1 ⧸ LinearMap.range δ)]

Lean source · statement

def kerMapEquiv : LinearMap.ker (dK δ) ≃ₗ[R] LinearMap.ker δ

theorem

subtype_comp_kerMap

L343 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.subtype_comp_kerMap

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section LastStep
variable {R : Type u} [CommRing R]
variable {C0 K1 F : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup K1] [Module R K1]
  [AddCommGroup F] [Module R F]
variable (δ : C0 →ₗ[R] K1) (ε : K1 →ₗ[R] F) (hεδ : ε ∘ₗ δ = 0)
variable [Module.Finite R (K1 ⧸ LinearMap.range δ)]

Lean source · statement

theorem subtype_comp_kerMap :
    (LinearMap.ker δ).subtype ∘ₗ kerMap (dK δ) δ (ι0 δ) (ι1 δ) (comm δ) = ι0 δ ∘ₗ (LinearMap.ker
      (dK δ)).subtype

theorem

range_subtype_baseChange_eq_ker

L350 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.range_subtype_baseChange_eq_ker

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section LastStep
variable {R : Type u} [CommRing R]
variable {C0 K1 F : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup K1] [Module R K1]
  [AddCommGroup F] [Module R F]
variable (δ : C0 →ₗ[R] K1) (ε : K1 →ₗ[R] F) (hεδ : ε ∘ₗ δ = 0)
variable [Module.Finite R (K1 ⧸ LinearMap.range δ)]
variable [Module.Flat R K1]

Lean source · statement

theorem range_subtype_baseChange_eq_ker (A : Type u) [CommRing A] [Algebra R A]
    (h : LinearMap.range ((LinearMap.ker (dK δ)).subtype.baseChange A) = LinearMap.ker ((dK
      δ).baseChange A)) :
    LinearMap.range ((LinearMap.ker δ).subtype.baseChange A) = LinearMap.ker (δ.baseChange A)

theorem

subtype_baseChange_injective_of

L371 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.subtype_baseChange_injective_of

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section LastStep
variable {R : Type u} [CommRing R]
variable {C0 K1 F : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup K1] [Module R K1]
  [AddCommGroup F] [Module R F]
variable (δ : C0 →ₗ[R] K1) (ε : K1 →ₗ[R] F) (hεδ : ε ∘ₗ δ = 0)
variable [Module.Finite R (K1 ⧸ LinearMap.range δ)]
variable [Module.Flat R K1]

Lean source · statement

theorem subtype_baseChange_injective_of (A : Type u) [CommRing A] [Algebra R A]
    (h : Function.Injective ((LinearMap.ker (dK δ)).subtype.baseChange A)) :
    Function.Injective ((LinearMap.ker δ).subtype.baseChange A)

theorem

finalStep

L429 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_mumfordTruncation_of_flat_complex.TwoChartCech.Mumford.NTerm.finalStep

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace NTerm
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
section FinalStep
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
variable {C0 C1 C2 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2] [Module.Flat R C0] [Module.Flat R C1] [Module.Flat R C2]
variable (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hsq : d1 ∘ₗ d0 = 0)
variable [Module.Finite R (C2 ⧸ LinearMap.range d1)]
variable [Module.Finite R (LinearMap.ker d1 ⧸ (LinearMap.range d0).comap (LinearMap.ker
  d1).subtype)]
include hsq in

Lean source · statement

theorem finalStep (hfin0 : Module.Finite R (LinearMap.ker d0)) :
    ∃ (m₀ m₁ : ℕ) (P : Submodule R (C0 × (Fin m₀ → R))) (ε : (Fin m₀ → R) →ₗ[R] (Fin m₁ → R)),
      Module.Finite R P ∧ Module.Flat R P ∧
      ε ∘ₗ (LinearMap.snd R C0 (Fin m₀ → R) ∘ₗ P.subtype) = 0 ∧
      ∀ (A : Type u) [CommRing A] [Algebra R A],
        (LinearMap.ker (d1.baseChange A) ≤ LinearMap.range (d0.baseChange A) →
          LinearMap.ker (ε.baseChange A)
            ≤ LinearMap.range ((LinearMap.snd R C0 (Fin m₀ → R) ∘ₗ P.subtype).baseChange A)) ∧
        (LinearMap.range ((LinearMap.ker (LinearMap.snd R C0 (Fin m₀ → R) ∘ₗ
          P.subtype)).subtype.baseChange A)
            = LinearMap.ker ((LinearMap.snd R C0 (Fin m₀ → R) ∘ₗ P.subtype).baseChange A) →
          LinearMap.range ((LinearMap.ker d0).subtype.baseChange A) = LinearMap.ker (d0.baseChange
            A)) ∧
        (Function.Injective
            ((LinearMap.ker (LinearMap.snd R C0 (Fin m₀ → R) ∘ₗ P.subtype)).subtype.baseChange A) →
          Function.Injective ((LinearMap.ker d0).subtype.baseChange A))

theorem

exists_mumfordTruncation_of_flat_complex

L491 ↗

Module.exists_mumfordTruncation_of_flat_complex

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_mumfordTruncation_of_flat_complex
universe u
open scoped TensorProduct
open _root_.TwoChartCech.Mumford TwoChartCech.Mumford TwoChartCech.Mumford.NTerm in

Lean source · statement

theorem _root_.Module.exists_mumfordTruncation_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)) :
    ∃ (m₀ m₁ : ℕ) (P : Submodule R (C 0 × (Fin m₀ → R))) (ε : (Fin m₀ → R) →ₗ[R] (Fin m₁ → R)),
      Module.Finite R P ∧ Module.Flat R P ∧
      ε ∘ₗ (LinearMap.snd R (C 0) (Fin m₀ → R) ∘ₗ P.subtype) = 0 ∧
      ∀ (A : Type u) [CommRing A] [Algebra R A],
        (LinearMap.ker ((d 1).baseChange A) ≤ LinearMap.range ((d 0).baseChange A) →
          LinearMap.ker (ε.baseChange A)
            ≤ LinearMap.range ((LinearMap.snd R (C 0) (Fin m₀ → R) ∘ₗ P.subtype).baseChange A)) ∧
        (LinearMap.range ((LinearMap.ker (LinearMap.snd R (C 0) (Fin m₀ → R) ∘ₗ
          P.subtype)).subtype.baseChange A)
            = LinearMap.ker ((LinearMap.snd R (C 0) (Fin m₀ → R) ∘ₗ P.subtype).baseChange A) →
          LinearMap.range ((LinearMap.ker (d 0)).subtype.baseChange A) = LinearMap.ker ((d
            0).baseChange A)) ∧
        (Function.Injective
            ((LinearMap.ker (LinearMap.snd R (C 0) (Fin m₀ → R) ∘ₗ P.subtype)).subtype.baseChange
              A) →
          Function.Injective ((LinearMap.ker (d 0)).subtype.baseChange A))

Module documentation

Module exists mumford Truncation of flat complex

Declarations