NYLL
Module

TwoChartCech.lean

Nyll.SchemeTheory.Cohomology.Cech.TwoChartCech
23 declarations indexed from sourceView source ↗

Module documentation

Cech data on two charts

This file defines algebraic chart covers and their section modules, the Cech difference, its kernel and cokernel, and their comparison maps under scalar extension. It also defines two-term models whose kernel and cokernel comparisons remain bijective after base change.

Imports5
Imported by70

Declarations

structure

Cover

L36 ↗
TwoChartCech.Cover
Documentation

R-algebra data for two charts and their overlap.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
Lean source · full declaration
structure Cover (R : Type u) [CommRing R] where
  /-- The ring assigned to the first chart. -/
  A0 : Type v
  /-- The ring assigned to the second chart. -/
  A1 : Type v
  /-- The ring assigned to the overlap of the two charts. -/
  A01 : Type v
  /-- The commutative ring structure on the first chart ring. -/
  [A0_commRing : CommRing A0]
  /-- The base ring algebra structure on the first chart ring. -/
  [A0_algebra : Algebra R A0]
  /-- The commutative ring structure on the second chart ring. -/
  [A1_commRing : CommRing A1]
  /-- The base ring algebra structure on the second chart ring. -/
  [A1_algebra : Algebra R A1]
  /-- The commutative ring structure on the overlap ring. -/
  [A01_commRing : CommRing A01]
  /-- The base ring algebra structure on the overlap ring. -/
  [A01_algebra : Algebra R A01]
  /-- Restriction from the first chart ring to the overlap ring. -/
  ρ0 : A0 →ₐ[R] A01
  /-- Restriction from the second chart ring to the overlap ring. -/
  ρ1 : A1 →ₐ[R] A01
structure

Sections

L64 ↗
TwoChartCech.Sections
Documentation

Modules on two charts and their overlap, with scalar compatible restriction maps.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
Lean source · full declaration
structure Sections {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R) where
  /-- The module of sections on the first chart. -/
  M0 : Type w
  /-- The module of sections on the second chart. -/
  M1 : Type w
  /-- The module of sections on the overlap. -/
  M01 : Type w
  /-- The additive commutative group structure on the first chart sections. -/
  [M0_addCommGroup : AddCommGroup M0]
  /-- The action of the first chart ring on its section module. -/
  [M0_moduleA : Module 𝒰.A0 M0]
  /-- The base ring module structure on the first chart sections. -/
  [M0_module : Module R M0]
  /-- Compatibility of the base ring and first chart scalar actions. -/
  [M0_tower : IsScalarTower R 𝒰.A0 M0]
  /-- The additive commutative group structure on the second chart sections. -/
  [M1_addCommGroup : AddCommGroup M1]
  /-- The action of the second chart ring on its section module. -/
  [M1_moduleA : Module 𝒰.A1 M1]
  /-- The base ring module structure on the second chart sections. -/
  [M1_module : Module R M1]
  /-- Compatibility of the base ring and second chart scalar actions. -/
  [M1_tower : IsScalarTower R 𝒰.A1 M1]
  /-- The additive commutative group structure on the overlap sections. -/
  [M01_addCommGroup : AddCommGroup M01]
  /-- The action of the overlap ring on its section module. -/
  [M01_moduleA : Module 𝒰.A01 M01]
  /-- The base ring module structure on the overlap sections. -/
  [M01_module : Module R M01]
  /-- Compatibility of the base ring and overlap scalar actions. -/
  [M01_tower : IsScalarTower R 𝒰.A01 M01]
  /-- The base ring linear restriction from the first chart to the overlap. -/
  r0 : M0 →ₗ[R] M01
  /-- The base ring linear restriction from the second chart to the overlap. -/
  r1 : M1 →ₗ[R] M01
  /-- The first restriction transports chart scalars through `ρ0`. -/
  r0_smul : ∀ (a : 𝒰.A0) (m : M0), r0 (a • m) = 𝒰.ρ0 a • r0 m
  /-- The second restriction transports chart scalars through `ρ1`. -/
  r1_smul : ∀ (a : 𝒰.A1) (m : M1), r1 (a • m) = 𝒰.ρ1 a • r1 m
