Geb.Mathlib.CategoryTheory.DiscreteFibration.FiberPresheaf

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

The fibre presheaf of a discrete fibration

The presheaf b ↦ p⁻¹(b) of a discrete fibration, restriction along g being the domain of the unique lift of g ([LoregianRiehl2018] § 2.1; [nLabDiscreteFibration]), together with the functors between C and the category of elements of that presheaf.

Main definitions

DiscreteFibration.restrict and DiscreteFibration.fiberPresheaf, the fibre presheaf.

DiscreteFibration.toElements and DiscreteFibration.ofElements, the functors between C and (fiberPresheaf D).CoElements.

Functor.CoElements.fiberPresheafEquiv, the bijection between the fibre of π F over b and F b.

Main statements

DiscreteFibration.π_toElements_obj, .π_toElements_map and .obj_ofElements_obj: both functors lie over B.

DiscreteFibration.ofElements_map_toElements_map, .ofElements_obj_toElements_obj, .coElements_eq_toElements_obj and .toElements_map_ofElements_map: the two functors are mutually inverse.

Functor.CoElements.fiberPresheafEquiv_restrict: restriction in the fibre presheaf of π F is restriction in F.

Implementation notes

The statements here are elementwise, on objects and on morphisms separately. Their packaged forms, which mention ⋙ or bundle the bijections, inherit Classical.choice from the mathlib constructions they use and live in Geb/Mathlib/CategoryTheory/DiscreteFibration/Packaged.lean.

obj_elt restates a fibre element's defining property with x.base in place of unop (op x.base), which the eqToHom composites below need in order to match.

References

[LoregianRiehl2018]

[nLabDiscreteFibration]

Tags

discrete fibration, fibre, presheaf, 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]namespace DiscreteFibrationvariable {p : C ⥤ B} (D : DiscreteFibration p)include D

Restriction along g : b ⟶ b' of a fiber element c' over b': the domain of the unique lift of g with codomain c'.

