Theorems · Definition · category theory

CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      ⦃X₁ X₂ : C⦄ →
        ⦃M₁ : ↑(F.obj { as := Opposite.op X₁ })⦄ →
          ⦃M₂ : ↑(F.obj { as := Opposite.op X₂ })⦄ →
            ⦃Y : C⦄ →
              ⦃f₁ : Y ⟶ X₁⦄ →
                ⦃f₂ : Y ⟶ X₂⦄ →
                  ((F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂) →
                    ⦃Y' : C⦄ →
                      (g : Y' ⟶ Y) →
                        (gf₁ : Y' ⟶ X₁) →
                          (gf₂ : Y' ⟶ X₂) →
                            autoParam (CategoryTheory.CategoryStruct.comp g f₁ = gf₁)
                                CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom._auto_1 →
                              autoParam (CategoryTheory.CategoryStruct.comp g f₂ = gf₂)
                                  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom._auto_3 →
                                ((F.map gf₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map gf₂.op.toLoc).toFunctor.obj M₂)

Given a pseudofunctor F from LocallyDiscrete Cᵒᵖ to Cat, objects M₁ and M₂ of F over X₁ and X₂, morphisms f₁ : Y ⟶ X₁ and f₂ : Y ⟶ X₂, this is a version of the pullback map (f₁^* M₁ ⟶ f₂^* M₂) → (g^* (f₁^* M₁) ⟶ g^* (f₂^* M₂)) by a morphism g : Y' ⟶ Y, where we actually replace g^* (f₁^* M₁) by gf₁^* M₁ where gf₁ : Y' ⟶ X₁ is a morphism such that g ≫ f₁ = gf₁ (and similarly for M₂).

Defined in

Mathlib.CategoryTheory.Sites.Descent.IsPrestack

Cited by

23 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category