def

cechDiff

L114 ↗
TwoChartCech.Sections.cechDiff
Documentation

The Cech difference sending a pair of sections to r1 s.2 - r0 s.1.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
namespace Sections
variable {R : Type u} [CommRing R] {𝒰 : Cover.{u, v} R} (S : Sections.{u, v, w} 𝒰)
Lean source · statement
def cechDiff : S.M0 × S.M1 →ₗ[R] S.M01
theorem

cechDiff_apply

L116 ↗
TwoChartCech.Sections.cechDiff_apply
Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
namespace Sections
variable {R : Type u} [CommRing R] {𝒰 : Cover.{u, v} R} (S : Sections.{u, v, w} 𝒰)
Lean source · statement
theorem cechDiff_apply (s : S.M0 × S.M1) : S.cechDiff s = S.r1 s.2 - S.r0 s.1
abbrev

H0

L120 ↗
TwoChartCech.Sections.H0
Documentation

Compatible pairs of chart sections, forming the kernel of the Cech difference.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
namespace Sections
variable {R : Type u} [CommRing R] {𝒰 : Cover.{u, v} R} (S : Sections.{u, v, w} 𝒰)
Lean source · statement
abbrev H0 : Submodule R (S.M0 × S.M1)
theorem

mem_H0_iff

L122 ↗
TwoChartCech.Sections.mem_H0_iff
Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
namespace Sections
variable {R : Type u} [CommRing R] {𝒰 : Cover.{u, v} R} (S : Sections.{u, v, w} 𝒰)
Lean source · statement
theorem mem_H0_iff (s : S.M0 × S.M1) : s ∈ S.H0 ↔ S.r0 s.1 = S.r1 s.2
abbrev

H1

L126 ↗
TwoChartCech.Sections.H1
Documentation

Overlap sections modulo the image of the Cech difference.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
namespace Sections
variable {R : Type u} [CommRing R] {𝒰 : Cover.{u, v} R} (S : Sections.{u, v, w} 𝒰)
Lean source · statement
abbrev H1 : Type w
def

lineBundle

L135 ↗
TwoChartCech.Cover.lineBundle
Documentation

Two chart section data with transition unit t, multiplying the second restriction by t.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
namespace Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R)
Lean source · full declaration
def lineBundle (t : 𝒰.A01ˣ) : Sections.{u, v, v} 𝒰 where
  M0 := 𝒰.A0
  M1 := 𝒰.A1
  M01 := 𝒰.A01
  r0 := 𝒰.ρ0.toLinearMap
  r1 := (t : 𝒰.A01) • 𝒰.ρ1.toLinearMap
  r0_smul a m := by simp
  r1_smul a m := by simp [mul_left_comm]
theorem

lineBundle_r0_apply

L144 ↗
TwoChartCech.Cover.lineBundle_r0_apply
Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
namespace Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R)
Lean source · statement
theorem lineBundle_r0_apply (t : 𝒰.A01ˣ) (p : 𝒰.A0) : (𝒰.lineBundle t).r0 p = 𝒰.ρ0 p
theorem

lineBundle_r1_apply

L145 ↗
TwoChartCech.Cover.lineBundle_r1_apply
Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
namespace Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R)
Lean source · statement
theorem lineBundle_r1_apply (t : 𝒰.A01ˣ) (p : 𝒰.A1) :
    (𝒰.lineBundle t).r1 p = (t : 𝒰.A01) * 𝒰.ρ1 p
theorem

mem_H0_lineBundle_iff

L148 ↗
TwoChartCech.Cover.mem_H0_lineBundle_iff
Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
namespace Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R)
Lean source · statement
theorem mem_H0_lineBundle_iff (t : 𝒰.A01ˣ) (p : 𝒰.A0 × 𝒰.A1) :
    p ∈ (𝒰.lineBundle t).H0 ↔ 𝒰.ρ0 p.1 = (t : 𝒰.A01) * 𝒰.ρ1 p.2
abbrev

structureSheaf

L153 ↗
TwoChartCech.Cover.structureSheaf
Documentation

