tilde — Mathlib

Lean4
/-- `M^~` as a sheaf of `𝒪_{Spec R}`-modules
-/
noncomputable def tilde : (Spec <| .of R).Modules
    where
  val :=
    { obj := fun U ↦ ModuleCat.of _ (M.tildeInType.val.obj U)
      map := fun {U V} i ↦
        ofHom (Y :=
          (restrictScalars ((Spec <| .of R).ringCatSheaf.val.map i).hom).obj
            (of ((Spec <| .of R).ringCatSheaf.val.obj V) (M.tildeInType.val.obj V)))
          { toFun := M.tildeInType.val.map i
            map_smul' := by intros; rfl
            map_add' := by intros; rfl } }
  isSheaf := (TopCat.Presheaf.isSheaf_iff_isSheaf_comp (forget AddCommGrpCat) _).2 M.tildeInType.2
Похожие утверждения