NYLL
Module

MumfordTruncation.lean

Nyll.AlgebraicCurves.Geometry.Schemes.MumfordTruncation
29 declarations indexed from sourceView source ↗

Module documentation

Kernel-coproduct truncations of two-term complexes

The kernel of a coproduct map gives a two-term truncation. When its cokernel is finite, a chosen free presentation and projective lift produce the Mumford truncation maps.

Imports4
  • Mathlib.LinearAlgebra.Prod
  • Mathlib.LinearAlgebra.Quotient.Basic
  • Mathlib.RingTheory.Finiteness.Cardinality
  • Mathlib.Algebra.Module.Projective
Imported by10

Declarations

abbrev

K0

L39 ↗
TwoChartCech.KerCoprod.K0
Documentation

The pairs whose images under the coproduct of the two maps add to zero.

Source context 8 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace KerCoprod
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable {P : Type w'} [AddCommGroup P] [Module R P]
variable (d : C0 →ₗ[R] C1) (g : P →ₗ[R] C1)
Lean source · statement
abbrev K0 : Submodule R (C0 × P)
theorem

mem_K0_iff

L41 ↗
TwoChartCech.KerCoprod.mem_K0_iff
Source context 8 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace KerCoprod
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable {P : Type w'} [AddCommGroup P] [Module R P]
variable (d : C0 →ₗ[R] C1) (g : P →ₗ[R] C1)
Lean source · statement
theorem mem_K0_iff (z : C0 × P) : z ∈ K0 d g ↔ d z.1 + g z.2 = 0
def

dK

L45 ↗
TwoChartCech.KerCoprod.dK
Documentation

The projection of the coproduct kernel to the auxiliary module.

Source context 8 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace KerCoprod
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable {P : Type w'} [AddCommGroup P] [Module R P]
variable (d : C0 →ₗ[R] C1) (g : P →ₗ[R] C1)
Lean source · statement
def dK : K0 d g →ₗ[R] P
def

ι0

L48 ↗
TwoChartCech.KerCoprod.ι0
Documentation

The projection of the coproduct kernel to the original degree-zero module.

Source context 8 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace KerCoprod
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable {P : Type w'} [AddCommGroup P] [Module R P]
variable (d : C0 →ₗ[R] C1) (g : P →ₗ[R] C1)
Lean source · statement
def ι0 : K0 d g →ₗ[R] C0
def

ι1

L51 ↗
TwoChartCech.KerCoprod.ι1
Documentation

The negative of the auxiliary map to the degree-one module.

Source context 8 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace KerCoprod
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable {P : Type w'} [AddCommGroup P] [Module R P]
variable (d : C0 →ₗ[R] C1) (g : P →ₗ[R] C1)
Lean source · statement
def ι1 : P →ₗ[R] C1
theorem

dK_apply

L53 ↗
TwoChartCech.KerCoprod.dK_apply
Source context 8 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace KerCoprod
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable {P : Type w'} [AddCommGroup P] [Module R P]
variable (d : C0 →ₗ[R] C1) (g : P →ₗ[R] C1)
Lean source · statement
theorem dK_apply (z : K0 d g) : dK d g z = (z : C0 × P).2
theorem

ι0_apply

L54 ↗
TwoChartCech.KerCoprod.ι0_apply
Source context 8 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace KerCoprod
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable {P : Type w'} [AddCommGroup P] [Module R P]
variable (d : C0 →ₗ[R] C1) (g : P →ₗ[R] C1)
Lean source · statement
theorem ι0_apply (z : K0 d g) : ι0 d g z = (z : C0 × P).1
theorem

ι1_apply

L55 ↗
TwoChartCech.KerCoprod.ι1_apply
Source context 8 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace KerCoprod
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable {P : Type w'} [AddCommGroup P] [Module R P]
variable (d : C0 →ₗ[R] C1) (g : P →ₗ[R] C1)
Lean source · statement
theorem ι1_apply (p : P) : ι1 g p = -g p
theorem

ι1_eq

L56 ↗
TwoChartCech.KerCoprod.ι1_eq
Source context 8 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace KerCoprod
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable {P : Type w'} [AddCommGroup P] [Module R P]
variable (d : C0 →ₗ[R] C1) (g : P →ₗ[R] C1)
Lean source · statement
theorem ι1_eq : ι1 g = -g
theorem

comm

L58 ↗
TwoChartCech.KerCoprod.comm
Source context 8 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace KerCoprod
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable {P : Type w'} [AddCommGroup P] [Module R P]
variable (d : C0 →ₗ[R] C1) (g : P →ₗ[R] C1)
Lean source · statement
theorem comm : d ∘ₗ ι0 d g = ι1 g ∘ₗ dK d g
theorem

ι0_prod_dK

L64 ↗
TwoChartCech.KerCoprod.ι0_prod_dK
Source context 8 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace KerCoprod
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable {P : Type w'} [AddCommGroup P] [Module R P]
variable (d : C0 →ₗ[R] C1) (g : P →ₗ[R] C1)
Lean source · statement
theorem ι0_prod_dK : (ι0 d g).prod (dK d g) = (K0 d g).subtype
def

rank

L76 ↗
TwoChartCech.Mumford.rank
Documentation

The size of the chosen finite free presentation of the cokernel.

Source context 7 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace Mumford
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
Lean source · statement
def rank : ℕ
def

quot

L79 ↗
TwoChartCech.Mumford.quot
Documentation

The chosen surjection from a finite free module to the cokernel.

Source context 7 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace Mumford
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
Lean source · statement
def quot : (Fin (rank d) → R) →ₗ[R] (C1 ⧸ LinearMap.range d)
theorem

quot_surjective

L82 ↗
TwoChartCech.Mumford.quot_surjective
Source context 7 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace Mumford
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
Lean source · statement
theorem quot_surjective : Function.Surjective (quot d)
def

lift

L86 ↗
TwoChartCech.Mumford.lift
Documentation

The projective lift of the chosen cokernel presentation to the degree-one module.

Source context 7 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace Mumford
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
Lean source · statement
def lift : (Fin (rank d) → R) →ₗ[R] C1
theorem

mkQ_comp_lift

L90 ↗
TwoChartCech.Mumford.mkQ_comp_lift
Source context 7 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace Mumford
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
Lean source · statement
theorem mkQ_comp_lift : (LinearMap.range d).mkQ ∘ₗ lift d = quot d
theorem

mkQ_lift_apply

L94 ↗
TwoChartCech.Mumford.mkQ_lift_apply
Source context 7 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace Mumford
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
Lean source · statement
theorem mkQ_lift_apply (v : Fin (rank d) → R) : (LinearMap.range d).mkQ (lift d v) = quot d v
theorem

surjective_coprod

L97 ↗
TwoChartCech.Mumford.surjective_coprod
Source context 7 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace Mumford
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
Lean source · statement
theorem surjective_coprod : Function.Surjective (d.coprod (lift d))
abbrev

K0

L107 ↗
TwoChartCech.Mumford.K0
Documentation

The kernel of the original map coproduct with the chosen presentation lift.

Source context 7 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace Mumford
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
Lean source · statement
abbrev K0 : Submodule R (C0 × (Fin (rank d) → R))
theorem

mem_K0_iff

L109 ↗
TwoChartCech.Mumford.mem_K0_iff
Source context 7 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace Mumford
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
Lean source · statement
theorem mem_K0_iff (z : C0 × (Fin (rank d) → R)) : z ∈ K0 d ↔ d z.1 + lift d z.2 = 0
abbrev

dK

L113 ↗
TwoChartCech.Mumford.dK
Documentation

The projection from the Mumford kernel to the chosen finite free module.

Source context 7 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace Mumford
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
Lean source · statement
abbrev dK : K0 d →ₗ[R] (Fin (rank d) → R)
abbrev

ι0

L116 ↗
TwoChartCech.Mumford.ι0
Documentation

The projection from the Mumford kernel to the original degree-zero module.

Source context 7 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace Mumford
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
Lean source · statement
abbrev ι0 : K0 d →ₗ[R] C0
abbrev

ι1

L119 ↗
TwoChartCech.Mumford.ι1
Documentation

The negative of the chosen presentation lift.

Source context 7 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace Mumford
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
Lean source · statement
abbrev ι1 : (Fin (rank d) → R) →ₗ[R] C1
theorem

dK_apply

L121 ↗
TwoChartCech.Mumford.dK_apply
Source context 7 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace Mumford
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
Lean source · statement
theorem dK_apply (z : K0 d) : dK d z = (z : C0 × (Fin (rank d) → R)).2
theorem

ι0_apply

L122 ↗
TwoChartCech.Mumford.ι0_apply
Source context 7 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace Mumford
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
Lean source · statement
theorem ι0_apply (z : K0 d) : ι0 d z = (z : C0 × (Fin (rank d) → R)).1
theorem

ι1_apply

L123 ↗
TwoChartCech.Mumford.ι1_apply
Source context 7 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace Mumford
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
Lean source · statement
theorem ι1_apply (v : Fin (rank d) → R) : ι1 d v = -lift d v
theorem

ι1_eq

L124 ↗
TwoChartCech.Mumford.ι1_eq
Source context 7 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace Mumford
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
Lean source · statement
theorem ι1_eq : ι1 d = -lift d
theorem

comm

L126 ↗
TwoChartCech.Mumford.comm
Source context 7 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace Mumford
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
Lean source · statement
theorem comm : d ∘ₗ ι0 d = ι1 d ∘ₗ dK d
theorem

ι0_prod_dK

L128 ↗
TwoChartCech.Mumford.ι0_prod_dK
Source context 7 commands

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

noncomputable section
universe u v w w'
namespace TwoChartCech
namespace Mumford
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
Lean source · statement
theorem ι0_prod_dK : (ι0 d).prod (dK d) = (K0 d).subtype

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.