English
There is an equivalence between natural transformations from S.functor to P and compatible families of elements of P with respect to S, given by natTransEquivCompatibleFamily.
Русский
Существует эквивалентность между естественными преобразованиями из S.functor в P и совместимыми семействами элементов P относительно S; это эквивалентность natTransEquivCompatibleFamily.
LaTeX
$${(S.functor ⟶ P)} ≃ { x : FamilyOfElements P (S : Presieve X) // x.Compatible }$$
Lean4
/-- (Implementation). This is a (primarily internal) equivalence between natural transformations
and compatible families.
Cf the discussion after Lemma 7.47.10 in <https://stacks.math.columbia.edu/tag/00YW>. See also
the proof of C2.1.4 of [Elephant], and the discussion in [MM92], Chapter III, Section 4.
-/
def natTransEquivCompatibleFamily {P : Cᵒᵖ ⥤ Type v₁} :
(S.functor ⟶ P) ≃ { x : FamilyOfElements P (S : Presieve X) // x.Compatible }
where
toFun
α := by
refine ⟨fun Y f hf => ?_, ?_⟩
· apply α.app (op Y) ⟨_, hf⟩
· rw [compatible_iff_sieveCompatible]
intro Y Z f g hf
dsimp
rw [← FunctorToTypes.naturality _ _ α g.op]
rfl
invFun
t :=
{ app := fun _ f => t.1 _ f.2
naturality := fun Y Z g => by
ext ⟨f, hf⟩
apply t.2.to_sieveCompatible _ }
left_inv
α := by
ext X ⟨_, _⟩
rfl
right_inv := by
rintro ⟨x, hx⟩
rfl
