NYLL
Module

Scheme_Modules_nonempty_pullback_exteriorPower_iso_exteriorPower_pullback.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_pullback_exteriorPower_iso_exteriorPower_pullback
8 declarations indexed from sourceView source ↗

Module documentation

Pullback to an open commutes with exterior powers

Restriction commutes with presheaf exterior powers, and sheafification transports this comparison to pullback of module sheaves.

Imports2
Imported by3

Declarations

def

restrictPresheaf₀CompPresheafExteriorPowerIso

L45 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_exteriorPower_iso_exteriorPower_pullback.AlgebraicGeometry.Scheme.Modules.restrictPresheaf₀CompPresheafExteriorPowerIso
Documentation

Restriction along the open indexing functor commutes with presheaf exterior powers.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_exteriorPower_iso_exteriorPower_pullback
universe u
open CategoryTheory
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
def restrictPresheaf₀CompPresheafExteriorPowerIso (n : ℕ) (U : X.Opens) :
    presheafExteriorPower X n ⋙ restrictPresheaf₀ U ≅
      restrictPresheaf₀ U ⋙ presheafExteriorPower (U : Scheme.{u}) n
def

restrictPresheafCompPresheafExteriorPowerIso

L58 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_exteriorPower_iso_exteriorPower_pullback.AlgebraicGeometry.Scheme.Modules.restrictPresheafCompPresheafExteriorPowerIso
Documentation

The restriction comparison transported to the ring-sheaf restriction functor.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_exteriorPower_iso_exteriorPower_pullback
universe u
open CategoryTheory
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
def restrictPresheafCompPresheafExteriorPowerIso (n : ℕ) (U : X.Opens) :
    presheafExteriorPower X n ⋙ restrictPresheaf U ≅
      restrictPresheaf U ⋙ presheafExteriorPower (U : Scheme.{u}) n
def

pullbackExteriorPowerIso_step1

L69 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_exteriorPower_iso_exteriorPower_pullback.AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerIso_step1
Documentation

The comparison between pullback of the sheafified power and sheafified restriction.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_exteriorPower_iso_exteriorPower_pullback
universe u
open CategoryTheory
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section steps
variable (n : ℕ) (U : X.Opens) (M : X.Modules)
Lean source · statement
def pullbackExteriorPowerIso_step1 :
    (Modules.pullback U.ι).obj ((exteriorPower X n).obj M) ≅
      (PresheafOfModules.sheafification (𝟙 (U : Scheme.{u}).ringCatSheaf.obj)).obj
        ((restrictPresheaf U).obj ((presheafExteriorPower X n).obj M.val))
def

pullbackExteriorPowerIso_step2

L76 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_exteriorPower_iso_exteriorPower_pullback.AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerIso_step2
Documentation

The sheafified comparison between exterior power before and after restriction.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_exteriorPower_iso_exteriorPower_pullback
universe u
open CategoryTheory
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section steps
variable (n : ℕ) (U : X.Opens) (M : X.Modules)
Lean source · statement
def pullbackExteriorPowerIso_step2 :
    (PresheafOfModules.sheafification (𝟙 (U : Scheme.{u}).ringCatSheaf.obj)).obj
        ((restrictPresheaf U).obj ((presheafExteriorPower X n).obj M.val)) ≅
      (PresheafOfModules.sheafification (𝟙 (U : Scheme.{u}).ringCatSheaf.obj)).obj
        ((presheafExteriorPower (U : Scheme.{u}) n).obj ((restrictPresheaf U).obj M.val))
def

pullbackExteriorPowerIso_step25

L85 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_exteriorPower_iso_exteriorPower_pullback.AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerIso_step25
Documentation

The sheafified restricted power identified with the exterior power of the restriction.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_exteriorPower_iso_exteriorPower_pullback
universe u
open CategoryTheory
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section steps
variable (n : ℕ) (U : X.Opens) (M : X.Modules)
Lean source · statement
def pullbackExteriorPowerIso_step25 :
    (PresheafOfModules.sheafification (𝟙 (U : Scheme.{u}).ringCatSheaf.obj)).obj
        ((presheafExteriorPower (U : Scheme.{u}) n).obj ((restrictPresheaf U).obj M.val)) ≅
      (exteriorPower (U : Scheme.{u}) n).obj ((restrictOpen U).obj M)
def

pullbackExteriorPowerIso_step3

L92 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_exteriorPower_iso_exteriorPower_pullback.AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerIso_step3
Documentation

The exterior-power comparison induced by the restriction-pullback isomorphism.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_exteriorPower_iso_exteriorPower_pullback
universe u
open CategoryTheory
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section steps
variable (n : ℕ) (U : X.Opens) (M : X.Modules)
Lean source · statement
def pullbackExteriorPowerIso_step3 :
    (exteriorPower (U : Scheme.{u}) n).obj ((restrictOpen U).obj M) ≅
      (exteriorPower (U : Scheme.{u}) n).obj ((Modules.pullback U.ι).obj M)
def

pullbackExteriorPowerIso

L100 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_exteriorPower_iso_exteriorPower_pullback.AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerIso
Documentation

The canonical isomorphism commuting pullback to the open with exterior power.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_exteriorPower_iso_exteriorPower_pullback
universe u
open CategoryTheory
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
def pullbackExteriorPowerIso (n : ℕ) (U : X.Opens) (M : X.Modules) :
    (Modules.pullback U.ι).obj ((exteriorPower X n).obj M) ≅
      (exteriorPower (U : Scheme.{u}) n).obj ((Modules.pullback U.ι).obj M)
theorem

nonempty_pullback_exteriorPower_iso_exteriorPower_pullback

L109 ↗
AlgebraicGeometry.Scheme.Modules.nonempty_pullback_exteriorPower_iso_exteriorPower_pullback
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_exteriorPower_iso_exteriorPower_pullback
universe u
open CategoryTheory
open _root_.AlgebraicGeometry AlgebraicGeometry in
Lean source · statement
theorem
  _root_.AlgebraicGeometry.Scheme.Modules.nonempty_pullback_exteriorPower_iso_exteriorPower_pullback
  {X : Scheme.{u}} (n : ℕ) (U : X.Opens) (M : X.Modules) :
    Nonempty ((Scheme.Modules.pullback U.ι).obj ((Scheme.Modules.exteriorPower X n).obj M) ≅
      (Scheme.Modules.exteriorPower (U : Scheme.{u}) n).obj ((Scheme.Modules.pullback U.ι).obj M))

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