Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_inv_app_app

∀ {X Y : AlgebraicGeometry.Scheme} {U : X.Opens} {f g : X ⟶ Y} (hf : f = g) [inst : AlgebraicGeometry.IsOpenImmersion f]
  [inst_1 : AlgebraicGeometry.IsOpenImmersion g] (M : Y.Modules),
  AlgebraicGeometry.Scheme.Modules.Hom.app ((AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr hf).inv.app M) U =
    M.presheaf.map (CategoryTheory.eqToHom ⋯).op

Defined in

Mathlib.AlgebraicGeometry.Modules.Sheaf

Cited by

0 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsOpenImmersionAlgebraicGeometry.IsOpenImmersion