AlgebraicGeometry.Scheme.Modules.exists_pullback_glueOfCocycle_iso
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullback_glueOfCocycle_iso
attribute [-instance]
SheafOfModules.isIso_ihomModelToIhom
pullback_monoidal
isIso_δ
PresheafOfModules.pushforward_laxMonoidal
isIso_η
PresheafOfModules.free_monoidal
PresheafOfModules.restrictScalars_laxMonoidal
isIso_δ_gS
PresheafOfModules.pullback_oplaxMonoidal
instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
PresheafOfModules.pullback_monoidal'
AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
AlgebraicGeometry.Scheme.Modules.pullback_monoidal
AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
SheafOfModules.ihomSectionsEquivFamily_unit
AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply
SheafOfModules.unit_ihomSectionsEquivFamily AlgebraicGeometry.Scheme.Modules.familyOfHom_app
AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
PresheafOfModules.freeεIso_hom_app PresheafOfModules.freeμIso_hom_app
open _root_.CategoryTheory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
universe u
open AlgebraicGeometry.Scheme.Modules inLean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.exists_pullback_glueOfCocycle_iso
{X X' : Scheme.{u}} (g : X' ⟶ X) {ι : Type u} {U : ι → X.Opens} (hU : ⨆ i, U i = ⊤)
(c : Scheme.Modules.UnitCocycle U) :
∃ φ : (Scheme.Modules.pullback g).obj (Scheme.Modules.glueOfCocycle c) ≅
Scheme.Modules.glueOfCocycle (c.comap g),
∀ i, φ.hom.app (g ⁻¹ᵁ U i) (Scheme.Modules.pullbackLocalSection g (Scheme.Modules.glueFrame c
i)) =
Scheme.Modules.glueFrame (c.comap g) i