Theorems · Definition · category theory

CategoryTheory.Equalizer.Presieve.secondMap

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) →
      {X : C} →
        (R : CategoryTheory.Presieve X) →
          [inst_1 : R.HasPairwisePullbacks] →
            CategoryTheory.Equalizer.FirstObj P R ⟶ CategoryTheory.Equalizer.Presieve.SecondObj P R

The map pr₁* of the Stacks entry.

Defined in

Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Presieve.HasPairwisePullbacks