The two chart section datum with transition unit equal to one.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
namespace Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R)
Lean source · statement
abbrev structureSheaf : Sections.{u, v, v} 𝒰
theorem

mem_H0_structureSheaf_iff

L155 ↗
TwoChartCech.Cover.mem_H0_structureSheaf_iff
Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
namespace Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R)
Lean source · statement
theorem mem_H0_structureSheaf_iff (p : 𝒰.A0 × 𝒰.A1) :
    p ∈ 𝒰.structureSheaf.H0 ↔ 𝒰.ρ0 p.1 = 𝒰.ρ1 p.2
def

kerBaseChangeHom

L168 ↗
TwoChartCech.kerBaseChangeHom
Documentation

The natural map from the tensor product of a kernel to the kernel of the map after extending scalars.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
section Dock
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type v} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
Lean source · statement
def kerBaseChangeHom (d : C0 →ₗ[R] C1) (A : Type w) [CommRing A] [Algebra R A] :
    A ⊗[R] (LinearMap.ker d) →ₗ[A] LinearMap.ker (d.baseChange A)
theorem

kerBaseChangeHom_apply_coe

L178 ↗
TwoChartCech.kerBaseChangeHom_apply_coe
Source context 9 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
section Dock
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type v} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
Lean source · statement
theorem kerBaseChangeHom_apply_coe (d : C0 →ₗ[R] C1) (A : Type w) [CommRing A] [Algebra R A]
    (x : A ⊗[R] (LinearMap.ker d)) :
    (kerBaseChangeHom d A x : A ⊗[R] C0) = (LinearMap.ker d).subtype.baseChange A x
def

kerMap

L184 ↗
TwoChartCech.kerMap
Documentation

The map on kernels induced by a commuting square of linear maps.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
section Dock
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type v} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
Lean source · statement
def kerMap {K0 : Type v} {K1 : Type v} [AddCommGroup K0] [Module R K0] [AddCommGroup K1]
    [Module R K1] (dK : K0 →ₗ[R] K1) (d : C0 →ₗ[R] C1) (ι0 : K0 →ₗ[R] C0) (ι1 : K1 →ₗ[R] C1)
    (comm : d ∘ₗ ι0 = ι1 ∘ₗ dK) : LinearMap.ker dK →ₗ[R] LinearMap.ker d
def

cokerMap

L192 ↗
TwoChartCech.cokerMap
Documentation

The map on cokernels induced by a commuting square of linear maps.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
section Dock
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type v} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
Lean source · statement
def cokerMap {K0 : Type v} {K1 : Type v} [AddCommGroup K0] [Module R K0] [AddCommGroup K1]
    [Module R K1] (dK : K0 →ₗ[R] K1) (d : C0 →ₗ[R] C1) (ι0 : K0 →ₗ[R] C0) (ι1 : K1 →ₗ[R] C1)
    (comm : d ∘ₗ ι0 = ι1 ∘ₗ dK) : (K1 ⧸ LinearMap.range dK) →ₗ[R] (C1 ⧸ LinearMap.range d)
def

kerMapBaseChange

L201 ↗
TwoChartCech.kerMapBaseChange
Documentation

The induced map on kernels after extending scalars to A.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
section Dock
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type v} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
Lean source · statement
def kerMapBaseChange {K0 : Type v} {K1 : Type v} [AddCommGroup K0] [Module R K0] [AddCommGroup K1]
    [Module R K1] (dK : K0 →ₗ[R] K1) (d : C0 →ₗ[R] C1) (ι0 : K0 →ₗ[R] C0) (ι1 : K1 →ₗ[R] C1)
    (comm : d ∘ₗ ι0 = ι1 ∘ₗ dK) (A : Type w) [CommRing A] [Algebra R A] :
    LinearMap.ker (dK.baseChange A) →ₗ[A] LinearMap.ker (d.baseChange A)
def

cokerMapBaseChange

L211 ↗
TwoChartCech.cokerMapBaseChange
Documentation

