Module

Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff

54 declarations indexed from sourceView source ↗

Module documentation

Compatibility of the projection morphism with restriction and pullback on an open subscheme.

Imports18

Imported by4

instance

projectionPresheafSectionsModule

L51 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.projectionPresheafSectionsModule

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal

Lean source · statement

instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U))

instance

e_hom_app_pullbackLocalSection

L147 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections.e_hom_app_pullbackLocalSection

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
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
namespace PullbackTensorSections
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
local instance : (PresheafOfModules.pushforward.{u}
    (F := TopologicalSpace.Opens.map f.base) f.toRingCatSheafHom.hom).IsRightAdjoint :=
  (PresheafOfModules.PullbackMonoidal.adj (TopologicalSpace.Opens.map f.base)
    (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c).isRightAdjoint
local instance : (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Modules.pullbackPushforwardAdjunction f).isRightAdjoint
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
local instance : (pf f).LaxMonoidal :=
  PresheafOfModules.pushforward_laxMonoidal
    (F := TopologicalSpace.Opens.map f.base) (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c

Lean source · statement

lemma e_hom_app_pullbackLocalSection (P : Y.PresheafOfModules) (V : Y.Opens) (s : P.obj (op V)) :
    Scheme.Modules.Hom.app ((e f).hom.app P) (f ⁻¹ᵁ V) (pullbackLocalSection f (shUnit P V s)) =
      shUnit ((pullback₀ f).obj P) (f ⁻¹ᵁ V) (pb₀Section f P V s)

lemma

δ_sheafify_comp_pullback_app_shUnit_tmul

L255 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections.δ_sheafify_comp_pullback_app_shUnit_tmul

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
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
namespace PullbackTensorSections
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
local instance : (PresheafOfModules.pushforward.{u}
    (F := TopologicalSpace.Opens.map f.base) f.toRingCatSheafHom.hom).IsRightAdjoint :=
  (PresheafOfModules.PullbackMonoidal.adj (TopologicalSpace.Opens.map f.base)
    (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c).isRightAdjoint
local instance : (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Modules.pullbackPushforwardAdjunction f).isRightAdjoint
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
local instance : (pf f).LaxMonoidal :=
  PresheafOfModules.pushforward_laxMonoidal
    (F := TopologicalSpace.Opens.map f.base) (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c

Lean source · statement

lemma δ_sheafify_comp_pullback_app_shUnit_tmul (P Q : Y.PresheafOfModules) (V : Y.Opens)
    (x : P.obj (op V)) (y : Q.obj (op V)) :
    Scheme.Modules.Hom.app (δ (Modules.sheafify Y ⋙ Modules.pullback f) P Q) (f ⁻¹ᵁ V)
      (pullbackLocalSection f (shUnit (P ⊗ Q) V (x ⊗ₜ[Γ(Y, V)] y))) =
      Modules.tensorSections (pullbackLocalSection f (shUnit P V x))
        (pullbackLocalSection f (shUnit Q V y))

theorem

pullbackTensorObjIso_hom_app_pullbackLocalSection_tensorSections

L297 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections.pullbackTensorObjIso_hom_app_pullbackLocalSection_tensorSections

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
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
namespace PullbackTensorSections
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
local instance : (PresheafOfModules.pushforward.{u}
    (F := TopologicalSpace.Opens.map f.base) f.toRingCatSheafHom.hom).IsRightAdjoint :=
  (PresheafOfModules.PullbackMonoidal.adj (TopologicalSpace.Opens.map f.base)
    (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c).isRightAdjoint
local instance : (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Modules.pullbackPushforwardAdjunction f).isRightAdjoint
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
local instance : (pf f).LaxMonoidal :=
  PresheafOfModules.pushforward_laxMonoidal
    (F := TopologicalSpace.Opens.map f.base) (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c

Lean source · statement

theorem pullbackTensorObjIso_hom_app_pullbackLocalSection_tensorSections (L M : Y.Modules) (V :
    Y.Opens)
    (s : Γ(L, V)) (t : Γ(M, V)) :
    ((pullbackTensorObjIso f L M).hom.app (f ⁻¹ᵁ V)) (pullbackLocalSection f
      (Modules.tensorSections s t)) =
      Modules.tensorSections (pullbackLocalSection f s) (pullbackLocalSection f t)

lemma

pf_ε_app

L366 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections.pf_ε_app

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
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
namespace PullbackTensorSections
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
local instance : (PresheafOfModules.pushforward.{u}
    (F := TopologicalSpace.Opens.map f.base) f.toRingCatSheafHom.hom).IsRightAdjoint :=
  (PresheafOfModules.PullbackMonoidal.adj (TopologicalSpace.Opens.map f.base)
    (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c).isRightAdjoint
local instance : (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Modules.pullbackPushforwardAdjunction f).isRightAdjoint
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
local instance : (pf f).LaxMonoidal :=
  PresheafOfModules.pushforward_laxMonoidal
    (F := TopologicalSpace.Opens.map f.base) (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c

Lean source · full declaration

lemma pf_ε_app (V : Y.Opens) (g : (𝟙_ Y.PresheafOfModules).obj (op V)) :
    (ε (pf f)).app (op V) g = (f.app V (show Γ(Y, V) from g) :
      ((pf f).obj (𝟙_ X.PresheafOfModules)).obj (op V)) := by
  let : (PresheafOfModules.restrictScalars
      (PresheafOfModules.ringCatHom (R := (TopologicalSpace.Opens.map f.base).op ⋙ X.sheaf.obj)
        f.c)).LaxMonoidal :=
    PresheafOfModules.restrictScalars_laxMonoidal
      (R := (TopologicalSpace.Opens.map f.base).op ⋙ X.sheaf.obj) (S := Y.sheaf.obj) f.c
  change (ε (PresheafOfModules.restrictScalars
      (PresheafOfModules.ringCatHom (R := (TopologicalSpace.Opens.map f.base).op ⋙ X.sheaf.obj)
        f.c)) ≫
    (PresheafOfModules.restrictScalars
      (PresheafOfModules.ringCatHom (R := (TopologicalSpace.Opens.map f.base).op ⋙ X.sheaf.obj)
        f.c)).map
        (ε (PresheafOfModules.pushforward₀OfCommRingCat (TopologicalSpace.Opens.map f.base)
          X.sheaf.obj))).app
      (op V) g = _
  erw [show ε (PresheafOfModules.pushforward₀OfCommRingCat (TopologicalSpace.Opens.map f.base)
    X.sheaf.obj)
      = 𝟙 _ from rfl, CategoryTheory.Functor.map_id, Category.comp_id]
  erw [ModuleCat.restrictScalars_η]
  rfl

lemma

pb₀_η_app_pb₀Section

L389 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections.pb₀_η_app_pb₀Section

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
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
namespace PullbackTensorSections
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
local instance : (PresheafOfModules.pushforward.{u}
    (F := TopologicalSpace.Opens.map f.base) f.toRingCatSheafHom.hom).IsRightAdjoint :=
  (PresheafOfModules.PullbackMonoidal.adj (TopologicalSpace.Opens.map f.base)
    (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c).isRightAdjoint
local instance : (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Modules.pullbackPushforwardAdjunction f).isRightAdjoint
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
local instance : (pf f).LaxMonoidal :=
  PresheafOfModules.pushforward_laxMonoidal
    (F := TopologicalSpace.Opens.map f.base) (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c

Lean source · full declaration

lemma pb₀_η_app_pb₀Section (V : Y.Opens) (g : (𝟙_ Y.PresheafOfModules).obj (op V)) :
    (η (pullback₀ f)).app (op (f ⁻¹ᵁ V)) (pb₀Section f (𝟙_ Y.PresheafOfModules) V g)
      = (f.app V (show Γ(Y, V) from g) : (𝟙_ X.PresheafOfModules).obj (op (f ⁻¹ᵁ V))) := by
  have h : η (pullback₀ f) = ((adj₀ f).homEquiv _ _).symm (ε (pf f)) :=
    Adjunction.leftAdjointOplaxMonoidal_η (adj₀ f)
  rw [h]
  erw [homEquiv_symm_app_pb₀Section f (ε (pf f)) V g]
  exact pf_ε_app f V g

lemma

pb₀_ε_app

L398 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections.pb₀_ε_app

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
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
namespace PullbackTensorSections
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
local instance : (PresheafOfModules.pushforward.{u}
    (F := TopologicalSpace.Opens.map f.base) f.toRingCatSheafHom.hom).IsRightAdjoint :=
  (PresheafOfModules.PullbackMonoidal.adj (TopologicalSpace.Opens.map f.base)
    (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c).isRightAdjoint
local instance : (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Modules.pullbackPushforwardAdjunction f).isRightAdjoint
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
local instance : (pf f).LaxMonoidal :=
  PresheafOfModules.pushforward_laxMonoidal
    (F := TopologicalSpace.Opens.map f.base) (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c

Lean source · full declaration

lemma pb₀_ε_app (V : Y.Opens) (g : (𝟙_ Y.PresheafOfModules).obj (op V)) :
    (ε (pullback₀ f)).app (op (f ⁻¹ᵁ V)) (f.app V (show Γ(Y, V) from g) : (𝟙_
      X.PresheafOfModules).obj (op (f ⁻¹ᵁ V)))
      = pb₀Section f (𝟙_ Y.PresheafOfModules) V g := by
  have h1 := pb₀_η_app_pb₀Section f V g
  have h2 := congr($(Functor.Monoidal.η_ε (pullback₀ f)).app (op (f ⁻¹ᵁ V))
    (pb₀Section f (𝟙_ Y.PresheafOfModules) V g))
  change (ε (pullback₀ f)).app (op (f ⁻¹ᵁ V))
      ((η (pullback₀ f)).app (op (f ⁻¹ᵁ V)) (pb₀Section f (𝟙_ Y.PresheafOfModules) V g))
    = pb₀Section f (𝟙_ Y.PresheafOfModules) V g at h2
  rw [h1] at h2
  exact h2

lemma

sheafify_ε_app

L411 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections.sheafify_ε_app

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
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
namespace PullbackTensorSections
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
local instance : (PresheafOfModules.pushforward.{u}
    (F := TopologicalSpace.Opens.map f.base) f.toRingCatSheafHom.hom).IsRightAdjoint :=
  (PresheafOfModules.PullbackMonoidal.adj (TopologicalSpace.Opens.map f.base)
    (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c).isRightAdjoint
local instance : (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Modules.pullbackPushforwardAdjunction f).isRightAdjoint
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
local instance : (pf f).LaxMonoidal :=
  PresheafOfModules.pushforward_laxMonoidal
    (F := TopologicalSpace.Opens.map f.base) (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c

Lean source · statement

lemma sheafify_ε_app {Z : Scheme.{u}} (W : Z.Opens) (c : Γ(𝟙_ Z.Modules, W)) :
    Scheme.Modules.Hom.app (ε (Modules.sheafify Z)) W c = shUnit (𝟙_ Z.PresheafOfModules) W c

lemma

pullback_ε_app_unitSection

L425 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections.pullback_ε_app_unitSection

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
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
namespace PullbackTensorSections
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
local instance : (PresheafOfModules.pushforward.{u}
    (F := TopologicalSpace.Opens.map f.base) f.toRingCatSheafHom.hom).IsRightAdjoint :=
  (PresheafOfModules.PullbackMonoidal.adj (TopologicalSpace.Opens.map f.base)
    (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c).isRightAdjoint
local instance : (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Modules.pullbackPushforwardAdjunction f).isRightAdjoint
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
local instance : (pf f).LaxMonoidal :=
  PresheafOfModules.pushforward_laxMonoidal
    (F := TopologicalSpace.Opens.map f.base) (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c

Lean source · statement

lemma pullback_ε_app_unitSection (V : Y.Opens) :
    Scheme.Modules.Hom.app (ε (Modules.pullback f)) (f ⁻¹ᵁ V) (Modules.unitSection (f ⁻¹ᵁ V))
      = pullbackLocalSection f (Modules.unitSection V)

theorem

pullbackTensorUnitObjIso_hom_app_pullbackLocalSection_unitSection

L462 ↗

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
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
namespace PullbackTensorSections
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
local instance : (PresheafOfModules.pushforward.{u}
    (F := TopologicalSpace.Opens.map f.base) f.toRingCatSheafHom.hom).IsRightAdjoint :=
  (PresheafOfModules.PullbackMonoidal.adj (TopologicalSpace.Opens.map f.base)
    (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c).isRightAdjoint
local instance : (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Modules.pullbackPushforwardAdjunction f).isRightAdjoint
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
local instance : (pf f).LaxMonoidal :=
  PresheafOfModules.pushforward_laxMonoidal
    (F := TopologicalSpace.Opens.map f.base) (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c

Lean source · statement

theorem pullbackTensorUnitObjIso_hom_app_pullbackLocalSection_unitSection (V : Y.Opens) :
    (pullbackTensorUnitObjIso f).hom.app (f ⁻¹ᵁ V) (pullbackLocalSection f (Modules.unitSection V))
      = Modules.unitSection (f ⁻¹ᵁ V)

theorem

pullbackTensorUnitObjIso_hom_app_pullbackLocalSection'

L472 ↗

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
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
namespace PullbackTensorSections
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
local instance : (PresheafOfModules.pushforward.{u}
    (F := TopologicalSpace.Opens.map f.base) f.toRingCatSheafHom.hom).IsRightAdjoint :=
  (PresheafOfModules.PullbackMonoidal.adj (TopologicalSpace.Opens.map f.base)
    (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c).isRightAdjoint
local instance : (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Modules.pullbackPushforwardAdjunction f).isRightAdjoint
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
open _root_.AlgebraicGeometry.Scheme.Modules.PullbackTensorSections
local instance : (pf f).LaxMonoidal :=
  PresheafOfModules.pushforward_laxMonoidal
    (F := TopologicalSpace.Opens.map f.base) (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c

Lean source · full declaration

theorem pullbackTensorUnitObjIso_hom_app_pullbackLocalSection' (V : Y.Opens) (g : Γ(𝟙_
    Y.Modules, V)) :
    ((pullbackTensorUnitObjIso f).hom.app (f ⁻¹ᵁ V)) (pullbackLocalSection f g) =
      (show Γ(𝟙_ X.Modules, f ⁻¹ᵁ V) from f.app V (show Γ(Y, V) from g)) := by
  have hg : (show Γ(Y, V) from g) • Modules.unitSection V = g := by
    change (show Γ(Y, V) from g) * 1 = (show Γ(Y, V) from g)
    exact mul_one _
  have key : ((pullbackTensorUnitObjIso f).hom.app (f ⁻¹ᵁ V))
      (pullbackLocalSection f ((show Γ(Y, V) from g) • Modules.unitSection V)) =
        (show Γ(𝟙_ X.Modules, f ⁻¹ᵁ V) from f.app V (show Γ(Y, V) from g)) := by
    rw [pullbackLocalSection_smul, Scheme.Modules.Hom.app_smul,
      pullbackTensorUnitObjIso_hom_app_pullbackLocalSection_unitSection]
    change f.app V (show Γ(Y, V) from g) * 1 = _
    rw [mul_one]
  rw [hg] at key
  exact key

theorem

pullbackTensorObjIso_hom_app_pullbackLocalSection_tensorSections

L506 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict.pullbackTensorObjIso_hom_app_pullbackLocalSection_tensorSections

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31Restrict
variable {W X Y Z : Scheme.{u}}
with_weak_namespace _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
with_weak_namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
with_weak_namespace AlgebraicGeometry.Scheme
open Modules in
with_weak_namespace _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
with_weak_namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict

Lean source · statement

theorem pullbackTensorObjIso_hom_app_pullbackLocalSection_tensorSections (f : X ⟶ Y) (L
    M : Y.Modules)
    (V : Y.Opens) (s : Γ(L, V)) (t : Γ(M, V)) :
    ((pullbackTensorObjIso f L M).hom.app (f ⁻¹ᵁ V)) (pullbackLocalSection f (tensorSections s t))
      = tensorSections (pullbackLocalSection f s) (pullbackLocalSection f t)

theorem

pullbackTensorUnitObjIso_hom_app_pullbackLocalSection

L519 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict.pullbackTensorUnitObjIso_hom_app_pullbackLocalSection

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31Restrict
variable {W X Y Z : Scheme.{u}}
with_weak_namespace _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
with_weak_namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
with_weak_namespace AlgebraicGeometry.Scheme
open Modules in
with_weak_namespace _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
with_weak_namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict

Lean source · statement

theorem pullbackTensorUnitObjIso_hom_app_pullbackLocalSection (f : X ⟶ Y) (V : Y.Opens) (g :
    Γ(𝟙_ Y.Modules, V)) :
    ((pullbackTensorUnitObjIso f).hom.app (f ⁻¹ᵁ V)) (pullbackLocalSection f g)
      = (f.app V (g : Γ(Y, V)) : Γ(𝟙_ X.Modules, f ⁻¹ᵁ V))

theorem

projectionMorphism_app_tensorSections

L526 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict.projectionMorphism_app_tensorSections

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31Restrict
variable {W X Y Z : Scheme.{u}}

Lean source · full declaration

theorem projectionMorphism_app_tensorSections (i : Z ⟶ X) (F : X.Modules) (V : X.Opens)
    (a : Γ((Scheme.Modules.pushforward i).obj (𝟙_ Z.Modules), V)) (s : Γ(F, V)) :
    (projectionMorphism i F).app V (tensorSections a s)
      = (((show Γ(Z, i ⁻¹ᵁ V) from a) • pullbackLocalSection i s : Γ((Scheme.Modules.pullback
        i).obj F, i ⁻¹ᵁ V))
          : Γ((Scheme.Modules.pushforward i).obj ((Scheme.Modules.pullback i).obj F), V)) := by
  rw [projectionMorphism_def, Adjunction.homEquiv_unit]
  change (projectionMorphismMate i F).app (i ⁻¹ᵁ V) (pullbackLocalSection i (tensorSections a
    s)) = _
  rw [projectionMorphismMate_def]
  change (λ_ ((Scheme.Modules.pullback i).obj F)).hom.app _
      ((((Scheme.Modules.pullbackPushforwardAdjunction i).counit.app (𝟙_ Z.Modules)) ▷
          (Scheme.Modules.pullback i).obj F).app _
        ((Functor.Monoidal.μIso (Scheme.Modules.pullback i)
            ((Scheme.Modules.pushforward i).obj (𝟙_ Z.Modules)) F).inv.app _
          (pullbackLocalSection i (tensorSections a s)))) = _
  have hB1 : (Functor.Monoidal.μIso (Scheme.Modules.pullback i)
        ((Scheme.Modules.pushforward i).obj (𝟙_ Z.Modules)) F).inv.app (i ⁻¹ᵁ V)
        (pullbackLocalSection i (tensorSections a s))
      = tensorSections (pullbackLocalSection i a) (pullbackLocalSection i s) :=
    pullbackTensorObjIso_hom_app_pullbackLocalSection_tensorSections i _ F V a s
  rw [hB1, whiskerRight_app_tensorSections, counit_app_pullbackLocalSection]
  exact leftUnitor_hom_app_tensorSections (X := Z)
    (N := (Scheme.Modules.pullback i).obj F) (U := i ⁻¹ᵁ V)
    (show Γ(Z, i ⁻¹ᵁ V) from a) (pullbackLocalSection i s)

theorem

app_naturality

L552 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict.app_naturality

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31Restrict
variable {W X Y Z : Scheme.{u}}

Lean source · statement

theorem app_naturality {M N : X.Modules} (φ : M ⟶ N) {U V : X.Opens} (k : V ⟶ U) (m : Γ(M, U)) :
    φ.app V (M.presheaf.map k.op m) = N.presheaf.map k.op (φ.app U m)

theorem

pullbackComp_hom_app_app_pullbackLocalSection

L556 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict.pullbackComp_hom_app_app_pullbackLocalSection

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31Restrict
variable {W X Y Z : Scheme.{u}}

Lean source · statement

theorem pullbackComp_hom_app_app_pullbackLocalSection (f : W ⟶ X) (g : X ⟶ Y) (L : Y.Modules) (V
    : Y.Opens)
    (s : Γ(L, V)) :
    (((pullbackComp f g).hom.app L).app (f ⁻¹ᵁ g ⁻¹ᵁ V)) (pullbackLocalSection f
      (pullbackLocalSection g s))
      = pullbackLocalSection (f ≫ g) s

theorem

pullbackCongr_hom_app_app_pullbackLocalSection

L570 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict.pullbackCongr_hom_app_app_pullbackLocalSection

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31Restrict
variable {W X Y Z : Scheme.{u}}

Lean source · full declaration

theorem pullbackCongr_hom_app_app_pullbackLocalSection {f g : X ⟶ Y} (e : f = g) (L : Y.Modules)
    (V : Y.Opens)
    (s : Γ(L, V)) :
    (((pullbackCongr e).hom.app L).app (f ⁻¹ᵁ V)) (pullbackLocalSection f s)
      = ((Scheme.Modules.pullback g).obj L).presheaf.map (eqToHom (by rw [e])).op
        (pullbackLocalSection g s) := by
  subst e
  simp [pullbackCongr]

theorem

sq

L582 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict.sq

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31Restrict
variable {W X Y Z : Scheme.{u}}
section main
variable (i : Z ⟶ X) (F : X.Modules) (U : X.Opens)

Lean source · statement

theorem sq : (i ⁻¹ᵁ U).ι ≫ i = (i ∣_ U) ≫ U.ι

theorem

preimage_eq

L584 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict.preimage_eq

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31Restrict
variable {W X Y Z : Scheme.{u}}
section main
variable (i : Z ⟶ X) (F : X.Modules) (U : X.Opens)

Lean source · statement

theorem preimage_eq (V : X.Opens) : (i ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ V = (i ⁻¹ᵁ U).ι ⁻¹ᵁ i ⁻¹ᵁ V

theorem

isIso_bc

L587 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict.isIso_bc

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31Restrict
variable {W X Y Z : Scheme.{u}}
section main
variable (i : Z ⟶ X) (F : X.Modules) (U : X.Opens)

Lean source · statement

theorem isIso_bc (N : Z.Modules) : IsIso (baseChangeHom (sq i U) N)

theorem

bc_app_pullbackLocalSection

L590 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict.bc_app_pullbackLocalSection

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31Restrict
variable {W X Y Z : Scheme.{u}}
section main
variable (i : Z ⟶ X) (F : X.Modules) (U : X.Opens)

Lean source · statement

theorem bc_app_pullbackLocalSection (N : Z.Modules) (V : X.Opens)
    (t : Γ((Scheme.Modules.pushforward i).obj N, V)) :
    (baseChangeHom (sq i U) N).app (U.ι ⁻¹ᵁ V) (pullbackLocalSection U.ι t)
      = ((Scheme.Modules.pullback (i ⁻¹ᵁ U).ι).obj N).presheaf.map (eqToHom (preimage_eq i U V)).op
          (pullbackLocalSection (i ⁻¹ᵁ U).ι (t : Γ(N, i ⁻¹ᵁ V)))

def

τIso

L599 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict.τIso

Documentation

The comparison between restricted pullback and pullback after restriction.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31Restrict
variable {W X Y Z : Scheme.{u}}
section main
variable (i : Z ⟶ X) (F : X.Modules) (U : X.Opens)

Lean source · statement

def τIso :
    (Scheme.Modules.pullback (i ∣_ U)).obj ((Scheme.Modules.pullback U.ι).obj F) ≅
      (Scheme.Modules.pullback (i ⁻¹ᵁ U).ι).obj ((Scheme.Modules.pullback i).obj F)

theorem

τIso_hom_app_pullbackLocalSection

L605 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict.τIso_hom_app_pullbackLocalSection

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31Restrict
variable {W X Y Z : Scheme.{u}}
section main
variable (i : Z ⟶ X) (F : X.Modules) (U : X.Opens)

Lean source · statement

theorem τIso_hom_app_pullbackLocalSection (V : X.Opens) (s : Γ(F, V)) :
    (τIso i F U).hom.app _ (pullbackLocalSection (i ∣_ U) (pullbackLocalSection U.ι s))
      = ((Scheme.Modules.pullback (i ⁻¹ᵁ U).ι).obj ((Scheme.Modules.pullback i).obj F)).presheaf.map
          (eqToHom (preimage_eq i U V)).op (pullbackLocalSection (i ⁻¹ᵁ U).ι
            (pullbackLocalSection i s))

def

βIso

L631 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict.βIso

Documentation

The comparison isomorphism for restriction of the projection formula source.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31Restrict
variable {W X Y Z : Scheme.{u}}
section main
variable (i : Z ⟶ X) (F : X.Modules) (U : X.Opens)

Lean source · statement

def βIso :
    (Scheme.Modules.pullback U.ι).obj ((Scheme.Modules.pushforward i).obj
      ((Scheme.Modules.pullback i).obj F)) ≅
      (Scheme.Modules.pushforward (i ∣_ U)).obj
        ((Scheme.Modules.pullback (i ∣_ U)).obj ((Scheme.Modules.pullback U.ι).obj F))

def

unitBC

L641 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict.unitBC

Documentation

The base change isomorphism for the pushforward of the unit module.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31Restrict
variable {W X Y Z : Scheme.{u}}
section main
variable (i : Z ⟶ X) (F : X.Modules) (U : X.Opens)

Lean source · statement

def unitBC :
    (Scheme.Modules.pullback U.ι).obj ((Scheme.Modules.pushforward i).obj (𝟙_ Z.Modules)) ≅
      (Scheme.Modules.pushforward (i ∣_ U)).obj (𝟙_ _)

def

αIso

L649 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict.αIso

Documentation

The comparison isomorphism for restriction of the projection formula target.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31Restrict
variable {W X Y Z : Scheme.{u}}
section main
variable (i : Z ⟶ X) (F : X.Modules) (U : X.Opens)

Lean source · statement

def αIso :
    (Scheme.Modules.pullback U.ι).obj ((Scheme.Modules.pushforward i).obj (𝟙_ Z.Modules) ⊗ F) ≅
      (Scheme.Modules.pushforward (i ∣_ U)).obj (𝟙_ _) ⊗ (Scheme.Modules.pullback U.ι).obj F

def

nf

L655 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict.nf

Documentation

The scalar expression for the projection formula after restriction.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31Restrict
variable {W X Y Z : Scheme.{u}}
section main
variable (i : Z ⟶ X) (F : X.Modules) (U : X.Opens)

Lean source · statement

def nf (V : X.Opens) (a : Γ((Scheme.Modules.pushforward i).obj (𝟙_ Z.Modules), V))
    (s : Γ(F, V)) :
    Γ((Scheme.Modules.pullback (i ∣_ U)).obj ((Scheme.Modules.pullback U.ι).obj F), (i ∣_ U) ⁻¹ᵁ
      U.ι ⁻¹ᵁ V)

theorem

key_lhs

L664 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict.key_lhs

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31Restrict
variable {W X Y Z : Scheme.{u}}
section main
variable (i : Z ⟶ X) (F : X.Modules) (U : X.Opens)

Lean source · statement

theorem key_lhs (V : X.Opens) (a : Γ((Scheme.Modules.pushforward i).obj (𝟙_ Z.Modules), V)) (s :
    Γ(F, V)) :
    ((Scheme.Modules.pullback U.ι).map (projectionMorphism i F) ≫ (βIso i F U).hom).app (U.ι ⁻¹ᵁ V)
        (pullbackLocalSection U.ι (tensorSections a s))
      = (nf i F U V a s : Γ((Scheme.Modules.pushforward (i ∣_ U)).obj
          ((Scheme.Modules.pullback (i ∣_ U)).obj ((Scheme.Modules.pullback U.ι).obj F)), U.ι
            ⁻¹ᵁ V))

theorem

key_rhs

L693 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict.key_rhs

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31Restrict
variable {W X Y Z : Scheme.{u}}
section main
variable (i : Z ⟶ X) (F : X.Modules) (U : X.Opens)

Lean source · statement

theorem key_rhs (V : X.Opens) (a : Γ((Scheme.Modules.pushforward i).obj (𝟙_ Z.Modules), V)) (s :
    Γ(F, V)) :
    ((αIso i F U).hom ≫ projectionMorphism (i ∣_ U) ((Scheme.Modules.pullback U.ι).obj F)).app
      (U.ι ⁻¹ᵁ V)
        (pullbackLocalSection U.ι (tensorSections a s))
      = (nf i F U V a s : Γ((Scheme.Modules.pushforward (i ∣_ U)).obj
          ((Scheme.Modules.pullback (i ∣_ U)).obj ((Scheme.Modules.pullback U.ι).obj F)), U.ι
            ⁻¹ᵁ V))

theorem

key

L722 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict.key

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31Restrict
variable {W X Y Z : Scheme.{u}}
section main
variable (i : Z ⟶ X) (F : X.Modules) (U : X.Opens)

Lean source · statement

theorem key :
    (Scheme.Modules.pullback U.ι).map (projectionMorphism i F) ≫ (βIso i F U).hom
      = (αIso i F U).hom ≫ projectionMorphism (i ∣_ U) ((Scheme.Modules.pullback U.ι).obj F)

theorem

main

L738 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff.Ws31Restrict.main

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31Restrict
variable {W X Y Z : Scheme.{u}}
section main
variable (i : Z ⟶ X) (F : X.Modules) (U : X.Opens)

Lean source · statement

theorem main :
    IsIso ((Scheme.Modules.pullback U.ι).map (projectionMorphism i F)) ↔
      IsIso (projectionMorphism (i ∣_ U) ((Scheme.Modules.pullback U.ι).obj F))

theorem

isIso_pullback_map_projectionMorphism_iff

L768 ↗

AlgebraicGeometry.Scheme.Modules.isIso_pullback_map_projectionMorphism_iff

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open _root_.CategoryTheory.Functor.LaxMonoidal
open _root_.CategoryTheory.Functor.OplaxMonoidal
local instance projectionPresheafSectionsModule {Z : Scheme.{u}}
    (P : Z.PresheafOfModules) (U : Z.Opens) :
    Module Γ(Z, U) (P.obj (op U)) := (P.obj (op U)).isModule
noncomputable section
open TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.isIso_pullback_map_projectionMorphism_iff {Z X :
    Scheme.{u}} (i : Z ⟶ X) (F : X.Modules) (U : X.Opens) :
    IsIso ((Scheme.Modules.pullback U.ι).map (Scheme.Modules.projectionMorphism i F)) ↔
      IsIso (Scheme.Modules.projectionMorphism (i ∣_ U) ((Scheme.Modules.pullback U.ι).obj F))

Module documentation

Declarations