English
There is a canonical equivalence between the Pi-category indexed by C with indices J transported along an equivalence e: J ≃ I and the Pi-category indexed by I with the original indices.
Русский
Существуют каноническая эквивалентность между Pi-категорией, индексированной по J и перенесённой через эквивалентность e: J ≃ I, и Pi-категорией, индексированной по I с исходной индексной структурой.
LaTeX
$$$(\\forall j, C (e j)) \\simeq (\\forall i, C i)$$$
Lean4
/-- Two functors to a product category are equal iff they agree on every coordinate. -/
theorem pi_ext (f f' : A ⥤ ∀ i, C i) (h : ∀ i, f ⋙ (Pi.eval C i) = f' ⋙ (Pi.eval C i)) : f = f' :=
by
apply Functor.ext; rotate_left
· intro X
ext i
specialize h i
have := congr_obj h X
simpa
· intro X Y g
funext i
specialize h i
have := congr_hom h g
simpa
