Module

OModulePresheafCechPushforward.lean

Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheafCechPushforward

25 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf Cech Pushforward

Imports2

Imported by2

abbrev

chart

L36 ↗

AlgebraicGeometry.OModulePresheaf.cechPushforward.chart

Documentation

Intersect a cover chart with the preimage of the given open subset.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
namespace cechPushforward

Lean source · statement

abbrev chart (U : Z.Opens) (i : K'.ι) : V'.Opens

theorem

chart_le_preimage

L38 ↗

AlgebraicGeometry.OModulePresheaf.cechPushforward.chart_le_preimage

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
namespace cechPushforward

Lean source · statement

theorem chart_le_preimage (U : Z.Opens) (i : K'.ι) : chart p K' U i ≤ p ⁻¹ᵁ U

theorem

chart_mono

L40 ↗

AlgebraicGeometry.OModulePresheaf.cechPushforward.chart_mono

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
namespace cechPushforward

Lean source · statement

theorem chart_mono {U U' : Z.Opens} (h : U ≤ U') (i : K'.ι) : chart p K' U i ≤ chart p K' U' i

def

cocycles

L46 ↗

AlgebraicGeometry.OModulePresheaf.cechPushforward.cocycles

Documentation

Families of sections on the charts that agree on every pairwise intersection.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
namespace cechPushforward
variable (G : OModulePresheaf (p ≫ πZ))

Lean source · statement

def cocycles (U : Z.Opens) : Submodule R (∀ i : K'.ι, G.obj (chart p K' U i))

theorem

mem_cocycles_iff

L51 ↗

AlgebraicGeometry.OModulePresheaf.cechPushforward.mem_cocycles_iff

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
namespace cechPushforward
variable (G : OModulePresheaf (p ≫ πZ))

Lean source · statement

theorem mem_cocycles_iff (U : Z.Opens) (x : ∀ i : K'.ι, G.obj (chart p K' U i)) :
    x ∈ cocycles p πZ K' G U ↔ ∀ i j : K'.ι,
      G.res (U := chart p K' U i ⊓ chart p K' U j) inf_le_left (x i)
        = G.res (U := chart p K' U i ⊓ chart p K' U j) inf_le_right (x j)

abbrev

toChart

L60 ↗

AlgebraicGeometry.OModulePresheaf.cechPushforward.toChart

Documentation

Pull a section on the base open subset back to one chart of its preimage.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
namespace cechPushforward
variable (G : OModulePresheaf (p ≫ πZ))

Lean source · statement

abbrev toChart (U : Z.Opens) (i : K'.ι) : Γ(Z, U) ⟶ Γ(V', chart p K' U i)

theorem

toChart_algebraMap

L63 ↗

AlgebraicGeometry.OModulePresheaf.cechPushforward.toChart_algebraMap

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
namespace cechPushforward
variable (G : OModulePresheaf (p ≫ πZ))

Lean source · full declaration

theorem toChart_algebraMap (U : Z.Opens) (i : K'.ι) (r : R) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom πZ U
    letI := Scheme.TwoAffineOpenCover.algebraOfHom (p ≫ πZ) (chart p K' U i)
    (toChart p K' U i).hom (algebraMap R Γ(Z, U) r) = algebraMap R Γ(V', chart p K' U i) r := by
  have hZTop : U ≤ πZ ⁻¹ᵁ (⊤ : (Spec (.of R)).Opens) := by
    rw [Scheme.Hom.preimage_top]
    exact le_top
  have hVTop : chart p K' U i ≤ (p ≫ πZ) ⁻¹ᵁ (⊤ : (Spec (.of R)).Opens) := by
    rw [Scheme.Hom.preimage_top]
    exact le_top
  change (p.appLE U _ _).hom ((πZ.appLE ⊤ U hZTop).hom _) =
    ((p ≫ πZ).appLE ⊤ _ hVTop).hom _
  rw [← CommRingCat.comp_apply, Scheme.Hom.appLE_comp_appLE]

theorem

map_toChart_left

L77 ↗

AlgebraicGeometry.OModulePresheaf.cechPushforward.map_toChart_left

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
namespace cechPushforward
variable (G : OModulePresheaf (p ≫ πZ))

Lean source · statement

theorem map_toChart_left (U : Z.Opens) (i j : K'.ι) (a : Γ(Z, U)) :
    (V'.presheaf.map (homOfLE (inf_le_left : chart p K' U i ⊓ chart p K' U j ≤ chart p K' U
      i)).op).hom
        ((toChart p K' U i).hom a)
      = (p.appLE U (chart p K' U i ⊓ chart p K' U j) (inf_le_left.trans (chart_le_preimage p K'
        U i))).hom a

theorem

map_toChart_right

L85 ↗

AlgebraicGeometry.OModulePresheaf.cechPushforward.map_toChart_right

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
namespace cechPushforward
variable (G : OModulePresheaf (p ≫ πZ))

Lean source · statement

theorem map_toChart_right (U : Z.Opens) (i j : K'.ι) (a : Γ(Z, U)) :
    (V'.presheaf.map (homOfLE (inf_le_right : chart p K' U i ⊓ chart p K' U j ≤ chart p K' U
      j)).op).hom
        ((toChart p K' U j).hom a)
      = (p.appLE U (chart p K' U i ⊓ chart p K' U j) (inf_le_left.trans (chart_le_preimage p K'
        U i))).hom a

def

sectionsSMul

L94 ↗

AlgebraicGeometry.OModulePresheaf.cechPushforward.sectionsSMul

Documentation

The action of base sections on compatible chart families through their pullbacks.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
namespace cechPushforward
variable (G : OModulePresheaf (p ≫ πZ))

Lean source · full declaration

def sectionsSMul (U : Z.Opens) : SMul Γ(Z, U) (cocycles p πZ K' G U) where
  smul a x := ⟨fun i => (toChart p K' U i).hom a • x.1 i, by
    rw [mem_cocycles_iff]
    intro i j
    rw [G.res_smul, G.res_smul, map_toChart_left, map_toChart_right,
      (mem_cocycles_iff p πZ K' G U x.1).mp x.2 i j]⟩

def

sectionsModule

L102 ↗

AlgebraicGeometry.OModulePresheaf.cechPushforward.sectionsModule

Documentation

The module structure over base sections on compatible chart families.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
namespace cechPushforward
variable (G : OModulePresheaf (p ≫ πZ))

Lean source · statement

def sectionsModule (U : Z.Opens) : Module Γ(Z, U) (cocycles p πZ K' G U)

theorem

res_mem

L121 ↗

AlgebraicGeometry.OModulePresheaf.cechPushforward.res_mem

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
namespace cechPushforward
variable (G : OModulePresheaf (p ≫ πZ))

Lean source · full declaration

theorem res_mem {U U' : Z.Opens} (h : U ≤ U') (x : cocycles p πZ K' G U') :
    (fun i => G.res (chart_mono p K' h i) (x.1 i)) ∈ cocycles p πZ K' G U := by
  rw [mem_cocycles_iff]
  intro i j
  rw [G.res_res, G.res_res,
    ← G.res_res (inf_le_inf (chart_mono p K' h i) (chart_mono p K' h j))
      (inf_le_left : chart p K' U' i ⊓ chart p K' U' j ≤ _),
    ← G.res_res (inf_le_inf (chart_mono p K' h i) (chart_mono p K' h j))
      (inf_le_right : chart p K' U' i ⊓ chart p K' U' j ≤ _),
    (mem_cocycles_iff p πZ K' G U' x.1).mp x.2 i j]

def

resL

L133 ↗

AlgebraicGeometry.OModulePresheaf.cechPushforward.resL

Documentation

Restrict compatible chart families when the base open subset shrinks.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
namespace cechPushforward
variable (G : OModulePresheaf (p ≫ πZ))

Lean source · full declaration

def resL {U U' : Z.Opens} (h : U ≤ U') : cocycles p πZ K' G U' →ₗ[R] cocycles p πZ K' G U where
  toFun x := ⟨fun i => G.res (chart_mono p K' h i) (x.1 i), res_mem p πZ K' G h x⟩
  map_add' x y := Subtype.ext (funext fun i => (G.res (chart_mono p K' h i)).map_add (x.1 i)
    (y.1 i))
  map_smul' r x := Subtype.ext (funext fun i => (G.res (chart_mono p K' h i)).map_smul r (x.1 i))

def

cechPushforward

L143 ↗

AlgebraicGeometry.OModulePresheaf.cechPushforward

Documentation

Push the module presheaf forward by taking compatible families on the chosen cover.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
open cechPushforward in

Lean source · full declaration

def cechPushforward (G : OModulePresheaf (p ≫ πZ)) : OModulePresheaf πZ where
  obj U := cocycles p πZ K' G U
  module U := inferInstance
  moduleSections U := sectionsModule p πZ K' G U
  isScalarTower U := by
    let := Scheme.TwoAffineOpenCover.algebraOfHom πZ U
    let := sectionsModule p πZ K' G U
    refine ⟨fun r a x => Subtype.ext (funext fun i => ?_)⟩
    let := Scheme.TwoAffineOpenCover.algebraOfHom (p ≫ πZ) (chart p K' U i)
    change (toChart p K' U i).hom (r • a) • x.1 i = r • ((toChart p K' U i).hom a • x.1 i)
    rw [Algebra.smul_def, map_mul, mul_smul, toChart_algebraMap, algebraMap_smul]
  res h := resL p πZ K' G h
  res_smul {U U'} h a x := Subtype.ext (funext fun i => by
    change G.res _ ((toChart p K' U' i).hom a • x.1 i)
      = (toChart p K' U i).hom ((Z.presheaf.map (homOfLE h).op).hom a) • G.res (chart_mono p K'
        h i) (x.1 i)
    rw [G.res_smul, ← CommRingCat.comp_apply, ← CommRingCat.comp_apply (f := Z.presheaf.map _),
      Scheme.Hom.appLE_map, Scheme.Hom.map_appLE])
  res_refl U := LinearMap.ext fun x => Subtype.ext (funext fun i => G.res_refl_apply _ _)
  res_comp h h' := LinearMap.ext fun x => Subtype.ext (funext fun i => (G.res_res _ _ _).symm)

theorem

cechPushforward_obj

L168 ↗

AlgebraicGeometry.OModulePresheaf.cechPushforward_obj

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
section Lemmas
variable (G : OModulePresheaf (p ≫ πZ))

Lean source · statement

theorem cechPushforward_obj (U : Z.Opens) :
    (cechPushforward p πZ K' G).obj U = ↥(cechPushforward.cocycles p πZ K' G U)

theorem

coe_res

L173 ↗

AlgebraicGeometry.OModulePresheaf.cechPushforward.coe_res

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
section Lemmas
variable (G : OModulePresheaf (p ≫ πZ))
namespace cechPushforward

Lean source · statement

theorem coe_res {U U' : Z.Opens} (h : U ≤ U') (x : (cechPushforward p πZ K' G).obj U') (i : K'.ι) :
    ((cechPushforward p πZ K' G).res h x).1 i = G.res (cechPushforward.chart_mono p K' h i) (x.1
      i)

theorem

coe_smul

L177 ↗

AlgebraicGeometry.OModulePresheaf.cechPushforward.coe_smul

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
section Lemmas
variable (G : OModulePresheaf (p ≫ πZ))
namespace cechPushforward

Lean source · statement

theorem coe_smul (U : Z.Opens) (r : R) (x : (cechPushforward p πZ K' G).obj U) (i : K'.ι) :
    (r • x).1 i = r • x.1 i

theorem

coe_sectionsSMul

L180 ↗

AlgebraicGeometry.OModulePresheaf.cechPushforward.coe_sectionsSMul

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
section Lemmas
variable (G : OModulePresheaf (p ≫ πZ))
namespace cechPushforward

Lean source · statement

theorem coe_sectionsSMul (U : Z.Opens) (a : Γ(Z, U)) (x : (cechPushforward p πZ K' G).obj U) (i
  : K'.ι) :
    (a • x).1 i = (cechPushforward.toChart p K' U i).hom a • x.1 i

theorem

coe_add

L184 ↗

AlgebraicGeometry.OModulePresheaf.cechPushforward.coe_add

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
section Lemmas
variable (G : OModulePresheaf (p ≫ πZ))
namespace cechPushforward

Lean source · statement

theorem coe_add (U : Z.Opens) (x y : (cechPushforward p πZ K' G).obj U) (i : K'.ι) :
    (x + y).1 i = x.1 i + y.1 i

theorem

ext

L187 ↗

AlgebraicGeometry.OModulePresheaf.cechPushforward.ext

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
section Lemmas
variable (G : OModulePresheaf (p ≫ πZ))
namespace cechPushforward

Lean source · statement

theorem ext {U : Z.Opens} {x y : (cechPushforward p πZ K' G).obj U} (h : ∀ i, x.1 i = y.1 i) : x
  = y

def

cechPushforward

L200 ↗

AlgebraicGeometry.OModulePresheaf.Hom.cechPushforward

Documentation

Push a presheaf morphism forward by applying it to each chart section.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
namespace Hom
variable {G G' : OModulePresheaf (p ≫ πZ)}

Lean source · full declaration

def cechPushforward (φ : Hom G G') :
    Hom (OModulePresheaf.cechPushforward p πZ K' G) (OModulePresheaf.cechPushforward p πZ K' G')
      where
  app U :=
    { toFun := fun x => ⟨fun i => φ.app _ (x.1 i), by
        rw [cechPushforward.mem_cocycles_iff]
        intro i j
        rw [← φ.naturality_apply, ← φ.naturality_apply,
          (cechPushforward.mem_cocycles_iff p πZ K' G U x.1).mp x.2 i j]⟩
      map_add' := fun x y => Subtype.ext (funext fun i => map_add _ _ _)
      map_smul' := fun r x => Subtype.ext (funext fun i => LinearMap.map_smul _ _ _) }
  app_smul U a x := Subtype.ext (funext fun i => φ.app_smul _ _ _)
  naturality h := LinearMap.ext fun x => Subtype.ext (funext fun i => φ.naturality_apply _ _)

theorem

coe_cechPushforward_app

L214 ↗

AlgebraicGeometry.OModulePresheaf.Hom.coe_cechPushforward_app

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
namespace Hom
variable {G G' : OModulePresheaf (p ≫ πZ)}

Lean source · statement

theorem coe_cechPushforward_app (φ : Hom G G') (U : Z.Opens)
    (x : (OModulePresheaf.cechPushforward p πZ K' G).obj U) (i : K'.ι) :
    ((φ.cechPushforward p πZ K').app U x).1 i = φ.app _ (x.1 i)

abbrev

affineChart

L225 ↗

AlgebraicGeometry.OModulePresheaf.AffHom.affineChart

Documentation

View the intersection chart over an affine base open as an affine open subset.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
namespace AffHom
variable {G G' : OModulePresheaf (p ≫ πZ)}

Lean source · statement

abbrev affineChart [IsSeparated πZ] (U : Z.affineOpens) (i : K'.ι) : V'.affineOpens

def

cechPushforward

L230 ↗

AlgebraicGeometry.OModulePresheaf.AffHom.cechPushforward

Documentation

Push an affine presheaf morphism forward through its maps on the affine charts.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
namespace AffHom
variable {G G' : OModulePresheaf (p ≫ πZ)}

Lean source · full declaration

def cechPushforward [IsSeparated πZ] [IsSeparated p] (φ : AffHom G G') :
    AffHom (OModulePresheaf.cechPushforward p πZ K' G) (OModulePresheaf.cechPushforward p πZ K'
      G') where
  app U :=
    { toFun := fun x => ⟨fun i => φ.app (affineChart p πZ K' U i) (x.1 i), by
        rw [OModulePresheaf.cechPushforward.mem_cocycles_iff]
        intro i j
        have hij : IsAffineOpen (OModulePresheaf.cechPushforward.chart p K' U.1 i
            ⊓ OModulePresheaf.cechPushforward.chart p K' U.1 j) :=
          haveI : IsSeparated (p ≫ πZ) := inferInstance
          Scheme.OrderedAffineCover.isAffineOpen_inf_of_isSeparated (p ≫ πZ)
            (affineChart p πZ K' U i).2 (affineChart p πZ K' U j).2
        rw [← φ.naturality_apply (U := ⟨_, hij⟩) (U' := affineChart p πZ K' U i),
          ← φ.naturality_apply (U := ⟨_, hij⟩) (U' := affineChart p πZ K' U j),
          (OModulePresheaf.cechPushforward.mem_cocycles_iff p πZ K' G U.1 x.1).mp x.2 i j]⟩
      map_add' := fun x y => Subtype.ext (funext fun i => map_add _ _ _)
      map_smul' := fun r x => Subtype.ext (funext fun i => LinearMap.map_smul _ _ _) }
  app_smul U a x := Subtype.ext (funext fun i => φ.app_smul _ _ _)
  naturality {U U'} h := LinearMap.ext fun x => Subtype.ext (funext fun i =>
    φ.naturality_apply (U := affineChart p πZ K' U i) (U' := affineChart p πZ K' U' i) _ _)

theorem

coe_cechPushforward_app

L251 ↗

AlgebraicGeometry.OModulePresheaf.AffHom.coe_cechPushforward_app

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R)) (K' : V'.OrderedAffineCover)
namespace AffHom
variable {G G' : OModulePresheaf (p ≫ πZ)}

Lean source · statement

theorem coe_cechPushforward_app [IsSeparated πZ] [IsSeparated p] (φ : AffHom G G') (U :
  Z.affineOpens)
    (x : (OModulePresheaf.cechPushforward p πZ K' G).obj U.1) (i : K'.ι) :
    ((φ.cechPushforward p πZ K').app U x).1 i = φ.app (affineChart p πZ K' U i) (x.1 i)

Module documentation

OModule Presheaf Cech Pushforward

Declarations