Module

Scheme_Modules_nonempty_pushforward_hom_comp_iso.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_pushforward_hom_comp_iso

3 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules nonempty pushforward hom comp iso

Imports4

Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.CategoryTheory.Adjunction.Basic
Mathlib.CategoryTheory.Adjunction.Unique
Mathlib.CategoryTheory.Equivalence

Imported by2

def

pushEquiv

L35 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pushforward_hom_comp_iso.PushIso.pushEquiv

Documentation

The equivalence of module sheaves induced by pushforward along the scheme isomorphism φ.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pushforward_hom_comp_iso
universe u
open CategoryTheory AlgebraicGeometry
namespace PushIso
variable {X Y : Scheme.{u}} (φ : X ≅ Y)

Lean source · statement

def pushEquiv : X.Modules ≌ Y.Modules

def

pullbackIsoPushforwardInv

L45 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pushforward_hom_comp_iso.PushIso.pullbackIsoPushforwardInv

Documentation

Identify pullback along φ.hom with pushforward along φ.inv using uniqueness of left adjoints.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pushforward_hom_comp_iso
universe u
open CategoryTheory AlgebraicGeometry
namespace PushIso
variable {X Y : Scheme.{u}} (φ : X ≅ Y)

Lean source · statement

def pullbackIsoPushforwardInv :
    Scheme.Modules.pullback φ.hom ≅ Scheme.Modules.pushforward φ.inv

theorem

nonempty_pushforward_hom_comp_iso

L52 ↗

AlgebraicGeometry.Scheme.Modules.nonempty_pushforward_hom_comp_iso

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pushforward_hom_comp_iso
universe u
open CategoryTheory AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.nonempty_pushforward_hom_comp_iso
    {X Y Z : Scheme.{u}} (e : X ≅ Y) (f : Y ⟶ Z) (F : X.Modules) :
    Nonempty ((Scheme.Modules.pushforward (e.hom ≫ f)).obj F ≅
      (Scheme.Modules.pushforward f).obj ((Scheme.Modules.pullback e.inv).obj F))

Module documentation

Scheme Modules nonempty pushforward hom comp iso

Declarations

pushEquiv

pullbackIsoPushforwardInv

nonempty_pushforward_hom_comp_iso