Geb.Mathlib.CategoryTheory.DiscreteFibration.Pullback

Imports

/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module

public import Geb.Mathlib.CategoryTheory.DiscreteFibration.Basic

Discrete fibrations: the codomain square

The internal formulation of a discrete fibration ([LoregianRiehl2018] § 2.1, Definition internaldefn; [nLabDiscreteFibration]): the square

Arrow C ---right---> C
   |                 |
   | p               | p
   v                 v
Arrow B ---right---> B

of codomain maps is a pullback of types.

Main definitions

CodPullback p, the pullback Arrow B ×_B C of types.

codPair p, the comparison map Arrow C → Arrow B ×_B C.

IsDiscreteFibration p, the proposition that codPair p is a bijection.

Main statements

DiscreteFibration.isDiscreteFibration: lifting data forces the square to be a pullback. The converse needs Classical.choice and lives in Geb/Mathlib/CategoryTheory/DiscreteFibration/Packaged.lean.

References

[LoregianRiehl2018]

[nLabDiscreteFibration]

Tags

discrete fibration, pullback, arrow category

              @[expose] public sectionuniverse v₁ v₂ u₁ u₂namespace CategoryTheoryvariable {C : Type u₁} [Category.{v₁} C] {B : Type u₂} [Category.{v₂} B]

The set-theoretic pullback Arrow B ×_B C of right : Arrow B → B along p : C → B: an arrow of B with an object of C over its codomain.

abbrev CodPullback (p : C ⥤ B) : Type (max u₁ u₂ v₂) :=
  { q : Arrow B × C // q.1.right = p.obj q.2 }

The comparison map (p, right) : Arrow C → Arrow B ×_B C.

def codPair (p : C ⥤ B) (a : Arrow C) : CodPullback p :=
  ⟨(Arrow.mk (p.map a.hom), a.right), rfl⟩

@[simp] theorem codPair_val (p : C ⥤ B) (a : Arrow C) :
    (codPair p a).1 = (Arrow.mk (p.map a.hom), a.right) := rfl

The pullback-square formulation: p is a discrete fibration iff its codomain square is a pullback of sets, i.e. iff codPair p is a bijection.

def IsDiscreteFibration (p : C ⥤ B) : Prop := Function.Bijective (codPair p)

Lifting data forces the codomain square to be a pullback. No choice is used.

theorem DiscreteFibration.isDiscreteFibration {p : C ⥤ B}
    (D : DiscreteFibration p) : IsDiscreteFibration p := byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration p⊢ IsDiscreteFibration p
  constructorleftC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration p⊢ Function.Injective (codPair p)rightC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration p⊢ Function.Surjective (codPair p)
  ·leftC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration p⊢ Function.Injective (codPair p) rintro ⟨x₁, y₁, f₁⟩ ⟨x₂, y₂, f₂⟩ hleftC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration px₁:Cy₁:Cf₁:(𝟭 C).obj x₁ ⟶ (𝟭 C).obj y₁x₂:Cy₂:Cf₂:(𝟭 C).obj x₂ ⟶ (𝟭 C).obj y₂h:codPair p { left := x₁, right := y₁, hom := f₁ } = codPair p { left := x₂, right := y₂, hom := f₂ }⊢ { left := x₁, right := y₁, hom := f₁ } = { left := x₂, right := y₂, hom := f₂ }
    have hy : y₁ = y₂ := congrArg (fun q : CodPullback p => q.1.2) hleftC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration px₁:Cy₁:Cf₁:(𝟭 C).obj x₁ ⟶ (𝟭 C).obj y₁x₂:Cy₂:Cf₂:(𝟭 C).obj x₂ ⟶ (𝟭 C).obj y₂h:codPair p { left := x₁, right := y₁, hom := f₁ } = codPair p { left := x₂, right := y₂, hom := f₂ }hy:y₁ = y₂⊢ { left := x₁, right := y₁, hom := f₁ } = { left := x₂, right := y₂, hom := f₂ }
    subst hyleftC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration px₁:Cy₁:Cf₁:(𝟭 C).obj x₁ ⟶ (𝟭 C).obj y₁x₂:Cf₂:(𝟭 C).obj x₂ ⟶ (𝟭 C).obj y₁h:codPair p { left := x₁, right := y₁, hom := f₁ } = codPair p { left := x₂, right := y₁, hom := f₂ }⊢ { left := x₁, right := y₁, hom := f₁ } = { left := x₂, right := y₁, hom := f₂ }
    have hf : Arrow.mk (p.map f₁) = Arrow.mk (p.map f₂) :=
      congrArg (fun q : CodPullback p => q.1.1) hleftC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration px₁:Cy₁:Cf₁:(𝟭 C).obj x₁ ⟶ (𝟭 C).obj y₁x₂:Cf₂:(𝟭 C).obj x₂ ⟶ (𝟭 C).obj y₁h:codPair p { left := x₁, right := y₁, hom := f₁ } = codPair p { left := x₂, right := y₁, hom := f₂ }hf:Arrow.mk (p.map f₁) = Arrow.mk (p.map f₂)⊢ { left := x₁, right := y₁, hom := f₁ } = { left := x₂, right := y₁, hom := f₂ }
    exact (D.eq_liftArrow (p.map f₂) f₁ hf).trans
      (D.eq_liftArrow (p.map f₂) f₂ rfl).symmAll goals completed! 🐙
  ·rightC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration p⊢ Function.Surjective (codPair p) rintro ⟨⟨⟨X, Y, g⟩, c⟩, (hg : Y = p.obj c)⟩rightC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:CX:BY:Bg:(𝟭 B).obj X ⟶ (𝟭 B).obj Yhg:Y = p.obj c⊢ ∃ a, codPair p a = ⟨({ left := X, right := Y, hom := g }, c), hg⟩
    subst hgrightC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:CX:Bg:(𝟭 B).obj X ⟶ (𝟭 B).obj (p.obj c)⊢ ∃ a, codPair p a = ⟨({ left := X, right := p.obj c, hom := g }, c), ⋯⟩
    exact ⟨D.liftArrow g, Subtype.ext (Prod.ext (D.arrow_mk_map_hom g) rfl)⟩All goals completed! 🐙

Auxiliary: an arrow equal to Arrow.mk h gives back h up to transport of the codomain.

theorem sigma_eq_of_arrow_eq {c c' : C} (h : c' ⟶ c) (a : Arrow C)
    (ha' : a = Arrow.mk h) (ha : a.right = c) :
    (⟨c', h⟩ : Σ c', c' ⟶ c) = ⟨a.left, a.hom ≫ eqToHom ha⟩ := byC:Type u₁inst✝:Category.{v₁, u₁} Cc:Cc':Ch:c' ⟶ ca:Arrow Cha':a = Arrow.mk hha:a.right = c⊢ ⟨c', h⟩ = ⟨a.left, a.hom ≫ eqToHom ha⟩
  subst ha'C:Type u₁inst✝:Category.{v₁, u₁} Cc:Cc':Ch:c' ⟶ cha:(Arrow.mk h).right = c⊢ ⟨c', h⟩ = ⟨(Arrow.mk h).left, (Arrow.mk h).hom ≫ eqToHom ha⟩
  simpAll goals completed! 🐙

end CategoryTheory