Theorems · Definition · category theory

CategoryTheory.Subfunctor.obj

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C (Type w)} → CategoryTheory.Subfunctor F → (U : C) → Set (F.obj U)

If G is a subfunctor of F, then the sections of G on U forms a subset of sections of F on U.

Defined in

Mathlib.CategoryTheory.Subfunctor.Basic

Cited by

227 results in Mathlib

Foundations

Depth 12 from the axioms, rests on 54 definitions · uses no axioms

Assumes

CategoryTheory.Category