The induced map on cokernels after extending scalars to A.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
section Dock
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type v} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
Lean source · statement
def cokerMapBaseChange {K0 : Type v} {K1 : Type v} [AddCommGroup K0] [Module R K0] [AddCommGroup K1]
    [Module R K1] (dK : K0 →ₗ[R] K1) (d : C0 →ₗ[R] C1) (ι0 : K0 →ₗ[R] C0) (ι1 : K1 →ₗ[R] C1)
    (comm : d ∘ₗ ι0 = ι1 ∘ₗ dK) (A : Type w) [CommRing A] [Algebra R A] :
    ((A ⊗[R] K1) ⧸ LinearMap.range (dK.baseChange A)) →ₗ[A]
      ((A ⊗[R] C1) ⧸ LinearMap.range (d.baseChange A))
structure

GrothendieckComplex

L224 ↗
TwoChartCech.GrothendieckComplex
Documentation

A model with two terms whose comparison with d is bijective on kernels and cokernels after every base change.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
section Dock
variable {R : Type u} [CommRing R]
variable {C0 : Type v} {C1 : Type v} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
Lean source · full declaration
structure GrothendieckComplex (d : C0 →ₗ[R] C1) where
  /-- The model two-term complex. -/
  G : CoherentBaseChange.TwoTermComplex.{u, v} R
  /-- The degree zero comparison from the model complex to `C0`. -/
  ι0 : G.C0 →ₗ[R] C0
  /-- The degree one comparison from the model complex to `C1`. -/
  ι1 : G.C1 →ₗ[R] C1
  /-- The comparison maps commute with the two differentials. -/
  comm : d ∘ₗ ι0 = ι1 ∘ₗ G.d
  /-- The kernel comparison is bijective after every base change. -/
  bijective_kerMap : ∀ (A : Type u) [CommRing A] [Algebra R A],
    Function.Bijective (kerMapBaseChange G.d d ι0 ι1 comm A)
  /-- The cokernel comparison is bijective after every base change. -/
  bijective_cokerMap : ∀ (A : Type u) [CommRing A] [Algebra R A],
    Function.Bijective (cokerMapBaseChange G.d d ι0 ι1 comm A)
def

trivial

L244 ↗
TwoChartCech.Cover.trivial
Documentation

The two chart cover with every ring equal to R and both restriction maps equal to the identity.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
Lean source · full declaration
def Cover.trivial (R : Type u) [CommRing R] : Cover.{u, u} R where
  A0 := R
  A1 := R
  A01 := R
  ρ0 := AlgHom.id R R
  ρ1 := AlgHom.id R R
def

ofSubmodules

L252 ↗
TwoChartCech.Sections.ofSubmodules
Documentation

The section datum of N0 and N1 restricting into N01 by inclusion.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
Lean source · statement
def Sections.ofSubmodules {R : Type u} [CommRing R] {F : Type v}
    [AddCommGroup F] [Module R F]
    (N0 N1 N01 : Submodule R F) (h0 : N0 ≤ N01) (h1 : N1 ≤ N01) :
    Sections.{u, u, v} (Cover.trivial R)
theorem

mem_H0_ofSubmodules_iff

L270 ↗
TwoChartCech.Sections.mem_H0_ofSubmodules_iff
Source context 6 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace TwoChartCech
attribute [instance] Cover.A0_commRing Cover.A0_algebra Cover.A1_commRing Cover.A1_algebra
  Cover.A01_commRing Cover.A01_algebra
attribute [instance] Sections.M0_addCommGroup Sections.M0_moduleA Sections.M0_module
  Sections.M0_tower Sections.M1_addCommGroup Sections.M1_moduleA Sections.M1_module
  Sections.M1_tower Sections.M01_addCommGroup Sections.M01_moduleA Sections.M01_module
  Sections.M01_tower
Lean source · statement
theorem Sections.mem_H0_ofSubmodules_iff {R : Type u} [CommRing R] {F : Type v} [AddCommGroup F]
    [Module R F] (N0 N1 N01 : Submodule R F) (h0 : N0 ≤ N01) (h1 : N1 ≤ N01) (p : N0 × N1) :
    p ∈ (Sections.ofSubmodules N0 N1 N01 h0 h1).H0 ↔ (p.1 : F) = p.2

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