NYLL
Module

Scheme_TwoAffineOpenCover_exists_sectionsOf_unit_equiv_structureSheafSections.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_exists_sectionsOf_unit_equiv_structureSheafSections
9 declarations indexed from sourceView source ↗

Module documentation

Unit-module and structure-sheaf Čech groups

For a two-affine-open cover, sections of the unit module and structure-sheaf sections give canonically equivalent zeroth and first Čech groups.

Imports3
Imported by4

Declarations

abbrev

SU

L52 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_sectionsOf_unit_equiv_structureSheafSections.AlgebraicGeometry.Scheme.TwoAffineOpenCover.UnitComparison.SU
Documentation

Čech sections of the unit module for the two-affine-open cover.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_sectionsOf_unit_equiv_structureSheafSections
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace UnitComparison
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
  (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
Lean source · statement
abbrev SU : TwoChartCech.Sections (𝒱.cover c)
abbrev

SO

L55 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_sectionsOf_unit_equiv_structureSheafSections.AlgebraicGeometry.Scheme.TwoAffineOpenCover.UnitComparison.SO
Documentation

Structure-sheaf Čech sections for the same cover.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_sectionsOf_unit_equiv_structureSheafSections
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace UnitComparison
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
  (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
Lean source · statement
abbrev SO : TwoChartCech.Sections (𝒱.cover c)
theorem

cechDiff_eq

L57 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_sectionsOf_unit_equiv_structureSheafSections.AlgebraicGeometry.Scheme.TwoAffineOpenCover.UnitComparison.cechDiff_eq
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_sectionsOf_unit_equiv_structureSheafSections
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace UnitComparison
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
  (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
Lean source · full declaration
theorem cechDiff_eq (s : (SU 𝒱 c).M0 × (SU 𝒱 c).M1) :
    (show (SO 𝒱 c).M01 from (SU 𝒱 c).cechDiff s)
      = (SO 𝒱 c).cechDiff (show (SO 𝒱 c).M0 × (SO 𝒱 c).M1 from s) := by
  rw [TwoChartCech.Sections.cechDiff_apply, TwoChartCech.Sections.cechDiff_apply,
    TwoChartCech.Cover.lineBundle_r1_apply, TwoChartCech.Cover.lineBundle_r0_apply,
      Units.val_one, one_mul]
  rfl
def

toFunH0

L66 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_sectionsOf_unit_equiv_structureSheafSections.AlgebraicGeometry.Scheme.TwoAffineOpenCover.UnitComparison.toFunH0
Documentation

Regard a compatible pair of unit-module sections as structure-sheaf sections.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_sectionsOf_unit_equiv_structureSheafSections
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace UnitComparison
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
  (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
Lean source · statement
def toFunH0 (x : (SU 𝒱 c).H0) : (SO 𝒱 c).H0
def

invFunH0

L73 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_sectionsOf_unit_equiv_structureSheafSections.AlgebraicGeometry.Scheme.TwoAffineOpenCover.UnitComparison.invFunH0
Documentation

Regard a compatible pair of structure-sheaf sections as unit-module sections.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_sectionsOf_unit_equiv_structureSheafSections
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace UnitComparison
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
  (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
Lean source · statement
def invFunH0 (x : (SO 𝒱 c).H0) : (SU 𝒱 c).H0
def

equivH0

L82 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_sectionsOf_unit_equiv_structureSheafSections.AlgebraicGeometry.Scheme.TwoAffineOpenCover.UnitComparison.equivH0
Documentation

The canonical linear equivalence between the two zeroth Čech groups.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_sectionsOf_unit_equiv_structureSheafSections
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace UnitComparison
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
  (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
Lean source · full declaration
def equivH0 : (SU 𝒱 c).H0 ≃ₗ[R] (SO 𝒱 c).H0 where
  toFun := toFunH0 𝒱 c
  invFun := invFunH0 𝒱 c
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  left_inv _ := rfl
  right_inv _ := rfl
theorem

range_eq

L90 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_sectionsOf_unit_equiv_structureSheafSections.AlgebraicGeometry.Scheme.TwoAffineOpenCover.UnitComparison.range_eq
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_sectionsOf_unit_equiv_structureSheafSections
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace UnitComparison
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
  (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
Lean source · full declaration
theorem range_eq :
    (show Submodule R (SO 𝒱 c).M01 from LinearMap.range (SU 𝒱 c).cechDiff)
      = LinearMap.range (SO 𝒱 c).cechDiff := by
  ext y
  constructor
  · rintro ⟨s, rfl⟩
    exact ⟨(show (SO 𝒱 c).M0 × (SO 𝒱 c).M1 from s), (cechDiff_eq 𝒱 c s).symm⟩
  · rintro ⟨s, rfl⟩
    exact ⟨(show (SU 𝒱 c).M0 × (SU 𝒱 c).M1 from s), cechDiff_eq 𝒱 c _⟩
def

equivH1

L101 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_sectionsOf_unit_equiv_structureSheafSections.AlgebraicGeometry.Scheme.TwoAffineOpenCover.UnitComparison.equivH1
Documentation

The canonical linear equivalence between the two first Čech groups.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_sectionsOf_unit_equiv_structureSheafSections
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace UnitComparison
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
  (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
Lean source · statement
def equivH1 : (SU 𝒱 c).H1 ≃ₗ[R] (SO 𝒱 c).H1
theorem

exists_sectionsOf_unit_equiv_structureSheafSections

L111 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.exists_sectionsOf_unit_equiv_structureSheafSections
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_sectionsOf_unit_equiv_structureSheafSections
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
with_weak_namespace AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover TwoAffineOpenCover in
with_weak_namespace _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · full declaration
theorem exists_sectionsOf_unit_equiv_structureSheafSections
    {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R)) :
    ∃ (e0 : (𝒱.sectionsOf c (SheafOfModules.unit X.ringCatSheaf : X.Modules)).H0 ≃ₗ[R]
          (𝒱.structureSheafSections c).H0)
      (e1 : (𝒱.sectionsOf c (SheafOfModules.unit X.ringCatSheaf : X.Modules)).H1 ≃ₗ[R]
          (𝒱.structureSheafSections c).H1),
      (∀ x, ((e0 x : (𝒱.structureSheafSections c).M0 × (𝒱.structureSheafSections c).M1)) = x.1) ∧
      (∀ y : (𝒱.sectionsOf c (SheafOfModules.unit X.ringCatSheaf : X.Modules)).M01,
          e1 (Submodule.Quotient.mk y)
            = Submodule.Quotient.mk (show (𝒱.structureSheafSections c).M01 from y)) :=
  ⟨UnitComparison.equivH0 𝒱 c, UnitComparison.equivH1 𝒱 c, fun _ => rfl, fun _ => rfl⟩

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