Module

TwoChartCechCupProduct.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCechCupProduct

10 declarations indexed from sourceView source ↗

Module documentation

Two Chart Cech Cup Product

Imports3

Mathlib.LinearAlgebra.BilinearMap
Mathlib.LinearAlgebra.Quotient.Basic
Nyll.SchemeTheory.Cohomology.Cech.TwoChartCech

Imported by2

theorem

smul_r0_mem_range_cechDiff

L31 ↗

TwoChartCech.Sections.smul_r0_mem_range_cechDiff

Source context 5 commands

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

noncomputable section
universe u v w
namespace TwoChartCech
namespace Sections
variable {R : Type u} [CommRing R] {𝒰 : Cover.{u, v} R} (S : Sections.{u, v, w} 𝒰)

Lean source · statement

theorem smul_r0_mem_range_cechDiff (x : S.H0) {f : 𝒰.A01}
    (hf : f ∈ LinearMap.range 𝒰.structureSheaf.cechDiff) :
    f • S.r0 x.val.1 ∈ LinearMap.range S.cechDiff

def

cupProductFun

L41 ↗

TwoChartCech.Sections.cupProductFun

Documentation

Cup product with a fixed global section, descended to first cohomology.

Source context 5 commands

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

noncomputable section
universe u v w
namespace TwoChartCech
namespace Sections
variable {R : Type u} [CommRing R] {𝒰 : Cover.{u, v} R} (S : Sections.{u, v, w} 𝒰)

Lean source · statement

def cupProductFun (x : S.H0) : 𝒰.structureSheaf.H1 →ₗ[R] S.H1

theorem

cupProductFun_mk

L50 ↗

TwoChartCech.Sections.cupProductFun_mk

Source context 5 commands

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

noncomputable section
universe u v w
namespace TwoChartCech
namespace Sections
variable {R : Type u} [CommRing R] {𝒰 : Cover.{u, v} R} (S : Sections.{u, v, w} 𝒰)

Lean source · statement

theorem cupProductFun_mk (x : S.H0) (f : 𝒰.A01) :
    S.cupProductFun x (Submodule.Quotient.mk f) = Submodule.Quotient.mk (f • S.r0 x.val.1)

def

cupProduct

L54 ↗

TwoChartCech.Sections.cupProduct

Documentation

The bilinear cup product of global sections and structure-sheaf cohomology.

Source context 5 commands

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

noncomputable section
universe u v w
namespace TwoChartCech
namespace Sections
variable {R : Type u} [CommRing R] {𝒰 : Cover.{u, v} R} (S : Sections.{u, v, w} 𝒰)

Lean source · full declaration

def cupProduct : S.H0 →ₗ[R] 𝒰.structureSheaf.H1 →ₗ[R] S.H1 where
  toFun := S.cupProductFun
  map_add' x y := by
    refine LinearMap.ext fun q => ?_
    induction q using Submodule.Quotient.induction_on with
    | H f =>
      rw [LinearMap.add_apply, cupProductFun_mk, cupProductFun_mk, cupProductFun_mk,
        Submodule.coe_add,
        Prod.fst_add, map_add, smul_add, Submodule.Quotient.mk_add]
  map_smul' r x := by
    refine LinearMap.ext fun q => ?_
    induction q using Submodule.Quotient.induction_on with
    | H f =>
      rw [LinearMap.smul_apply, RingHom.id_apply, cupProductFun_mk, cupProductFun_mk,
        Submodule.coe_smul,
        Prod.smul_fst, LinearMap.map_smul, smul_comm (f : 𝒰.A01) r, Submodule.Quotient.mk_smul]

theorem

cupProduct_apply_mk

L71 ↗

TwoChartCech.Sections.cupProduct_apply_mk

Source context 5 commands

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

noncomputable section
universe u v w
namespace TwoChartCech
namespace Sections
variable {R : Type u} [CommRing R] {𝒰 : Cover.{u, v} R} (S : Sections.{u, v, w} 𝒰)

Lean source · statement

theorem cupProduct_apply_mk (x : S.H0) (f : 𝒰.A01) :
    S.cupProduct x (Submodule.Quotient.mk f) = Submodule.Quotient.mk (f • S.r0 x.val.1)

theorem

cupProduct_apply_mk'

L74 ↗

TwoChartCech.Sections.cupProduct_apply_mk'

Source context 5 commands

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

noncomputable section
universe u v w
namespace TwoChartCech
namespace Sections
variable {R : Type u} [CommRing R] {𝒰 : Cover.{u, v} R} (S : Sections.{u, v, w} 𝒰)

Lean source · statement

theorem cupProduct_apply_mk' (x : S.H0) (f : 𝒰.A01) :
    S.cupProduct x (Submodule.Quotient.mk f) = Submodule.Quotient.mk (f • S.r1 x.val.2)

def

traceForm

L79 ↗

TwoChartCech.Sections.traceForm

Documentation

The functional on first cohomology induced by a functional vanishing on coboundaries.

Source context 5 commands

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

noncomputable section
universe u v w
namespace TwoChartCech
namespace Sections
variable {R : Type u} [CommRing R] {𝒰 : Cover.{u, v} R} (S : Sections.{u, v, w} 𝒰)

Lean source · statement

def traceForm (t : S.M01 →ₗ[R] R) (ht : LinearMap.range S.cechDiff ≤ LinearMap.ker t) : S.H1
  →ₗ[R] R

theorem

traceForm_mk

L83 ↗

TwoChartCech.Sections.traceForm_mk

Source context 5 commands

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

noncomputable section
universe u v w
namespace TwoChartCech
namespace Sections
variable {R : Type u} [CommRing R] {𝒰 : Cover.{u, v} R} (S : Sections.{u, v, w} 𝒰)

Lean source · statement

theorem traceForm_mk (t : S.M01 →ₗ[R] R) (ht : LinearMap.range S.cechDiff ≤ LinearMap.ker t)
    (m : S.M01) : S.traceForm t ht (Submodule.Quotient.mk m) = t m

def

tracePairing

L87 ↗

TwoChartCech.Sections.tracePairing

Documentation

Compose cup product with the induced trace functional.

Source context 5 commands

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

noncomputable section
universe u v w
namespace TwoChartCech
namespace Sections
variable {R : Type u} [CommRing R] {𝒰 : Cover.{u, v} R} (S : Sections.{u, v, w} 𝒰)

Lean source · statement

def tracePairing (t : S.M01 →ₗ[R] R) (ht : LinearMap.range S.cechDiff ≤ LinearMap.ker t) :
    S.H0 →ₗ[R] 𝒰.structureSheaf.H1 →ₗ[R] R

theorem

tracePairing_apply_mk

L91 ↗

TwoChartCech.Sections.tracePairing_apply_mk

Source context 5 commands

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

noncomputable section
universe u v w
namespace TwoChartCech
namespace Sections
variable {R : Type u} [CommRing R] {𝒰 : Cover.{u, v} R} (S : Sections.{u, v, w} 𝒰)

Lean source · statement

theorem tracePairing_apply_mk (t : S.M01 →ₗ[R] R) (ht : LinearMap.range S.cechDiff ≤
  LinearMap.ker t)
    (x : S.H0) (f : 𝒰.A01) :
    S.tracePairing t ht x (Submodule.Quotient.mk f) = t (f • S.r0 x.val.1)

Module documentation

Two Chart Cech Cup Product

Declarations