Theorems · Definition · category theory

CategoryTheory.Subfunctor.IsGeneratedBy

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      CategoryTheory.Subfunctor F → {ι : Type w'} → {X : ι → Cᵒᵖ} → ((i : ι) → F.obj (X i)) → Prop

A subpresheaf G : Subfunctor F is generated by sections x i : F.obj (X i) if ⨆ (i : ι), ofSection (x i) = G.

Defined in

Mathlib.CategoryTheory.Subfunctor.Finite

Cited by

11 results in Mathlib

Foundations

Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category