pullback is over

Stream: Is there code for X?

[Kenny Lau]

import Mathlib

universe v u

namespace CategoryTheory.Limits

noncomputable instance pullback_over {C : Type u} [Category.{v} C] [HasPullbacks C]
      {X₁ X₂ Y S : C} (f₁ : X₁ ⟶ Y) (f₂ : X₂ ⟶ Y)
      [OverClass X₁ S] [OverClass X₂ S] [OverClass Y S] [HomIsOver f₁ S] [HomIsOver f₂ S] :
    OverClass (pullback f₁ f₂) S :=
  ⟨pullback.fst _ _ ≫ X₁ ↘ S⟩

variable {C : Type u} [Category.{v} C] [HasPullbacks C] {X₁ X₂ Y S : C} (f₁ : X₁ ⟶ Y) (f₂ : X₂ ⟶ Y)
  [OverClass X₁ S] [OverClass X₂ S] [OverClass Y S] [HomIsOver f₁ S] [HomIsOver f₂ S]

theorem pullback_over_fst : pullback f₁ f₂ ↘ S = pullback.fst _ _ ≫ X₁ ↘ S := rfl

theorem pullback_over_snd : pullback f₁ f₂ ↘ S = pullback.snd _ _ ≫ X₂ ↘ S := by
  rw [pullback_over_fst, ← comp_over f₁, pullback.condition_assoc, comp_over]

end CategoryTheory.Limits

[Kenny Lau]

image.png

[Kenny Lau]

if X_1, X_2, and Y are objects over S, and maps X_1 -> Y and X_2 -> Y are over S, then the pullback is also over S

[Robin Carlier]

I couldn’t get type class inference to work properly on this one, so we might have to record it manually, but perhaps we want the proof to invoke the more general

import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
import Mathlib.CategoryTheory.IsConnected
import Mathlib.CategoryTheory.Comma.Over.OverClass

universe v u

namespace CategoryTheory.Limits

noncomputable instance limit_connected_over
    {C : Type u} [Category.{v} C]
    {J : Type*} [Category J] [IsConnected J]
    (F : J ⥤ C) [HasLimit F] (S : C)
    [∀ (j : J), OverClass (F.obj j) S] [∀ ⦃j j' : J⦄ (f : j ⟶ j'), HomIsOver (F.map f) S] :
    OverClass (limit F) S :=
  letI : Inhabited J := ⟨Nonempty.some (inferInstance)⟩
  ⟨limit.π F default ≫ F.obj (default) ↘ S⟩

variable {C : Type u} [Category.{v} C]
    {J : Type*} [Category J] [IsConnected J]
    (F : J ⥤ C) [HasLimit F]
    (S : C)
    [∀ (j : J), OverClass (F.obj j) S] [∀ ⦃j j' : J⦄ (f : j ⟶ j'), HomIsOver (F.map f) S]

theorem π_limit_connected_over (j : J) :
    (limit F) ↘ S = limit.π F j ≫ F.obj j ↘ S := by
  let φ : J → (limit F ⟶ S)  := fun j' => limit.π F j' ≫ F.obj j' ↘ S
  apply constant_of_preserves_morphisms (F := φ)
  intro j₁ j₂ f
  simpa [-comp_over] using limit.π F j₁ ≫= comp_over (F.map f) S|>.symm

end CategoryTheory.Limits

(names is my example are bad)