Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Modules.smul_restrictAppIso_inv_assoc

∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (M : Y.Modules)
  (U : X.Opens) (r : ↑(Y.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)))) {Z : Ab}
  (h : (M.restrict f).presheaf.obj (Opposite.op U) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.smul r)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).inv h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).inv
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Scheme.Modules.smul
          ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appIso f U).hom) r))
        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