Subfunctors

Stream: new members

[VayusElytra]

I have the following code to define subfunctors into ModuleCat:

open CategoryTheory

--Persistence modules over some (small) category C.
abbrev FunctCat (C : Type*) [Category C] (K : Type*) [DivisionRing K]
   := (C ⥤ ModuleCat K)

structure Subfunctor (R : Type) [DivisionRing R] (C : Type) [Category C]
  (F : FunctCat C R) where
  BaseFunctor : FunctCat C R
  sub_obj (X : C) : --I want to express that BaseFunctor.obj(X) is a subset
  -- of F.obj X

How can I express the condition that BaseFunctor.obj(X) is a submodule of F.obj X? I had a look at the submodule structure, but I can't do something like sub_obj (X : C) := (BaseFunctor.obj X : Submodule R (F.obj X)) since that causes a type mismatch. How can I work around this?

[Kevin Buzzard]

A submodule is a term, not a type. Just write down an injective R-module hom instead?

[Adam Topaz]

See also CategoryTheory.NatTrans.mono_iff_mono_app

[Joël Riou]

You may use a variant of docs#CategoryTheory.GrothendieckTopology.Subpresheaf, or as Adam implies, you may consider monomorphisms in the functor category.

[VayusElytra]

Thank you all. Is something like this what you had in mind?

structure Subfunctor (R : Type) [DivisionRing R] (C : Type) [Category C]
  (F : FunctCat C R) where
  baseFunctor : FunctCat C R
  targetFunctor := F
  injection (X : C) : (baseFunctor.obj X →ₗ[R] F.obj X)
  inj_cond (X : C) : Function.Injective (injection X)
  restriction (f : X ⟶ Y) : ∀ (x : baseFunctor.obj X),
    ((baseFunctor.map f) ≫ (injection Y)) x = ((asHom (injection X)) ≫ (F.map f)) x
    --careful with asHom! This breaks if you use asHom injection Y instead.

[Joël Riou]

No, what I intended was a variation of

structure Subpresheaf (F : Cᵒᵖ ⥤ Type w) where
  /-- If `G` is a sub-presheaf of `F`, then the sections of `G` on `U` forms a subset of sections of
    `F` on `U`. -/
  obj : ∀ U, Set (F.obj U)
  /-- If `G` is a sub-presheaf of `F` and `i : U ⟶ V`, then for each `G`-sections on `U` `x`,
    `F i x` is in `F(V)`. -/
  map : ∀ {U V : Cᵒᵖ} (i : U ⟶ V), obj U ⊆ F.map i ⁻¹' obj V

Instead of Set (which in mathlib means "subset of"), it would be Submodule.

Alternatives would be MonoOver F which is the category of monomorphisms with target object F, or the variant Subobject F.