Subfunctors

Stream: Is there code for X?

[Rémi Bottinelli]

Hey,
Is the following code covered by something in the library? Thanks!

import category_theory.types
import category_theory.functor
import data.set.function

universes u v w

open category_theory

namespace category_theory.functor


def subfunctor {C : Type u} [category C] (F : C ⥤ Type v)
  (obj : ∀ c, set $ F.obj c)
  (map : ∀ (c d : C) (m : c ⟶ d), set.maps_to (F.map m) (obj c) (obj d)) : C ⥤ Type v :=
{ obj := λ c, subtype (obj c),
  map := λ c d m, set.maps_to.restrict _ _ _ (map c d m),
  map_id' := by {intro, ext, simp only [map_id, set.maps_to.coe_restrict_apply, types_id_apply], },
  map_comp' := by {intros, ext, simp only [map_comp, set.maps_to.coe_restrict_apply, types_comp_apply], },}

lemma subfunctor.ext {C : Type u} [category C] (F : C ⥤ Type v)
  (obj₁ : ∀ c, set $ F.obj c)
  (map₁ : ∀ (c d : C) (m : c ⟶ d), set.maps_to (F.map m) (obj₁ c) (obj₁ d))
  (obj₂ : ∀ c, set $ F.obj c)
  (map₂ : ∀ (c d : C) (m : c ⟶ d), set.maps_to (F.map m) (obj₂ c) (obj₂ d)) :
  (∀ c, obj₁ c = obj₂ c) → F.subfunctor obj₁ map₁ = F.subfunctor obj₂ map₂ :=
begin
  rintro objeq,
  dsimp [subfunctor],
  fapply category_theory.functor.hext,
  dsimp,
  { rintro c, rw objeq c, },
  { rintro c d m,
    dsimp only [set.maps_to.restrict] at ⊢,
    apply function.hfunext, rw objeq,
    rintro a a' aea',
    dsimp only [subtype.map],
    rw subtype.heq_iff_coe_eq at aea' ⊢,
    { simp only [subtype.coe_mk], rw aea', },
    all_goals { rintro, rw (objeq),},},
end

end category_theory.functor

[Adam Topaz]

I don't think we have such subfunctors, but we can speak about natural transformations which are monomorphisms, and that offers a more flexible notion of "subfunctor" as it can be used not just with functors taking values in Type*.

[Adam Topaz]

The mathlib approach to such constructions would go via the following definition of "bundled subfunctors":

import category_theory.types
import category_theory.functor
import data.set.function

universes u

namespace category_theory

structure subfunctor {C : Type*} [category C] (F : C ⥤ Type u) :=
(carrier : Π X : C, set (F.obj X))
(map_mem : ∀ (X Y : C) (f : X ⟶ Y) (x : F.obj X), x ∈ carrier X → F.map f x ∈ carrier Y)

def subfunctor.to_functor {C : Type*} [category C] {F : C ⥤ Type u} (G : subfunctor F) : C ⥤ Type u :=
{ obj := λ X, G.carrier X,
  map := λ X Y f t, ⟨F.map f t, G.map_mem _ _ _ _ t.2⟩ }

def subfunctor.incl {C : Type*} [category C] {F : C ⥤ Type u} (G : subfunctor F) :
  G.to_functor ⟶ F :=
{ app := λ X (t : G.carrier X), (t : F.obj X) }

--etc...

end category_theory

[Andrew Yang]

We have docs#category_theory.grothendieck_topology.subpresheaf, which is basically the same thing but defined on the opposite category. It might be worthy to generalize it into subfunctors if you need them.

[Adam Topaz]

One should probably generalize and use subobjects

import category_theory.types
import category_theory.functor
import category_theory.abelian.subobject
import data.set.function

universes u

namespace category_theory

structure subfunctor {C D : Type*} [category C] [category D] (F : C ⥤ D) :=
(carrier : Π X : C, subobject (F.obj X))
(map_mem : ∀ (X Y : C) (f : X ⟶ Y), ∃ g, (carrier X).arrow ≫ F.map f = g ≫ (carrier Y).arrow)

noncomputable theory

def subfunctor.map_carrier {C D : Type*} [category C] [category D]  {F : C ⥤ D} (G : subfunctor F) {X Y : C} (f : X ⟶ Y) :
  (G.carrier X : D) ⟶ G.carrier Y :=
(G.map_mem _ _ f).some

@[simp, reassoc]
lemma subfunctor.map_carrier_spec {C D : Type*} [category C] [category D]  {F : C ⥤ D} (G : subfunctor F) {X Y : C} (f : X ⟶ Y) :
  G.map_carrier f ≫ (G.carrier Y).arrow = (G.carrier X).arrow ≫ F.map f :=
(G.map_mem _ _ f).some_spec.symm

lemma subfunctor.map_carrier_unique {C D : Type*} [category C] [category D]  {F : C ⥤ D} (G : subfunctor F) {X Y : C} (f : X ⟶ Y)
  (g : (G.carrier X : D) ⟶ G.carrier Y) (hg : (G.carrier X).arrow ≫ F.map f = g ≫ (G.carrier Y).arrow) :
  g = G.map_carrier f :=
by { ext, simp [hg] }

@[simps]
def subfunctor.to_functor
  {C D : Type*} [category C] [category D]  {F : C ⥤ D} (G : subfunctor F) : C ⥤ D :=
{ obj := λ X, G.carrier X,
  map := λ X Y f, G.map_carrier f }

@[simps]
def subfunctor.incl
  {C D : Type*} [category C] [category D]  {F : C ⥤ D} (G : subfunctor F) : G.to_functor ⟶ F :=
{ app := λ X, (G.carrier X).arrow }

end category_theory

[Rémi Bottinelli]

Thanks! I guess my terminology was a bit off: what I really wanted was the "functor" part of the subfunctor. That is, in my case, I don't really care about the hierarchy of subobjects of F, but only about realizing one such into a functor of its own. By the way, can my code for subfunctor.ext be simplified? I didn't find an easy way to avoid dependent problems.

[Adam Topaz]

On second thought, you could just use subobject (C ⥤ D)

[Andrew Yang]

The proof for subfunctor.ext could be shortened to
by { intro objeq, have : obj₁ = obj₂ := funext objeq, subst this }.

[Rémi Bottinelli]

(and I now feel very dumb)

[Adam Topaz]

But this is an equality of functors, which is very rarely useful.

[Adam Topaz]

This is probably better:

import category_theory.types
import category_theory.functor
import data.set.function

universes u v w

open category_theory

namespace category_theory.functor

@[simps]
def subfunctor {C : Type u} [category C] (F : C ⥤ Type v)
  (obj : ∀ c, set $ F.obj c)
  (map : ∀ (c d : C) (m : c ⟶ d), set.maps_to (F.map m) (obj c) (obj d)) : C ⥤ Type v :=
{ obj := λ c, subtype (obj c),
  map := λ c d m, set.maps_to.restrict _ _ _ (map c d m),
  map_id' := by {intro, ext, simp only [map_id, set.maps_to.coe_restrict_apply, types_id_apply], },
  map_comp' := by {intros, ext, simp only [map_comp, set.maps_to.coe_restrict_apply, types_comp_apply], },}

def subfunctor.ext {C : Type u} [category C] (F : C ⥤ Type v)
  (obj₁ : ∀ c, set $ F.obj c)
  (map₁ : ∀ (c d : C) (m : c ⟶ d), set.maps_to (F.map m) (obj₁ c) (obj₁ d))
  (obj₂ : ∀ c, set $ F.obj c)
  (map₂ : ∀ (c d : C) (m : c ⟶ d), set.maps_to (F.map m) (obj₂ c) (obj₂ d)) :
  (∀ c, obj₁ c = obj₂ c) → (F.subfunctor obj₁ map₁ ≅ F.subfunctor obj₂ map₂) := λ objeq,
nat_iso.of_components
(λ X, equiv.to_iso $ equiv.subtype_equiv_prop $ objeq _ ) (by tidy)

end category_theory.functor

[Rémi Bottinelli]

In what sense is that better? (not a rhetorical question)

[Rémi Bottinelli]

is it because it uses more "categorical" building blocks instead of a blind substitution?

[Adam Topaz]

Yeah essentially. In practice, think about how you would use the equality of functors -- essentially you would have to rewrite it somewhere, which would introduce eq.recs in the goals, and those are hard to work with.

[Adam Topaz]

The benefit of the isomorphism above is that it has good defeq properties, so if you compose with such an iso instead of rewriting with an equality, then by applying ext lemmas sufficiently many times, you should be able to reduce goals to, essentially, ∀ c, obj₁ c = obj₂ c.

[Rémi Bottinelli]

ah, OK, so it's really more than aesthetics questions.