SheafOfModules.Submodule.imposeOn
Impose membership in N only after restriction to objects mapping to U. On the site of opens this is the largest submodule agreeing with N on U.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe v v₁ u₁ u
open CategoryTheory Opposite
namespace SheafOfModules.Submodule
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
{R : Sheaf J RingCat.{u}} {M : SheafOfModules.{v} R}Lean source · full declaration
def imposeOn (N : M.Submodule) (U : C) : M.Submodule where
toSubmodule :=
{ obj X :=
{ carrier := {s | ∀ (V : C) (i : V ⟶ X.unop) (_j : V ⟶ U),
M.val.map i.op s ∈ N.toSubmodule.obj (op V)}
zero_mem' := by
intro V i j
rw [map_zero]
exact (N.toSubmodule.obj (op V)).zero_mem
add_mem' := by
intro s t hs ht V i j
rw [map_add]
exact (N.toSubmodule.obj (op V)).add_mem (hs V i j) (ht V i j)
smul_mem' := by
intro r s hs V i j
rw [M.val.map_smul]
exact (N.toSubmodule.obj (op V)).smul_mem _ (hs V i j) }
map := by
intro X Y f s hs V i j
change M.val.map i.op (M.val.map f s) ∈ N.toSubmodule.obj (op V)
have h := hs V (i ≫ f.unop) j
rw [op_comp, M.val.map_comp_apply] at h
exact h }
isSheaf := by
intro X s hs V i j
apply N.isSheaf (X := op V) (M.val.map i.op s)
apply J.superset_covering _ (J.pullback_stable i hs)
intro W f hf
change ∀ (Z : C) (k : Z ⟶ W) (l : Z ⟶ U),
M.val.map k.op (M.val.map (f ≫ i).op s) ∈ N.toSubmodule.obj (op Z) at hf
have h := hf W (𝟙 W) (f ≫ j)
change M.val.map f.op (M.val.map i.op s) ∈ N.toSubmodule.obj (op W)
rw [op_id, ← M.val.map_comp_apply, op_comp,
Category.comp_id (i.op ≫ f.op), M.val.map_comp_apply] at h
exact h