NYLL
Module

Exists_twoAffineOpenCover_fibre_linearEquiv_sectionsOf_of_isPullback.lean

Nyll.AlgebraicCurves.Geometry.Picard.Exists_twoAffineOpenCover_fibre_linearEquiv_sectionsOf_of_isPullback
5 declarations indexed from sourceView source ↗

Module documentation

Transporting two-chart fibre cohomology along a Cartesian square

A Cartesian identification of a fibre transports a two-affine-open cover and induces linear equivalences on the zeroth and first cohomology of the corresponding modules.

Imports11
Imported by12

Declarations

def

φ

L64 ↗
AlgebraicCurves.Geometry.Picard.Proofs.Exists_twoAffineOpenCover_fibre_linearEquiv_sectionsOf_of_isPullback.AlgebraicGeometry.RelPicard.TransportGen.φ
Documentation

The pullback identification of the geometric fibre with the given Cartesian scheme.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Exists_twoAffineOpenCover_fibre_linearEquiv_sectionsOf_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace TransportGen
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C T : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (t : T ⟶ Spec (CommRingCat.of R)) (M : (pullback c t).Modules)
  {k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ T)
  {Y : Scheme.{u}} (y : Y ⟶ Spec (CommRingCat.of k)) (g' : Y ⟶ pullback c t)
  (hcart : IsPullback g' y (pullback.snd c t) s)
Lean source · statement
def φ : pullback (pullback.snd c t) s ≅ Y
theorem

φ_hom_y

L66 ↗
AlgebraicCurves.Geometry.Picard.Proofs.Exists_twoAffineOpenCover_fibre_linearEquiv_sectionsOf_of_isPullback.AlgebraicGeometry.RelPicard.TransportGen.φ_hom_y
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Exists_twoAffineOpenCover_fibre_linearEquiv_sectionsOf_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace TransportGen
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C T : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (t : T ⟶ Spec (CommRingCat.of R)) (M : (pullback c t).Modules)
  {k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ T)
  {Y : Scheme.{u}} (y : Y ⟶ Spec (CommRingCat.of k)) (g' : Y ⟶ pullback c t)
  (hcart : IsPullback g' y (pullback.snd c t) s)
Lean source · statement
theorem φ_hom_y : (φ c t s y g' hcart).hom ≫ y = fibreAt c t s
def

modIso

L72 ↗
AlgebraicCurves.Geometry.Picard.Proofs.Exists_twoAffineOpenCover_fibre_linearEquiv_sectionsOf_of_isPullback.AlgebraicGeometry.RelPicard.TransportGen.modIso
Documentation

The module comparison obtained by transport along the Cartesian identification and composition of pullback functors.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Exists_twoAffineOpenCover_fibre_linearEquiv_sectionsOf_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace TransportGen
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C T : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (t : T ⟶ Spec (CommRingCat.of R)) (M : (pullback c t).Modules)
  {k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ T)
  {Y : Scheme.{u}} (y : Y ⟶ Spec (CommRingCat.of k)) (g' : Y ⟶ pullback c t)
  (hcart : IsPullback g' y (pullback.snd c t) s)
Lean source · statement
def modIso : fibreModule c t s M ≅ (Scheme.Modules.pullback (φ c t s y g' hcart).hom).obj
    ((Scheme.Modules.pullback g').obj M)
theorem

main

L78 ↗
AlgebraicCurves.Geometry.Picard.Proofs.Exists_twoAffineOpenCover_fibre_linearEquiv_sectionsOf_of_isPullback.AlgebraicGeometry.RelPicard.TransportGen.main
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Exists_twoAffineOpenCover_fibre_linearEquiv_sectionsOf_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace TransportGen
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C T : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (t : T ⟶ Spec (CommRingCat.of R)) (M : (pullback c t).Modules)
  {k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ T)
  {Y : Scheme.{u}} (y : Y ⟶ Spec (CommRingCat.of k)) (g' : Y ⟶ pullback c t)
  (hcart : IsPullback g' y (pullback.snd c t) s)
include hcart in
Lean source · statement
theorem main (F : Y.Modules) (e : F ≅ (Scheme.Modules.pullback g').obj M) (𝒱 :
    Y.TwoAffineOpenCover) :
    ∃ 𝒲 : (pullback (pullback.snd c t) s).TwoAffineOpenCover,
      Nonempty ((𝒱.sectionsOf y F).H0 ≃ₗ[k] (𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s
          M)).H0) ∧
      Nonempty ((𝒱.sectionsOf y F).H1 ≃ₗ[k] (𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s
          M)).H1)
theorem

exists_twoAffineOpenCover_fibre_linearEquiv_sectionsOf_of_isPullback

L97 ↗
AlgebraicGeometry.RelPicard.exists_twoAffineOpenCover_fibre_linearEquiv_sectionsOf_of_isPullback
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Exists_twoAffineOpenCover_fibre_linearEquiv_sectionsOf_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open AlgebraicGeometry.RelPicard in
with_weak_namespace _root_.AlgebraicGeometry.RelPicard
Lean source · statement
theorem exists_twoAffineOpenCover_fibre_linearEquiv_sectionsOf_of_isPullback
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M : (pullback c t).Modules)
    {k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ T)
    {Y : Scheme.{u}} (y : Y ⟶ Spec (CommRingCat.of k)) (g' : Y ⟶ pullback c t)
    (hcart : IsPullback g' y (pullback.snd c t) s)
    (F : Y.Modules) (e : F ≅ (Scheme.Modules.pullback g').obj M) (𝒱 : Y.TwoAffineOpenCover) :
    ∃ 𝒲 : (pullback (pullback.snd c t) s).TwoAffineOpenCover,
      Nonempty ((𝒱.sectionsOf y F).H0 ≃ₗ[k] (𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s
          M)).H0) ∧
      Nonempty ((𝒱.sectionsOf y F).H1 ≃ₗ[k] (𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s
          M)).H1)

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