Theorems · Definition · category theory

CategoryTheory.Presieve.FamilyOfElements.localPreimage

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {R R' : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      (φ : R ⟶ R') →
        {X : Cᵒᵖ} →
          (r' : R'.obj X) → CategoryTheory.Presieve.FamilyOfElements R (CategoryTheory.Presheaf.imageSieve φ r').arrows

Given a morphism φ : R ⟶ R' of presheaves of types and r' : R'.obj X, this is the family of elements of R defined over the sieve Presheaf.imageSieve φ r' which sends a map in this sieve to an arbitrary choice of a preimage of the restriction of r'.

Defined in

Mathlib.CategoryTheory.Sites.LocallySurjective

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category