Geb.Mathlib.CategoryTheory.DiscreteFibration.Packaged

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.FiberPresheaf

Discrete fibrations: the packaged statements

The forms of the discrete-fibration correspondence that bundle their content into a mathlib construction: the converse of the pullback formulation, the equalities of composite functors, the equivalence of categories, and the natural isomorphism.

Main definitions

IsDiscreteFibration.equiv and IsDiscreteFibration.toDiscreteFibration, recovering lifting data from a bijective codPair.

DiscreteFibration.elementsEquivalence, the equivalence between C and the category of elements of its own fibre presheaf.

Functor.CoElements.fiberPresheafIso, the natural isomorphism between the fibre presheaf of π F and F.

Main statements

isDiscreteFibration_iff_nonempty: the two formulations of a discrete fibration agree.

DiscreteFibration.toElements_comp_π and DiscreteFibration.ofElements_comp: both functors lie over B.

DiscreteFibration.toElements_comp_ofElements and DiscreteFibration.ofElements_comp_toElements: both composites are identity functors.

Implementation notes

Every declaration here depends on Classical.choice, and only through a mathlib construction that does: Equiv.ofBijective, Functor.comp in each statement mentioning ⋙, Equivalence.mk, and NatIso.ofComponents. Each has an elementwise counterpart in Geb/Mathlib/CategoryTheory/DiscreteFibration/Pullback.lean or Geb/Mathlib/CategoryTheory/DiscreteFibration/FiberPresheaf.lean that carries the same content within the propext/Quot.sound budget, which is why this module is the only one of the group admitted to GebMeta.classicalAllowedModules.

References

[LoregianRiehl2018]

[nLabDiscreteFibration]

Tags

discrete fibration, equivalence of categories, category of elements

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

The bijection Arrow C ≃ Arrow B ×_B C of a discrete fibration in the pullback-square sense. Classical: Equiv.ofBijective uses choice.

noncomputable def IsDiscreteFibration.equiv {p : C ⥤ B}
    (H : IsDiscreteFibration p) : Arrow C ≃ CodPullback p :=
  Equiv.ofBijective _ H

equiv acts as codPair.

theorem IsDiscreteFibration.equiv_apply {p : C ⥤ B}
    (H : IsDiscreteFibration p) (a : Arrow C) : H.equiv a = codPair p a := rfl

Classical converse: a bijective codPair p yields lifting data. Uses Classical.choice; kept apart from the constructive development.

