Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Modules.restrictAppIso_inv_map_assoc

∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (M : Y.Modules)
  {U V : X.Opens} (hUV : Opposite.op V ⟶ Opposite.op U) {Z : Ab} (h : (M.restrict f).presheaf.obj (Opposite.op U) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M V).inv
      (CategoryTheory.CategoryStruct.comp ((M.restrict f).presheaf.map hUV) h) =
    CategoryTheory.CategoryStruct.comp (M.presheaf.map (CategoryTheory.homOfLE ⋯).op)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).inv h)

Defined in

Mathlib.AlgebraicGeometry.Modules.Sheaf

Cited by

0 results in Mathlib

Foundations

Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AlgebraicGeometry.IsOpenImmersion