def restrict {b b' : B} (g : b ⟶ b') (c' : p.Fiber b') : p.Fiber b :=
  ⟨D.src (g ≫ eqToHom c'.2.symm), D.obj_src _⟩

@[simp] theorem restrict_val {b b' : B} (g : b ⟶ b') (c' : p.Fiber b') :
    (D.restrict g c').1 = D.src (g ≫ eqToHom c'.2.symm) := rfl

Restriction along an identity is the identity.

theorem restrict_id {b : B} (c : p.Fiber b) : D.restrict (𝟙 b) c = c :=
  Subtype.ext (D.src_eq _ (𝟙 c.1) c.2 (byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pb:Bc:p.Fiber b⊢ p.map (𝟙 ↑c) = eqToHom ⋯ ≫ 𝟙 b ≫ eqToHom ⋯ simpAll goals completed! 🐙))

Restriction is contravariantly functorial.

theorem restrict_comp {b b' b'' : B} (g : b ⟶ b') (g' : b' ⟶ b'')
    (c : p.Fiber b'') :
    D.restrict (g ≫ g') c = D.restrict g (D.restrict g' c) := byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pb:Bb':Bb'':Bg:b ⟶ b'g':b' ⟶ b''c:p.Fiber b''⊢ D.restrict (g ≫ g') c = D.restrict g (D.restrict g' c)
  apply Subtype.extC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pb:Bb':Bb'':Bg:b ⟶ b'g':b' ⟶ b''c:p.Fiber b''⊢ ↑(D.restrict (g ≫ g') c) = ↑(D.restrict g (D.restrict g' c))
  exact D.src_eq ((g ≫ g') ≫ eqToHom c.2.symm)
    (D.hom (g ≫ eqToHom (D.obj_src (g' ≫ eqToHom c.2.symm)).symm) ≫
      D.hom (g' ≫ eqToHom c.2.symm))
    (D.obj_src _) (byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pb:Bb':Bb'':Bg:b ⟶ b'g':b' ⟶ b''c:p.Fiber b''⊢ p.map (D.hom (g ≫ eqToHom ⋯) ≫ D.hom (g' ≫ eqToHom ⋯)) = eqToHom ⋯ ≫ (g ≫ g') ≫ eqToHom ⋯ simp [D.map_hom]All goals completed! 🐙)

The fiber presheaf b ↦ p⁻¹(b) of a discrete fibration.

def fiberPresheaf : Bᵒᵖ ⥤ Type u₁ where
  obj b := p.Fiber b.unop
  map g := TypeCat.ofHom fun c => D.restrict g.unop c
  map_id _ := ConcreteCategory.hom_ext _ _ fun c => D.restrict_id c
  map_comp g g' :=
    ConcreteCategory.hom_ext _ _ fun c => D.restrict_comp g'.unop g.unop c

The fiber presheaf's value on objects. Not a simp lemma: it rewrites the object arguments carried by the coercion in fiberPresheaf_map's left-hand side, which would take that lemma out of simp-normal form. Mathlib omits the corresponding yoneda_obj_obj for the same reason, supplying unif_hints instead.

theorem fiberPresheaf_obj (b : Bᵒᵖ) : D.fiberPresheaf.obj b = p.Fiber b.unop := rfl

@[simp] theorem fiberPresheaf_map {b b' : Bᵒᵖ} (g : b ⟶ b')
    (c : p.Fiber b.unop) : D.fiberPresheaf.map g c = D.restrict g.unop c := rfl

`C` and the category of elements of `fiberPresheaf D`

attribute [local simp] eqToHom_map

An element of the fiber presheaf at x lies over x.base. This restates the fiber element's own property, whose type reads p.obj x.elt.1 = unop (op x.base): the unop (op _) blocks the eqToHom composites below from matching.

theorem obj_elt (x : D.fiberPresheaf.CoElements) : p.obj x.elt.1 = x.base :=
  x.elt.2

c ↦ (p c, c).

def toElements : C ⥤ D.fiberPresheaf.CoElements where
  obj c := Functor.CoElements.mk (p.obj c) ⟨c, rfl⟩
  map {c c'} f :=
    Functor.CoElements.homMk (p.map f)
      (Subtype.ext (D.src_eq (p.map f ≫ eqToHom rfl) f rfl
        (byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:Cc':Cf:c ⟶ c'⊢ p.map f = eqToHom ⋯ ≫ p.map f ≫ eqToHom ⋯ change p.map f = eqToHom rfl ≫ p.map f ≫ eqToHom rflC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:Cc':Cf:c ⟶ c'⊢ p.map f = eqToHom ⋯ ≫ p.map f ≫ eqToHom ⋯; simpAll goals completed! 🐙)))
  map_id c := Functor.CoElements.hom_ext (p.map_id c)
  map_comp f g := Functor.CoElements.hom_ext (p.map_comp f g)

@[simp] theorem toElements_obj (c : C) :
    D.toElements.obj c =
      Functor.CoElements.mk (F := D.fiberPresheaf) (p.obj c) ⟨c, rfl⟩ := rfl

@[simp] theorem homBase_toElements_map {c c' : C} (f : c ⟶ c') :
    Functor.CoElements.homBase (D.toElements.map f) = p.map f := rfl

The object underlying the source of f is the domain of the unique lift of homBase f.

theorem obj_eq_src {x y : D.fiberPresheaf.CoElements} (f : x ⟶ y) :
    x.elt.1 = D.src (Functor.CoElements.homBase f ≫ eqToHom (D.obj_elt y).symm) :=
  (congrArg Subtype.val (Functor.CoElements.map_homBase_elt f)).symm

The unique lift of homBase f, transported to a morphism between the underlying objects of C.

def ofElementsMap {x y : D.fiberPresheaf.CoElements} (f : x ⟶ y) :
    x.elt.1 ⟶ y.elt.1 :=
  eqToHom (D.obj_eq_src f) ≫
    D.hom (Functor.CoElements.homBase f ≫ eqToHom (D.obj_elt y).symm)

ofElementsMap f lies over homBase f.

theorem map_ofElementsMap {x y : D.fiberPresheaf.CoElements} (f : x ⟶ y) :
    p.map (D.ofElementsMap f) =
      eqToHom (D.obj_elt x) ≫ Functor.CoElements.homBase f ≫
        eqToHom (D.obj_elt y).symm := 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⊢ p.map (D.ofElementsMap f) = eqToHom ⋯ ≫ Functor.CoElements.homBase f ≫ eqToHom ⋯
  rw [ofElementsMap,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 (eqToHom ⋯ ≫ D.hom (Functor.CoElements.homBase f ≫ eqToHom ⋯)) =
  eqToHom ⋯ ≫ Functor.CoElements.homBase f ≫ eqToHom ⋯ Functor.map_comp,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 (eqToHom ⋯) ≫ p.map (D.hom (Functor.CoElements.homBase f ≫ eqToHom ⋯)) =
  eqToHom ⋯ ≫ Functor.CoElements.homBase f ≫ eqToHom ⋯ eqToHom_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⊢ eqToHom ⋯ ≫ p.map (D.hom (Functor.CoElements.homBase f ≫ eqToHom ⋯)) =
  eqToHom ⋯ ≫ Functor.CoElements.homBase f ≫ eqToHom ⋯ D.map_homC: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 ⋯ ≫ eqToHom ⋯ ≫ Functor.CoElements.homBase f ≫ eqToHom ⋯ = eqToHom ⋯ ≫ Functor.CoElements.homBase 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 ⋯ ≫ eqToHom ⋯ ≫ Functor.CoElements.homBase f ≫ eqToHom ⋯ = eqToHom ⋯ ≫ Functor.CoElements.homBase f ≫ eqToHom ⋯
  simpAll goals completed! 🐙

(b, c) ↦ c.

def ofElements : D.fiberPresheaf.CoElements ⥤ C where
  obj x := x.elt.1
  map f := D.ofElementsMap f
  map_id x :=
    D.map_injective (byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration px:D.fiberPresheaf.CoElements⊢ p.map (D.ofElementsMap (𝟙 x)) = p.map (𝟙 ↑x.elt) rw [D.map_ofElementsMap,C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration px:D.fiberPresheaf.CoElements⊢ eqToHom ⋯ ≫ Functor.CoElements.homBase (𝟙 x) ≫ eqToHom ⋯ = p.map (𝟙 ↑x.elt) p.map_idC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration px:D.fiberPresheaf.CoElements⊢ eqToHom ⋯ ≫ Functor.CoElements.homBase (𝟙 x) ≫ eqToHom ⋯ = 𝟙 (p.obj ↑x.elt)]C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration px:D.fiberPresheaf.CoElements⊢ eqToHom ⋯ ≫ Functor.CoElements.homBase (𝟙 x) ≫ eqToHom ⋯ = 𝟙 (p.obj ↑x.elt); simpAll goals completed! 🐙)
  map_comp f g :=
    D.map_injective (byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pX✝:D.fiberPresheaf.CoElementsY✝:D.fiberPresheaf.CoElementsZ✝:D.fiberPresheaf.CoElementsf:X✝ ⟶ Y✝g:Y✝ ⟶ Z✝⊢ p.map (D.ofElementsMap (f ≫ g)) = p.map (D.ofElementsMap f ≫ D.ofElementsMap g)
      rw [D.map_ofElementsMap,C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pX✝:D.fiberPresheaf.CoElementsY✝:D.fiberPresheaf.CoElementsZ✝:D.fiberPresheaf.CoElementsf:X✝ ⟶ Y✝g:Y✝ ⟶ Z✝⊢ eqToHom ⋯ ≫ Functor.CoElements.homBase (f ≫ g) ≫ eqToHom ⋯ = p.map (D.ofElementsMap f ≫ D.ofElementsMap g) p.map_comp,C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pX✝:D.fiberPresheaf.CoElementsY✝:D.fiberPresheaf.CoElementsZ✝:D.fiberPresheaf.CoElementsf:X✝ ⟶ Y✝g:Y✝ ⟶ Z✝⊢ eqToHom ⋯ ≫ Functor.CoElements.homBase (f ≫ g) ≫ eqToHom ⋯ = p.map (D.ofElementsMap f) ≫ p.map (D.ofElementsMap g) D.map_ofElementsMap,C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pX✝:D.fiberPresheaf.CoElementsY✝:D.fiberPresheaf.CoElementsZ✝:D.fiberPresheaf.CoElementsf:X✝ ⟶ Y✝g:Y✝ ⟶ Z✝⊢ eqToHom ⋯ ≫ Functor.CoElements.homBase (f ≫ g) ≫ eqToHom ⋯ =
  (eqToHom ⋯ ≫ Functor.CoElements.homBase f ≫ eqToHom ⋯) ≫ p.map (D.ofElementsMap g)
        D.map_ofElementsMapC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pX✝:D.fiberPresheaf.CoElementsY✝:D.fiberPresheaf.CoElementsZ✝:D.fiberPresheaf.CoElementsf:X✝ ⟶ Y✝g:Y✝ ⟶ Z✝⊢ eqToHom ⋯ ≫ Functor.CoElements.homBase (f ≫ g) ≫ eqToHom ⋯ =
  (eqToHom ⋯ ≫ Functor.CoElements.homBase f ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ Functor.CoElements.homBase g ≫ 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.CoElementsZ✝:D.fiberPresheaf.CoElementsf:X✝ ⟶ Y✝g:Y✝ ⟶ Z✝⊢ eqToHom ⋯ ≫ Functor.CoElements.homBase (f ≫ g) ≫ eqToHom ⋯ =
  (eqToHom ⋯ ≫ Functor.CoElements.homBase f ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ Functor.CoElements.homBase g ≫ eqToHom ⋯
      simpAll goals completed! 🐙)

@[simp] theorem ofElements_obj (x : D.fiberPresheaf.CoElements) :
    D.ofElements.obj x = x.elt.1 := rfl

ofElements lies over Functor.CoElements.π, elementwise on morphisms.

theorem map_ofElements_map {x y : D.fiberPresheaf.CoElements} (f : x ⟶ y) :
    p.map (D.ofElements.map f) =
      eqToHom (D.obj_elt x) ≫ Functor.CoElements.homBase f ≫
        eqToHom (D.obj_elt y).symm :=
  D.map_ofElementsMap f

toElements lies over B, elementwise on objects.

theorem π_toElements_obj (c : C) :
    (Functor.CoElements.π D.fiberPresheaf).obj (D.toElements.obj c) = p.obj c := rfl

toElements lies over B, elementwise on morphisms.

theorem π_toElements_map {c c' : C} (f : c ⟶ c') :
    (Functor.CoElements.π D.fiberPresheaf).map (D.toElements.map f) = p.map f := rfl

ofElements lies over B, elementwise on objects.

theorem obj_ofElements_obj (x : D.fiberPresheaf.CoElements) :
    p.obj (D.ofElements.obj x) = (Functor.CoElements.π D.fiberPresheaf).obj x :=
  D.obj_elt x

ofElements undoes toElements on morphisms.

theorem ofElements_map_toElements_map {c c' : C} (f : c ⟶ c') :
    D.ofElements.map (D.toElements.map f) = 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.ofElements.map (D.toElements.map f) = f
  apply D.map_injectiveC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:Cc':Cf:c ⟶ c'⊢ p.map (D.ofElements.map (D.toElements.map f)) = p.map f
  rw [D.map_ofElements_mapC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:Cc':Cf:c ⟶ c'⊢ eqToHom ⋯ ≫ Functor.CoElements.homBase (D.toElements.map f) ≫ eqToHom ⋯ = p.map f]C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:Cc':Cf:c ⟶ c'⊢ eqToHom ⋯ ≫ Functor.CoElements.homBase (D.toElements.map f) ≫ eqToHom ⋯ = p.map f
  change 𝟙 _ ≫ p.map f ≫ 𝟙 _ = p.map fC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:Cc':Cf:c ⟶ c'⊢ 𝟙 (p.obj c) ≫ p.map f ≫ 𝟙 (p.obj c') = p.map f
  simpAll goals completed! 🐙

ofElements undoes toElements on objects.

theorem ofElements_obj_toElements_obj (c : C) :
    D.ofElements.obj (D.toElements.obj c) = c := rfl

An element of a fiber is toElements of its underlying object of C.

theorem mk_eq_toElements_obj {b : B} (c : p.Fiber b) :
    Functor.CoElements.mk (F := D.fiberPresheaf) b c = D.toElements.obj c.1 := byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pb:Bc:p.Fiber b⊢ Functor.CoElements.mk b c = D.toElements.obj ↑c
  obtain ⟨c, rfl⟩ := cC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:C⊢ Functor.CoElements.mk (p.obj c) ⟨c, ⋯⟩ = D.toElements.obj ↑⟨c, ⋯⟩
  rflAll goals completed! 🐙

Every object of the category of elements of fiberPresheaf D is toElements of its underlying object of C.

theorem coElements_eq_toElements_obj (x : D.fiberPresheaf.CoElements) :
    x = D.toElements.obj x.elt.1 :=
  (Functor.CoElements.mk_base_elt x).symm.trans (D.mk_eq_toElements_obj x.elt)

toElements undoes ofElements on morphisms.

theorem toElements_map_ofElements_map {c c' : C}
    (f : D.toElements.obj c ⟶ D.toElements.obj c') :
    D.toElements.map (D.ofElements.map f) = f :=
  Functor.CoElements.hom_ext (byC: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'⊢ Functor.CoElements.homBase (D.toElements.map (D.ofElements.map f)) = Functor.CoElements.homBase f
    rw [homBase_toElements_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'⊢ p.map (D.ofElements.map f) = Functor.CoElements.homBase f D.map_ofElements_mapC: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'⊢ eqToHom ⋯ ≫ Functor.CoElements.homBase f ≫ eqToHom ⋯ = Functor.CoElements.homBase 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'⊢ eqToHom ⋯ ≫ Functor.CoElements.homBase f ≫ eqToHom ⋯ = Functor.CoElements.homBase f
    change 𝟙 _ ≫ Functor.CoElements.homBase f ≫ 𝟙 _ =
      Functor.CoElements.homBase fC: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.obj c).base ≫ Functor.CoElements.homBase f ≫ 𝟙 (D.toElements.obj c').base = Functor.CoElements.homBase f
    rw [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'⊢ Functor.CoElements.homBase f ≫ 𝟙 (D.toElements.obj c').base = Functor.CoElements.homBase f 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'⊢ Functor.CoElements.homBase f = Functor.CoElements.homBase f]All goals completed! 🐙)

end DiscreteFibration

The fibre presheaf of `π F`

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

Choice-free and universe-free form of fiberPresheafIso below: the fiber of π F over b is in bijection with F b.

def fiberPresheafEquiv (b : B) : (π F).Fiber b ≃ F.obj (op b)
    where
  toFun x := F.map (eqToHom x.2.symm).op x.1.elt
  invFun y := ⟨mk b y, rfl⟩
  left_inv x := byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} BF:Bᵒᵖ ⥤ Type v₃b:Bx:(π F).Fiber b⊢ (fun y ↦ ⟨mk b y, ⋯⟩) ((fun x ↦ (ConcreteCategory.hom (F.map (eqToHom ⋯).op)) (↑x).elt) x) = x
    obtain ⟨x, hb⟩ := xC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} BF:Bᵒᵖ ⥤ Type v₃b:Bx:F.CoElementshb:(π F).obj x = b⊢ (fun y ↦ ⟨mk b y, ⋯⟩) ((fun x ↦ (ConcreteCategory.hom (F.map (eqToHom ⋯).op)) (↑x).elt) ⟨x, hb⟩) = ⟨x, hb⟩
    subst hbC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} BF:Bᵒᵖ ⥤ Type v₃x:F.CoElements⊢ (fun y ↦ ⟨mk ((π F).obj x) y, ⋯⟩) ((fun x_1 ↦ (ConcreteCategory.hom (F.map (eqToHom ⋯).op)) (↑x_1).elt) ⟨x, ⋯⟩) = ⟨x, ⋯⟩
    refine Subtype.ext ?_C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} BF:Bᵒᵖ ⥤ Type v₃x:F.CoElements⊢ ↑((fun y ↦ ⟨mk ((π F).obj x) y, ⋯⟩) ((fun x_1 ↦ (ConcreteCategory.hom (F.map (eqToHom ⋯).op)) (↑x_1).elt) ⟨x, ⋯⟩)) =
  ↑⟨x, ⋯⟩
    exact (congrArg (mk x.base)
      (ConcreteCategory.congr_hom (F.map_id (op x.base)) x.elt)).trans
      (mk_base_elt x)All goals completed! 🐙
  right_inv y :=
    show F.map (𝟙 (op b)) y = y from
      ConcreteCategory.congr_hom (F.map_id _) y

Naturality of fiberPresheafEquiv: restriction in the fiber presheaf of π F is restriction in F.

theorem fiberPresheafEquiv_restrict {b b' : B} (g : b ⟶ b')
    (x : (π F).Fiber b') :
    fiberPresheafEquiv F b ((discreteFibration F).restrict g x) =
      F.map g.op (fiberPresheafEquiv F b' x) := byB:Type u₂inst✝:Category.{v₂, u₂} BF:Bᵒᵖ ⥤ Type v₃b:Bb':Bg:b ⟶ b'x:(π F).Fiber b'⊢ (fiberPresheafEquiv F b) ((discreteFibration F).restrict g x) =
  (ConcreteCategory.hom (F.map g.op)) ((fiberPresheafEquiv F b') x)
  obtain ⟨x, hb⟩ := xB:Type u₂inst✝:Category.{v₂, u₂} BF:Bᵒᵖ ⥤ Type v₃b:Bb':Bg:b ⟶ b'x:F.CoElementshb:(π F).obj x = b'⊢ (fiberPresheafEquiv F b) ((discreteFibration F).restrict g ⟨x, hb⟩) =
  (ConcreteCategory.hom (F.map g.op)) ((fiberPresheafEquiv F b') ⟨x, hb⟩)
  subst hbB:Type u₂inst✝:Category.{v₂, u₂} BF:Bᵒᵖ ⥤ Type v₃b:Bx:F.CoElementsg:b ⟶ (π F).obj x⊢ (fiberPresheafEquiv F b) ((discreteFibration F).restrict g ⟨x, ⋯⟩) =
  (ConcreteCategory.hom (F.map g.op)) ((fiberPresheafEquiv F ((π F).obj x)) ⟨x, ⋯⟩)
  change F.map (𝟙 _) (F.map (g ≫ 𝟙 _).op x.elt) =
    F.map g.op (F.map (𝟙 _) x.elt)B:Type u₂inst✝:Category.{v₂, u₂} BF:Bᵒᵖ ⥤ Type v₃b:Bx:F.CoElementsg:b ⟶ (π F).obj x⊢ (ConcreteCategory.hom (F.map (𝟙 (op b)))) ((ConcreteCategory.hom (F.map (g ≫ 𝟙 ((π F).obj x)).op)) x.elt) =
  (ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (F.map (𝟙 (op ((π F).obj x))))) x.elt)
  rw [Category.comp_id,B:Type u₂inst✝:Category.{v₂, u₂} BF:Bᵒᵖ ⥤ Type v₃b:Bx:F.CoElementsg:b ⟶ (π F).obj x⊢ (ConcreteCategory.hom (F.map (𝟙 (op b)))) ((ConcreteCategory.hom (F.map g.op)) x.elt) =
  (ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (F.map (𝟙 (op ((π F).obj x))))) x.elt) F.map_id,B:Type u₂inst✝:Category.{v₂, u₂} BF:Bᵒᵖ ⥤ Type v₃b:Bx:F.CoElementsg:b ⟶ (π F).obj x⊢ (ConcreteCategory.hom (𝟙 (F.obj (op b)))) ((ConcreteCategory.hom (F.map g.op)) x.elt) =
  (ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (F.map (𝟙 (op ((π F).obj x))))) x.elt) F.map_idB:Type u₂inst✝:Category.{v₂, u₂} BF:Bᵒᵖ ⥤ Type v₃b:Bx:F.CoElementsg:b ⟶ (π F).obj x⊢ (ConcreteCategory.hom (𝟙 (F.obj (op b)))) ((ConcreteCategory.hom (F.map g.op)) x.elt) =
  (ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (𝟙 (F.obj (op ((π F).obj x))))) x.elt)]B:Type u₂inst✝:Category.{v₂, u₂} BF:Bᵒᵖ ⥤ Type v₃b:Bx:F.CoElementsg:b ⟶ (π F).obj x⊢ (ConcreteCategory.hom (𝟙 (F.obj (op b)))) ((ConcreteCategory.hom (F.map g.op)) x.elt) =
  (ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (𝟙 (F.obj (op ((π F).obj x))))) x.elt)
  rflAll goals completed! 🐙

end Functor.CoElementsend CategoryTheory