NYLL
Module

Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
32 declarations indexed from sourceView source ↗

Module documentation

Descent of endomorphisms of the unit module

The fpqc sheaf property of functions gives descent of endomorphisms through pullback.

Imports54
  • Nyll.AlgebraicCurves.Geometry.Picard.Functor
  • Mathlib.Algebra.Category.ModuleCat.Sheaf
  • Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
  • Mathlib.Algebra.Category.Ring.Basic
  • Mathlib.Algebra.Group.Hom.Defs
  • Mathlib.Algebra.MvPolynomial.Basic
  • Mathlib.AlgebraicGeometry.AffineSpace
  • Mathlib.AlgebraicGeometry.Modules.Presheaf
  • Mathlib.AlgebraicGeometry.Modules.Sheaf
  • Mathlib.AlgebraicGeometry.Morphisms.Flat
  • Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
  • Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
  • Mathlib.AlgebraicGeometry.Scheme
  • Mathlib.AlgebraicGeometry.Sites.Fpqc
  • Mathlib.CategoryTheory.Adjunction.Basic
  • Mathlib.CategoryTheory.Adjunction.Mates
  • Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
  • Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  • Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
  • Mathlib.CategoryTheory.Category.Basic
  • Mathlib.CategoryTheory.Category.Cat
  • Mathlib.CategoryTheory.Category.Preorder
  • Mathlib.CategoryTheory.Comma.Over.Basic
  • Mathlib.CategoryTheory.ConcreteCategory.Basic
  • Mathlib.CategoryTheory.ConcreteCategory.Forget
  • Mathlib.CategoryTheory.EqToHom
  • Mathlib.CategoryTheory.Functor.Basic
  • Mathlib.CategoryTheory.Functor.Category
  • Mathlib.CategoryTheory.Functor.Flat
  • Mathlib.CategoryTheory.HomCongr
  • Mathlib.CategoryTheory.Iso
  • Mathlib.CategoryTheory.NatIso
  • Mathlib.CategoryTheory.NatTrans
  • Mathlib.CategoryTheory.Opposites
  • Mathlib.CategoryTheory.Sites.Canonical
  • Mathlib.CategoryTheory.Sites.Continuous
  • Mathlib.CategoryTheory.Sites.Descent.DescentData
  • Mathlib.CategoryTheory.Sites.Descent.IsPrestack
  • Mathlib.CategoryTheory.Sites.Grothendieck
  • Mathlib.CategoryTheory.Sites.IsSheafFor
  • Mathlib.CategoryTheory.Sites.Over
  • Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
  • Mathlib.CategoryTheory.Sites.Sheaf
  • Mathlib.CategoryTheory.Sites.SheafOfTypes
  • Mathlib.CategoryTheory.Sites.Sieves.Basic
  • Mathlib.CategoryTheory.Sites.Sieves.Presieve
  • Mathlib.CategoryTheory.Types.Basic
  • Mathlib.CategoryTheory.Yoneda
  • Mathlib.Logic.Equiv.Defs
  • Mathlib.Order.BoundedOrder.Basic
  • Mathlib.Tactic.CategoryTheory.Reassoc
  • Mathlib.Tactic.Set
  • Mathlib.Topology.Category.TopCat.Opens
  • Mathlib.Topology.Sheaves.SheafCondition.Sites
Imported by2

Declarations

abbrev

MOD

L102 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.MOD
Documentation

The pseudofunctor of modules used for descent.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
abbrev MOD : Pseudofunctor (LocallyDiscrete Scheme.{u}ᵒᵖ) Cat
instance

pushforwardRightAdjoint

L107 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.pushforwardRightAdjoint
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
Lean source · statement
instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint
abbrev

OO

L116 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.OO
Documentation

The unit module of a scheme.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
abbrev OO (X : Scheme.{u}) : X.Modules
abbrev

uu

L119 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.uu
Documentation

The natural unit morphism into the pushforward of the unit module.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
abbrev uu (f : X ⟶ Y) : OO Y ⟶ (Scheme.Modules.pushforward f).obj (OO X)
def

ee

L123 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.ee
Documentation

The pullback of the unit module is the unit module.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
def ee (f : X ⟶ Y) : (Scheme.Modules.pullback f).obj (OO Y) ≅ OO X
lemma

homEquiv_ee_hom

L126 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.homEquiv_ee_hom
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
lemma homEquiv_ee_hom (f : X ⟶ Y) :
    (Scheme.Modules.pullbackPushforwardAdjunction f).homEquiv _ _ (ee f).hom = uu f
lemma

homEquiv_conjugate

