ModuleTwoChartCech_Mumford_finite_K0.lean
Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Mumford_finite_K0
3 declarations indexed from sourceView source ↗ Module documentation
Finiteness of the enlarged kernel used in the finite-presentation construction.
Declarations
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_finite_K0.TwoChartCech.Mumford.kerToK0
DocumentationEmbed the original kernel into the enlarged kernel with zero presentation coordinate.
Source context 14 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_finite_K0
noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
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)]
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_finite_K0.TwoChartCech.Mumford.kerEquiv
DocumentationIdentify the kernel of the presentation projection with the original kernel.
Source context 14 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_finite_K0
noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
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)]
TwoChartCech.Mumford.finite_K0
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_finite_K0
noncomputable section
open scoped TensorProduct
universe u v w
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs in
open _root_.TwoChartCech.Mumford TwoChartCech_Mumford_finite_K0.TwoChartCech.Mumford in