NYLL
Module

TwoChartCech_Mumford_flat_K0.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Mumford_flat_K0
3 declarations indexed from sourceView source ↗

Module documentation

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

Imports4
Imported by4

Declarations

theorem

flat_prod'

L41 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_flat_K0.TwoChartCech.Mumford.flat_prod'
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_flat_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]
Lean source · statement
theorem flat_prod' {M : Type v} {N : Type w} [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_of_surjective'

L64 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_flat_K0.TwoChartCech.Mumford.flat_ker_of_surjective'
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_flat_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]
Lean source · statement
theorem flat_ker_of_surjective' {M : Type v} {N : Type w} [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N] [Module.Flat R M] [Module.Flat R N]
    (f : M →ₗ[R] N) (hf : Function.Surjective f) :
    Module.Flat R (LinearMap.ker f)
theorem

flat_K0

L91 ↗
TwoChartCech.Mumford.flat_K0
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_flat_K0
noncomputable section
open scoped TensorProduct
universe u v w
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs in
open _root_.TwoChartCech.Mumford TwoChartCech_Mumford_flat_K0.TwoChartCech.Mumford in
Lean source · statement
theorem _root_.TwoChartCech.Mumford.flat_K0
    {R : Type u} [CommRing 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 (C1 ⧸ LinearMap.range d)] :
    Module.Flat 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.