L131 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.homEquiv_conjugate
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
lemma homEquiv_conjugate {C D : Type*} [Category C] [Category D] {L₁ L₂ : C ⥤ D} {R₁ R₂ : D ⥤ C}
    (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (α : L₂ ⟶ L₁) {c : C} {d : D} (f : L₁.obj c ⟶ d) :
    adj₂.homEquiv c d (α.app c ≫ f) = adj₁.homEquiv c d f ≫ (conjugateEquiv adj₁ adj₂ α).app d
lemma

conjugateEquiv_pullbackComp_hom

L141 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.conjugateEquiv_pullbackComp_hom
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
lemma conjugateEquiv_pullbackComp_hom (f : X ⟶ Y) (g : Y ⟶ Z) :
    conjugateEquiv (Scheme.Modules.pullbackPushforwardAdjunction (f ≫ g))
      ((Scheme.Modules.pullbackPushforwardAdjunction g).comp
        (Scheme.Modules.pullbackPushforwardAdjunction f))
      (Scheme.Modules.pullbackComp f g).hom = (Scheme.Modules.pushforwardComp f g).inv
lemma

uu_comp

L154 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.uu_comp
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
lemma uu_comp (f : X ⟶ Y) (g : Y ⟶ Z) :
    uu (f ≫ g) ≫ (Scheme.Modules.pushforwardComp f g).inv.app (OO X) =
      uu g ≫ (Scheme.Modules.pushforward g).map (uu f)
lemma

pullbackComp_hom_app_ee

L163 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.pullbackComp_hom_app_ee
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
lemma pullbackComp_hom_app_ee (f : X ⟶ Y) (g : Y ⟶ Z) :
    (Scheme.Modules.pullbackComp f g).hom.app (OO Z) ≫ (ee (f ≫ g)).hom =
      (Scheme.Modules.pullback f).map (ee g).hom ≫ (ee f).hom
def

evalOne

L187 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.evalOne
Documentation

A unit-module endomorphism evaluated on the global unit section.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
def evalOne (X : Scheme.{u}) (ψ : OO X ⟶ OO X) : Γ(X, ⊤)
lemma

evalOne_eq_app

L190 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.evalOne_eq_app
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
lemma evalOne_eq_app (X : Scheme.{u}) (ψ : OO X ⟶ OO X) :
    evalOne X ψ = (ψ.app ⊤ : Γ(X, ⊤) → Γ(X, ⊤)) (1 : Γ(X, ⊤))
lemma

sections_evalTop_bijective

L193 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.sections_evalTop_bijective
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · full declaration
lemma sections_evalTop_bijective (M : X.Modules) :
    Function.Bijective (fun s : SheafOfModules.sections M => s.val (op ⊤)) := by
  constructor
  · intro s t h
    apply Subtype.ext
    funext U
    have hs := s.property ((homOfLE (le_top : U.unop ≤ ⊤)).op : op ⊤ ⟶ U)
    have ht := t.property ((homOfLE (le_top : U.unop ≤ ⊤)).op : op ⊤ ⟶ U)
    rw [← hs, ← ht]
    exact congr_arg _ h
  · intro a
    refine ⟨⟨fun U => M.val.presheaf.map ((homOfLE (le_top : U.unop ≤ ⊤)).op : op ⊤ ⟶ U) a, ?_⟩, ?_⟩
    · intro U V i
      change M.val.presheaf.map i (M.val.presheaf.map _ a) = M.val.presheaf.map _ a
      rw [← CategoryTheory.comp_apply, ← Functor.map_comp]
      rfl
    · change M.val.presheaf.map _ a = a
      have : ((homOfLE (le_top : (⊤ : X.Opens) ≤ ⊤)).op : op ⊤ ⟶ op ⊤) = 𝟙 _ := Subsingleton.elim _
        _
      rw [this, CategoryTheory.Functor.map_id]
      rfl
lemma

evalOne_bijective

L215 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.evalOne_bijective
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
lemma evalOne_bijective (X : Scheme.{u}) : Function.Bijective (evalOne X)
lemma

uu_app_apply

L218 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.uu_app_apply
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
lemma uu_app_apply (g : X ⟶ Y) (U : Y.Opens) (x : Γ(Y, U)) :
    (Scheme.Modules.Hom.app (uu g) U : Γ(Y, U) → Γ(X, g ⁻¹ᵁ U)) x = g.app U x
lemma

evalOne_conj_pullback

L221 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.evalOne_conj_pullback
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
lemma evalOne_conj_pullback (g : X ⟶ Y) (ψ : OO Y ⟶ OO Y) :
    evalOne X ((ee g).inv ≫ (Scheme.Modules.pullback g).map ψ ≫ (ee g).hom) = g.appTop (evalOne Y
      ψ)
lemma

evalOne_conj_pullHom

L243 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.evalOne_conj_pullHom
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
lemma evalOne_conj_pullHom (p₂ : Y ⟶ Z) (g : X ⟶ Y) (p₁ : X ⟶ Z) (w : g ≫ p₂ = p₁)
    (φ : (Scheme.Modules.pullback p₂).obj (OO Z) ⟶ (Scheme.Modules.pullback p₂).obj (OO Z)) :
    evalOne X ((ee p₁).inv ≫
      (((Scheme.Modules.pullbackCongr w.symm).hom.app _ ≫ (Scheme.Modules.pullbackComp g
        p₂).inv.app _) ≫
        (Scheme.Modules.pullback g).map φ ≫
        ((Scheme.Modules.pullbackComp g p₂).hom.app _ ≫ (Scheme.Modules.pullbackCongr w).hom.app
          _)) ≫
      (ee p₁).hom) = g.appTop (evalOne Y ((ee p₂).inv ≫ φ ≫ (ee p₂).hom))
theorem

modMapComp'_eq

L275 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.modMapComp'_eq
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
theorem modMapComp'_eq {a b d : LocallyDiscrete Scheme.{u}ᵒᵖ} (s : a ⟶ b) (t : b ⟶ d) (M : MOD.obj
  a) :
    (MOD.mapComp' s t (s ≫ t) rfl).hom.toNatTrans.app M = (MOD.mapComp s t).hom.toNatTrans.app M
theorem

modMapComp'_eq_inv

L281 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.modMapComp'_eq_inv
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
theorem modMapComp'_eq_inv {a b d : LocallyDiscrete Scheme.{u}ᵒᵖ} (s : a ⟶ b) (t : b ⟶ d) (M :
  MOD.obj a) :
    (MOD.mapComp' s t (s ≫ t) rfl).inv.toNatTrans.app M = (MOD.mapComp s t).inv.toNatTrans.app M
theorem

modMapComp'_hom_app

L287 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.modMapComp'_hom_app
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · full declaration
theorem modMapComp'_hom_app (f : X ⟶ Y) (g : Y ⟶ Z) (fg : X ⟶ Z) (h : f ≫ g = fg) (L : Z.Modules) :
    (MOD.mapComp' g.op.toLoc f.op.toLoc fg.op.toLoc (by rw [← h]; rfl)).hom.toNatTrans.app L =
    (Scheme.Modules.pullbackCongr h.symm).hom.app L ≫ (Scheme.Modules.pullbackComp f g).inv.app L
      := by
  subst h
  simp only [Scheme.Modules.pullbackCongr, eqToIso_refl, Iso.refl_hom, NatTrans.id_app,
    Category.id_comp]
  exact modMapComp'_eq g.op.toLoc f.op.toLoc L
theorem

modMapComp'_inv_app

L296 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.modMapComp'_inv_app
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · full declaration
theorem modMapComp'_inv_app (f : X ⟶ Y) (g : Y ⟶ Z) (fg : X ⟶ Z) (h : f ≫ g = fg) (L : Z.Modules) :
    (MOD.mapComp' g.op.toLoc f.op.toLoc fg.op.toLoc (by rw [← h]; rfl)).inv.toNatTrans.app L =
    (Scheme.Modules.pullbackComp f g).hom.app L ≫ (Scheme.Modules.pullbackCongr h).hom.app L := by
  subst h
  simp only [Scheme.Modules.pullbackCongr, eqToIso_refl, Iso.refl_hom, NatTrans.id_app,
    Category.comp_id]
  exact modMapComp'_eq_inv g.op.toLoc f.op.toLoc L
abbrev

ΓType

L305 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.ΓType
Documentation

Global sections viewed as a presheaf of types.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
abbrev ΓType : Scheme.{u}ᵒᵖ ⥤ Type u
def

yonedaA1IsoΓType

L308 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.yonedaA1IsoΓType
Documentation

The affine line represents global sections.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
def yonedaA1IsoΓType :
    yoneda.obj (Spec (CommRingCat.of (MvPolynomial PUnit.{u + 1} (ULift.{u} ℤ)))) ≅ ΓType.{u}
lemma

ΓType_isSheaf

L318 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.ΓType_isSheaf
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
lemma ΓType_isSheaf : Presieve.IsSheaf Scheme.fpqcTopology ΓType.{u}
abbrev

ΓOver

L323 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.ΓOver
Documentation

Global sections on schemes over a fixed base.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
abbrev ΓOver (Y : Scheme.{u}) : (Over Y)ᵒᵖ ⥤ Type u
lemma

ΓOver_isSheaf

L325 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.ΓOver_isSheaf
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
lemma ΓOver_isSheaf (Y : Scheme.{u}) : Presieve.IsSheaf (Scheme.fpqcTopology.over Y) (ΓOver Y)
lemma

ΓOver_isSheafFor

L329 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.ΓOver_isSheafFor
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · full declaration
lemma ΓOver_isSheafFor {Y Y' : Scheme.{u}} (q : Y' ⟶ Y) [QuasiCompact q] [Flat q] [Surjective q] :
    Presieve.IsSheafFor (ΓOver Y) (Presieve.ofArrows (X := Over.mk (𝟙 Y)) (fun _ : Unit => Over.mk
      q)
      (fun _ : Unit => Over.homMk q)) := by
  refine (ΓOver_isSheaf Y).isSheafFor _ ?_
  rw [GrothendieckTopology.mem_over_iff]
  refine Scheme.fpqcTopology.superset_covering ?_
    (Precoverage.generate_mem_toGrothendieck (Scheme.Hom.singleton_mem_fpqcPrecoverage q))
  rw [Sieve.generate_le_iff]
  rintro Z g ⟨⟩
  rw [Sieve.overEquiv_iff]
  exact ⟨Over.mk q, Over.homMk (𝟙 _) (by simp), Over.homMk q, ⟨()⟩, by ext; simp⟩
def

theta

L343 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.theta
Documentation

The section corresponding to an endomorphism of a pulled-back unit module.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
def theta {Y : Scheme.{u}} (T : Over Y)
    (φ : (Scheme.Modules.pullback T.hom).obj (OO Y) ⟶ (Scheme.Modules.pullback T.hom).obj (OO Y)) :
    Γ(T.left, ⊤)
lemma

theta_bijective

L348 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.theta_bijective
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
lemma theta_bijective {Y : Scheme.{u}} (T : Over Y) : Function.Bijective (theta T)
lemma

evalOne_conj_pullHom'

L351 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.evalOne_conj_pullHom'
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
lemma evalOne_conj_pullHom' {Y₀ X₁ X₂ : Scheme.{u}} (p₂ : X₂ ⟶ Y₀) (g : X₁ ⟶ X₂) (p₁ : X₁ ⟶ Y₀)
    (w : g ≫ p₂ = p₁)
    (φ : (Scheme.Modules.pullback p₂).obj (OO Y₀) ⟶ (Scheme.Modules.pullback p₂).obj (OO Y₀)) :
    evalOne X₁ ((ee p₁).inv ≫
      (Pseudofunctor.LocallyDiscreteOpToCat.pullHom (F := MOD) (M₁ := OO Y₀) (M₂ := OO Y₀)
        (f₁ := p₂) (f₂ := p₂) φ g p₁ p₁ w w) ≫ (ee p₁).hom) =
      g.appTop (evalOne X₂ ((ee p₂).inv ≫ φ ≫ (ee p₂).hom))
def

thetaIso

L364 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.HomDescO.thetaIso
Documentation

Endomorphisms of pulled-back unit modules are global sections.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace HomDescO
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}}
private local instance pushforwardRightAdjoint (f : X ⟶ Y) :
    (SheafOfModules.pushforward.{u} f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
def thetaIso (Y : Scheme.{u}) : MOD.presheafHom (OO Y) (OO Y) ≅ ΓOver Y
theorem

toDescentData_map_bijective_unit_of_flat_of_surjective

L375 ↗
AlgebraicGeometry.Scheme.Modules.toDescentData_map_bijective_unit_of_flat_of_surjective
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Bicategory
open _root_.TopologicalSpace
noncomputable section
open AlgebraicGeometry.Scheme.Modules.HomDescO in
Lean source · full declaration
theorem
  _root_.AlgebraicGeometry.Scheme.Modules.toDescentData_map_bijective_unit_of_flat_of_surjective
    {Y Y' : Scheme.{u}} (q : Y' ⟶ Y) [QuasiCompact q] [Flat q] [Surjective q] :
    Function.Bijective
      ((((Scheme.Modules.pseudofunctor.{u}).comp Bicategory.Adj.forget₁).toDescentData
        (fun _ : Unit => q)).map :
          (SheafOfModules.unit Y.ringCatSheaf ⟶ SheafOfModules.unit Y.ringCatSheaf) → _) := by
  exact (Pseudofunctor.bijective_toDescentData_map_iff
    (F := MOD) (f := fun _ : Unit => q) (OO Y) (OO Y)).2
      (Presieve.isSheafFor_iso (thetaIso Y).symm (ΓOver_isSheafFor q))

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