NYLL
Module

TwoChartCech_Mumford_projective_ker_of_fibre_surjective.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Mumford_projective_ker_of_fibre_surjective
6 declarations indexed from sourceView source ↗

Module documentation

Projectivity and base change of a Cech kernel from surjectivity of the fibre kernel comparisons.

Imports10
Imported by5

Declarations

theorem

subsingleton_of_forall_maximal_smul_top

L53 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_projective_ker_of_fibre_surjective.TwoChartCech.Mumford.FibreSurj.subsingleton_of_forall_maximal_smul_top
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_Mumford_projective_ker_of_fibre_surjective
universe u v
open scoped TensorProduct
noncomputable section
section
open scoped TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace FibreSurj
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
variable {A : Type u} [CommRing A]
Lean source · statement
theorem subsingleton_of_forall_maximal_smul_top {M : Type v} [AddCommGroup M] [Module A M]
    [Module.Finite A M]
    (h : ∀ 𝔪 : Ideal A, 𝔪.IsMaximal → 𝔪 • (⊤ : Submodule A M) = ⊤) : Subsingleton M
theorem

dK_surjective

L76 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_projective_ker_of_fibre_surjective.TwoChartCech.Mumford.FibreSurj.dK_surjective
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_Mumford_projective_ker_of_fibre_surjective
universe u v
open scoped TensorProduct
noncomputable section
section
open scoped TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace FibreSurj
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
variable {A : Type u} [CommRing A]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module A C0] [AddCommGroup C1] [Module A C1]
variable (d : C0 →ₗ[A] C1) [Module.Finite A (C1 ⧸ LinearMap.range d)]
Lean source · statement
theorem dK_surjective
    (hH1 : ∀ (K : Type u) [Field K] [Algebra A K], Function.Surjective (d.baseChange K)) :
    Function.Surjective (Mumford.dK d)
theorem

kerMap_bijective

L108 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_projective_ker_of_fibre_surjective.TwoChartCech.Mumford.FibreSurj.kerMap_bijective
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_Mumford_projective_ker_of_fibre_surjective
universe u v
open scoped TensorProduct
noncomputable section
section
open scoped TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace FibreSurj
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
variable {A : Type u} [CommRing A]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module A C0] [AddCommGroup C1] [Module A C1]
variable (d : C0 →ₗ[A] C1) [Module.Finite A (C1 ⧸ LinearMap.range d)]
Lean source · statement
theorem kerMap_bijective :
    Function.Bijective (kerMap (dK d) d (ι0 d) (ι1 d) (comm d))
def

kerMapEquiv

L122 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_projective_ker_of_fibre_surjective.TwoChartCech.Mumford.FibreSurj.kerMapEquiv
Documentation

The kernel equivalence induced by projecting the enlarged source onto the original source.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_Mumford_projective_ker_of_fibre_surjective
universe u v
open scoped TensorProduct
noncomputable section
section
open scoped TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace FibreSurj
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
variable {A : Type u} [CommRing A]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module A C0] [AddCommGroup C1] [Module A C1]
variable (d : C0 →ₗ[A] C1) [Module.Finite A (C1 ⧸ LinearMap.range d)]
Lean source · statement
def kerMapEquiv : LinearMap.ker (dK d) ≃ₗ[A] LinearMap.ker d
theorem

subtype_comp_kerMap

L125 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_projective_ker_of_fibre_surjective.TwoChartCech.Mumford.FibreSurj.subtype_comp_kerMap
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_Mumford_projective_ker_of_fibre_surjective
universe u v
open scoped TensorProduct
noncomputable section
section
open scoped TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
namespace FibreSurj
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
variable {A : Type u} [CommRing A]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module A C0] [AddCommGroup C1] [Module A C1]
variable (d : C0 →ₗ[A] C1) [Module.Finite A (C1 ⧸ LinearMap.range d)]
Lean source · statement
theorem subtype_comp_kerMap :
    (LinearMap.ker d).subtype ∘ₗ kerMap (dK d) d (ι0 d) (ι1 d) (comm d)
      = ι0 d ∘ₗ (LinearMap.ker (dK d)).subtype
theorem

projective_ker_of_fibre_surjective

L140 ↗
TwoChartCech.Mumford.projective_ker_of_fibre_surjective
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_Mumford_projective_ker_of_fibre_surjective
universe u v
open scoped TensorProduct
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs in
open _root_.TwoChartCech TwoChartCech_Mumford_projective_ker_of_fibre_surjective.TwoChartCech
  _root_.TwoChartCech.Mumford
  TwoChartCech_Mumford_projective_ker_of_fibre_surjective.TwoChartCech.Mumford in
Lean source · statement
theorem _root_.TwoChartCech.Mumford.projective_ker_of_fibre_surjective
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    {C0 C1 : Type u} [AddCommGroup C0] [Module A C0] [AddCommGroup C1] [Module A C1]
    [Module.Flat A C0] [Module.Flat A C1] (d : C0 →ₗ[A] C1)
    [Module.Finite A (LinearMap.ker d)] [Module.Finite A (C1 ⧸ LinearMap.range d)]
    (hH1 : ∀ (K : Type u) [Field K] [Algebra A K], Function.Surjective (d.baseChange K)) :
    Module.Projective A (LinearMap.ker d) ∧
      (∀ (A' : Type u) [CommRing A'] [Algebra A A'], Function.Bijective
        (TwoChartCech.kerBaseChangeHom d A')) ∧
      ∀ (K : Type u) [Field K] [Algebra A K],
        Module.finrank K (K ⊗[A] LinearMap.ker d) = Module.finrank K (LinearMap.ker (d.baseChange
          K))

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