noncomputable def IsDiscreteFibration.toDiscreteFibration {p : C ⥤ B}
    (H : IsDiscreteFibration p) : DiscreteFibration p := byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BH:IsDiscreteFibration p⊢ DiscreteFibration p
  have hl : ∀ q, codPair p (H.equiv.symm q) = q := fun q =>
    (H.equiv_apply _).symm.trans (H.equiv.apply_symm_apply q)C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BH:IsDiscreteFibration phl:∀ (q : CodPullback p), codPair p (H.equiv.symm q) = q⊢ DiscreteFibration p
  have hr : ∀ {b : B} {c : C} (g : b ⟶ p.obj c),
      (H.equiv.symm ⟨(Arrow.mk g, c), rfl⟩).right = c :=
    fun g => congrArg (fun q : CodPullback p => q.1.2) (hl _)C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BH:IsDiscreteFibration phl:∀ (q : CodPullback p), codPair p (H.equiv.symm q) = qhr:∀ {b : B} {c : C} (g : b ⟶ p.obj c), (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).right = c⊢ DiscreteFibration p
  have hm : ∀ {b : B} {c : C} (g : b ⟶ p.obj c),
      Arrow.mk (p.map (H.equiv.symm ⟨(Arrow.mk g, c), rfl⟩).hom) =
        Arrow.mk g :=
    fun g => congrArg (fun q : CodPullback p => q.1.1) (hl _)C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BH:IsDiscreteFibration phl:∀ (q : CodPullback p), codPair p (H.equiv.symm q) = qhr:∀ {b : B} {c : C} (g : b ⟶ p.obj c), (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).right = chm:∀ {b : B} {c : C} (g : b ⟶ p.obj c), Arrow.mk (p.map (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).hom) = Arrow.mk g⊢ DiscreteFibration p
  refine
    { src := fun {b c} g => (H.equiv.symm ⟨(Arrow.mk g, c), rfl⟩).left
      hom := fun {b c} g =>
        (H.equiv.symm ⟨(Arrow.mk g, c), rfl⟩).hom ≫ eqToHom (hr g)
      obj_src := fun {b c} g =>
        congrArg (fun q : CodPullback p => q.1.1.left) (hl _)
      map_hom := fun {b c} g => ?_
      unique := fun {b c} g {c'} h eh hh => ?_ }refine_1C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BH:IsDiscreteFibration phl:∀ (q : CodPullback p), codPair p (H.equiv.symm q) = qhr:∀ {b : B} {c : C} (g : b ⟶ p.obj c), (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).right = chm:∀ {b : B} {c : C} (g : b ⟶ p.obj c), Arrow.mk (p.map (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).hom) = Arrow.mk gb:Bc:Cg:b ⟶ p.obj c⊢ p.map ((H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).hom ≫ eqToHom ⋯) = eqToHom ⋯ ≫ grefine_2C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BH:IsDiscreteFibration phl:∀ (q : CodPullback p), codPair p (H.equiv.symm q) = qhr:∀ {b : B} {c : C} (g : b ⟶ p.obj c), (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).right = chm:∀ {b : B} {c : C} (g : b ⟶ p.obj c), Arrow.mk (p.map (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).hom) = Arrow.mk gb:Bc:Cg:b ⟶ p.obj cc':Ch:c' ⟶ ceh:p.obj c' = bhh:p.map h = eqToHom eh ≫ g⊢ ⟨c', h⟩ = ⟨(H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).left, (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).hom ≫ eqToHom ⋯⟩
  ·refine_1C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BH:IsDiscreteFibration phl:∀ (q : CodPullback p), codPair p (H.equiv.symm q) = qhr:∀ {b : B} {c : C} (g : b ⟶ p.obj c), (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).right = chm:∀ {b : B} {c : C} (g : b ⟶ p.obj c), Arrow.mk (p.map (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).hom) = Arrow.mk gb:Bc:Cg:b ⟶ p.obj c⊢ p.map ((H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).hom ≫ eqToHom ⋯) = eqToHom ⋯ ≫ g obtain ⟨hX, hY, hf⟩ := (Arrow.mk_eq_mk_iff _ _).1 (hm g)refine_1C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BH:IsDiscreteFibration phl:∀ (q : CodPullback p), codPair p (H.equiv.symm q) = qhr:∀ {b : B} {c : C} (g : b ⟶ p.obj c), (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).right = chm:∀ {b : B} {c : C} (g : b ⟶ p.obj c), Arrow.mk (p.map (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).hom) = Arrow.mk gb:Bc:Cg:b ⟶ p.obj chX:p.obj (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).left = bhY:p.obj (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).right = p.obj chf:p.map (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).hom = eqToHom hX ≫ g ≫ eqToHom ⋯⊢ p.map ((H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).hom ≫ eqToHom ⋯) = eqToHom ⋯ ≫ g
    simp only [Functor.map_comp, eqToHom_map, hf]refine_1C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BH:IsDiscreteFibration phl:∀ (q : CodPullback p), codPair p (H.equiv.symm q) = qhr:∀ {b : B} {c : C} (g : b ⟶ p.obj c), (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).right = chm:∀ {b : B} {c : C} (g : b ⟶ p.obj c), Arrow.mk (p.map (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).hom) = Arrow.mk gb:Bc:Cg:b ⟶ p.obj chX:p.obj (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).left = bhY:p.obj (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).right = p.obj chf:p.map (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).hom = eqToHom hX ≫ g ≫ eqToHom ⋯⊢ (eqToHom hX ≫ g ≫ eqToHom ⋯) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ g
    simpAll goals completed! 🐙
  ·refine_2C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BH:IsDiscreteFibration phl:∀ (q : CodPullback p), codPair p (H.equiv.symm q) = qhr:∀ {b : B} {c : C} (g : b ⟶ p.obj c), (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).right = chm:∀ {b : B} {c : C} (g : b ⟶ p.obj c), Arrow.mk (p.map (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).hom) = Arrow.mk gb:Bc:Cg:b ⟶ p.obj cc':Ch:c' ⟶ ceh:p.obj c' = bhh:p.map h = eqToHom eh ≫ g⊢ ⟨c', h⟩ = ⟨(H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).left, (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).hom ≫ eqToHom ⋯⟩ refine sigma_eq_of_arrow_eq h _ ?_ (hr g)refine_2C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BH:IsDiscreteFibration phl:∀ (q : CodPullback p), codPair p (H.equiv.symm q) = qhr:∀ {b : B} {c : C} (g : b ⟶ p.obj c), (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).right = chm:∀ {b : B} {c : C} (g : b ⟶ p.obj c), Arrow.mk (p.map (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).hom) = Arrow.mk gb:Bc:Cg:b ⟶ p.obj cc':Ch:c' ⟶ ceh:p.obj c' = bhh:p.map h = eqToHom eh ≫ g⊢ H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩ = Arrow.mk h
    apply H.equiv.injectiverefine_2C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BH:IsDiscreteFibration phl:∀ (q : CodPullback p), codPair p (H.equiv.symm q) = qhr:∀ {b : B} {c : C} (g : b ⟶ p.obj c), (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).right = chm:∀ {b : B} {c : C} (g : b ⟶ p.obj c), Arrow.mk (p.map (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).hom) = Arrow.mk gb:Bc:Cg:b ⟶ p.obj cc':Ch:c' ⟶ ceh:p.obj c' = bhh:p.map h = eqToHom eh ≫ g⊢ H.equiv (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩) = H.equiv (Arrow.mk h)
    rw [H.equiv.apply_symm_apply,refine_2C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BH:IsDiscreteFibration phl:∀ (q : CodPullback p), codPair p (H.equiv.symm q) = qhr:∀ {b : B} {c : C} (g : b ⟶ p.obj c), (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).right = chm:∀ {b : B} {c : C} (g : b ⟶ p.obj c), Arrow.mk (p.map (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).hom) = Arrow.mk gb:Bc:Cg:b ⟶ p.obj cc':Ch:c' ⟶ ceh:p.obj c' = bhh:p.map h = eqToHom eh ≫ g⊢ ⟨(Arrow.mk g, c), ⋯⟩ = H.equiv (Arrow.mk h) H.equiv_applyrefine_2C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BH:IsDiscreteFibration phl:∀ (q : CodPullback p), codPair p (H.equiv.symm q) = qhr:∀ {b : B} {c : C} (g : b ⟶ p.obj c), (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).right = chm:∀ {b : B} {c : C} (g : b ⟶ p.obj c), Arrow.mk (p.map (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).hom) = Arrow.mk gb:Bc:Cg:b ⟶ p.obj cc':Ch:c' ⟶ ceh:p.obj c' = bhh:p.map h = eqToHom eh ≫ g⊢ ⟨(Arrow.mk g, c), ⋯⟩ = codPair p (Arrow.mk h)]refine_2C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BH:IsDiscreteFibration phl:∀ (q : CodPullback p), codPair p (H.equiv.symm q) = qhr:∀ {b : B} {c : C} (g : b ⟶ p.obj c), (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).right = chm:∀ {b : B} {c : C} (g : b ⟶ p.obj c), Arrow.mk (p.map (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).hom) = Arrow.mk gb:Bc:Cg:b ⟶ p.obj cc':Ch:c' ⟶ ceh:p.obj c' = bhh:p.map h = eqToHom eh ≫ g⊢ ⟨(Arrow.mk g, c), ⋯⟩ = codPair p (Arrow.mk h)
    exact Subtype.ext (Prod.ext
      ((Arrow.mk_eq_mk_iff _ _).2 ⟨eh, rfl, byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BH:IsDiscreteFibration phl:∀ (q : CodPullback p), codPair p (H.equiv.symm q) = qhr:∀ {b : B} {c : C} (g : b ⟶ p.obj c), (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).right = chm:∀ {b : B} {c : C} (g : b ⟶ p.obj c), Arrow.mk (p.map (H.equiv.symm ⟨(Arrow.mk g, c), ⋯⟩).hom) = Arrow.mk gb:Bc:Cg:b ⟶ p.obj cc':Ch:c' ⟶ ceh:p.obj c' = bhh:p.map h = eqToHom eh ≫ g⊢ p.map (Arrow.mk h).hom = eqToHom eh ≫ g ≫ eqToHom ⋯ simpa using hhAll goals completed! 🐙⟩).symm rfl)

A discrete fibration in the pullback sense admits lifting data.

theorem IsDiscreteFibration.nonempty {p : C ⥤ B}
    (H : IsDiscreteFibration p) : Nonempty (DiscreteFibration p) :=
  ⟨H.toDiscreteFibration⟩

The two formulations agree: the codomain square is a pullback exactly when lifting data exists. Lifting data is a Subsingleton, so the Nonempty on the right loses nothing.

theorem isDiscreteFibration_iff_nonempty {p : C ⥤ B} :
    IsDiscreteFibration p ↔ Nonempty (DiscreteFibration p) :=
  ⟨fun H => H.nonempty, fun ⟨D⟩ => D.isDiscreteFibration⟩

              namespace DiscreteFibrationvariable {p : C ⥤ B} (D : DiscreteFibration p)include D

toElements lies over B.

theorem toElements_comp_π :
    D.toElements ⋙ Functor.CoElements.π D.fiberPresheaf = p := rfl

ofElements lies over B.

theorem ofElements_comp : D.ofElements ⋙ p = Functor.CoElements.π D.fiberPresheaf :=
  Functor.ext (fun x => D.obj_elt x) (fun x y f => byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration px:D.fiberPresheaf.CoElementsy:D.fiberPresheaf.CoElementsf:x ⟶ y⊢ (D.ofElements ⋙ p).map f = eqToHom ⋯ ≫ (Functor.CoElements.π D.fiberPresheaf).map f ≫ eqToHom ⋯
    rw [Functor.comp_map,C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration px:D.fiberPresheaf.CoElementsy:D.fiberPresheaf.CoElementsf:x ⟶ y⊢ p.map (D.ofElements.map f) = eqToHom ⋯ ≫ (Functor.CoElements.π D.fiberPresheaf).map f ≫ eqToHom ⋯ D.map_ofElements_mapC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration px:D.fiberPresheaf.CoElementsy:D.fiberPresheaf.CoElementsf:x ⟶ y⊢ eqToHom ⋯ ≫ Functor.CoElements.homBase f ≫ eqToHom ⋯ =
  eqToHom ⋯ ≫ (Functor.CoElements.π D.fiberPresheaf).map f ≫ eqToHom ⋯]C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration px:D.fiberPresheaf.CoElementsy:D.fiberPresheaf.CoElementsf:x ⟶ y⊢ eqToHom ⋯ ≫ Functor.CoElements.homBase f ≫ eqToHom ⋯ =
  eqToHom ⋯ ≫ (Functor.CoElements.π D.fiberPresheaf).map f ≫ eqToHom ⋯
    rflAll goals completed! 🐙)

ofElements undoes toElements.

theorem toElements_comp_ofElements : D.toElements ⋙ D.ofElements = 𝟭 C :=
  Functor.ext (fun c => rfl) (fun c c' f => byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:Cc':Cf:c ⟶ c'⊢ (D.toElements ⋙ D.ofElements).map f = eqToHom ⋯ ≫ (𝟭 C).map f ≫ eqToHom ⋯
    change D.ofElements.map (D.toElements.map f) = 𝟙 _ ≫ f ≫ 𝟙 _C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:Cc':Cf:c ⟶ c'⊢ D.ofElements.map (D.toElements.map f) = 𝟙 c ≫ f ≫ 𝟙 c'
    rw [D.ofElements_map_toElements_map,C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:Cc':Cf:c ⟶ c'⊢ f = 𝟙 c ≫ f ≫ 𝟙 c' Category.id_comp,C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:Cc':Cf:c ⟶ c'⊢ f = f ≫ 𝟙 c' Category.comp_idC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:Cc':Cf:c ⟶ c'⊢ f = f]All goals completed! 🐙)

toElements undoes ofElements.

theorem ofElements_comp_toElements :
    D.ofElements ⋙ D.toElements = 𝟭 D.fiberPresheaf.CoElements :=
  Functor.ext (fun x => (D.coElements_eq_toElements_obj x).symm) (fun x y f => byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration px:D.fiberPresheaf.CoElementsy:D.fiberPresheaf.CoElementsf:x ⟶ y⊢ (D.ofElements ⋙ D.toElements).map f = eqToHom ⋯ ≫ (𝟭 D.fiberPresheaf.CoElements).map f ≫ eqToHom ⋯
    obtain ⟨c, rfl⟩ : ∃ c, x = D.toElements.obj c :=
      ⟨_, D.coElements_eq_toElements_obj x⟩C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration py:D.fiberPresheaf.CoElementsc:Cf:D.toElements.obj c ⟶ y⊢ (D.ofElements ⋙ D.toElements).map f = eqToHom ⋯ ≫ (𝟭 D.fiberPresheaf.CoElements).map f ≫ eqToHom ⋯
    obtain ⟨c', rfl⟩ : ∃ c', y = D.toElements.obj c' :=
      ⟨_, D.coElements_eq_toElements_obj y⟩C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:Cc':Cf:D.toElements.obj c ⟶ D.toElements.obj c'⊢ (D.ofElements ⋙ D.toElements).map f = eqToHom ⋯ ≫ (𝟭 D.fiberPresheaf.CoElements).map f ≫ eqToHom ⋯
    change D.toElements.map (D.ofElements.map f) = 𝟙 _ ≫ f ≫ 𝟙 _C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:Cc':Cf:D.toElements.obj c ⟶ D.toElements.obj c'⊢ D.toElements.map (D.ofElements.map f) = 𝟙 (D.toElements.obj c) ≫ f ≫ 𝟙 (D.toElements.obj c')
    rw [D.toElements_map_ofElements_map,C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:Cc':Cf:D.toElements.obj c ⟶ D.toElements.obj c'⊢ f = 𝟙 (D.toElements.obj c) ≫ f ≫ 𝟙 (D.toElements.obj c') Category.id_comp,C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:Cc':Cf:D.toElements.obj c ⟶ D.toElements.obj c'⊢ f = f ≫ 𝟙 (D.toElements.obj c') Category.comp_idC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:Cc':Cf:D.toElements.obj c ⟶ D.toElements.obj c'⊢ f = f]All goals completed! 🐙)

The two functors assemble into an equivalence, so a discrete fibration over B is the category of elements of its own fibre presheaf. Both composites are identity functors on the nose, so the unit and counit are eqToIsos.

def elementsEquivalence : C ≌ D.fiberPresheaf.CoElements :=
  .mk D.toElements D.ofElements (eqToIso D.toElements_comp_ofElements.symm)
    (eqToIso D.ofElements_comp_toElements)

              end DiscreteFibrationnamespace Functor.CoElementsvariable (F : Bᵒᵖ ⥤ Type v₃)

The fiber presheaf of π F is naturally isomorphic to F (up to the universe lift forced by F.CoElements : Type (max u₂ v₃)): the fiber over b is {x : F.CoElements // x.base = b}, and x ↦ x.elt, transported along x.base = b, is a bijection onto F b.

def fiberPresheafIso :
    (discreteFibration F).fiberPresheaf ≅ F ⋙ uliftFunctor.{u₂, v₃} :=
  NatIso.ofComponents
    (fun b => ((fiberPresheafEquiv F b.unop).trans Equiv.ulift.symm).toIso)
    (fun {b b'} g => ConcreteCategory.hom_ext _ _ fun x => byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} BF:Bᵒᵖ ⥤ Type v₃b:Bᵒᵖb':Bᵒᵖg:b ⟶ b'x:(discreteFibration F).fiberPresheaf.obj b⊢ (ConcreteCategory.hom
      ((discreteFibration F).fiberPresheaf.map g ≫ ((fiberPresheafEquiv F (unop b')).trans Equiv.ulift.symm).toIso.hom))
    x =
  (ConcreteCategory.hom
      (((fiberPresheafEquiv F (unop b)).trans Equiv.ulift.symm).toIso.hom ≫ (F ⋙ uliftFunctor.{u₂, v₃}).map g))
    x
      have h := fiberPresheafEquiv_restrict F g.unop xC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} BF:Bᵒᵖ ⥤ Type v₃b:Bᵒᵖb':Bᵒᵖg:b ⟶ b'x:(discreteFibration F).fiberPresheaf.obj bh:(fiberPresheafEquiv F (unop b')) ((discreteFibration F).restrict g.unop x) =
  (ConcreteCategory.hom (F.map g.unop.op)) ((fiberPresheafEquiv F (unop b)) x)⊢ (ConcreteCategory.hom
      ((discreteFibration F).fiberPresheaf.map g ≫ ((fiberPresheafEquiv F (unop b')).trans Equiv.ulift.symm).toIso.hom))
    x =
  (ConcreteCategory.hom
      (((fiberPresheafEquiv F (unop b)).trans Equiv.ulift.symm).toIso.hom ≫ (F ⋙ uliftFunctor.{u₂, v₃}).map g))
    x
      rw [Quiver.Hom.op_unopC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} BF:Bᵒᵖ ⥤ Type v₃b:Bᵒᵖb':Bᵒᵖg:b ⟶ b'x:(discreteFibration F).fiberPresheaf.obj bh:(fiberPresheafEquiv F (unop b')) ((discreteFibration F).restrict g.unop x) =
  (ConcreteCategory.hom (F.map g)) ((fiberPresheafEquiv F (unop b)) x)⊢ (ConcreteCategory.hom
      ((discreteFibration F).fiberPresheaf.map g ≫ ((fiberPresheafEquiv F (unop b')).trans Equiv.ulift.symm).toIso.hom))
    x =
  (ConcreteCategory.hom
      (((fiberPresheafEquiv F (unop b)).trans Equiv.ulift.symm).toIso.hom ≫ (F ⋙ uliftFunctor.{u₂, v₃}).map g))
    x] at hC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} BF:Bᵒᵖ ⥤ Type v₃b:Bᵒᵖb':Bᵒᵖg:b ⟶ b'x:(discreteFibration F).fiberPresheaf.obj bh:(fiberPresheafEquiv F (unop b')) ((discreteFibration F).restrict g.unop x) =
  (ConcreteCategory.hom (F.map g)) ((fiberPresheafEquiv F (unop b)) x)⊢ (ConcreteCategory.hom
      ((discreteFibration F).fiberPresheaf.map g ≫ ((fiberPresheafEquiv F (unop b')).trans Equiv.ulift.symm).toIso.hom))
    x =
  (ConcreteCategory.hom
      (((fiberPresheafEquiv F (unop b)).trans Equiv.ulift.symm).toIso.hom ≫ (F ⋙ uliftFunctor.{u₂, v₃}).map g))
    x
      exact congrArg ULift.up hAll goals completed! 🐙)

end Functor.CoElementsend CategoryTheory