NYLL
Module

TwoChartCech_Mumford_projective_K0.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Mumford_projective_K0
1 declaration indexed from sourceView source ↗

Module documentation

Projectivity of the enlarged kernel in the finite-presentation construction.

Imports8
Imported by2

Declarations

theorem

projective_K0

L38 ↗
TwoChartCech.Mumford.projective_K0
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_projective_K0
noncomputable section
open scoped TensorProduct
universe u v w
open TwoChartCech.Mumford in
Lean source · statement
theorem _root_.TwoChartCech.Mumford.projective_K0
    {R : Type u} [CommRing R] [IsNoetherianRing R]
    {C0 : Type v} {C1 : Type w} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
    [Module.Flat R C0] [Module.Flat R C1]
    (d : C0 →ₗ[R] C1) [Module.Finite R (LinearMap.ker d)] [Module.Finite R (C1 ⧸ LinearMap.range
      d)] :
    Module.Projective R (TwoChartCech.Mumford.K0 d)

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