English
There is a precise equality expressing Pi.map f as a composite built from canonical isomorphisms and maps arising from f, relating the functorial map on a dependent product to the product of the maps along each coordinate.
Русский
Существует точное равенство, выражающее Pi.map f как композицию, составленную из канонических изоморфизмов и отображений, возникающих из f, которое связывает отображение функции на зависимом произведении с произведениями отображений по координатам.
LaTeX
$$$\mathrm{Pi.map} \, f\;=\; \Big(\mathrm{Pi.binaryFanOfPropIsLimit} \, X \, P\Big).conePointUniqueUpToIso (\mathrm{prodIsProd} \;\ldots) .\mathrm{hom} \\\; \circ \; \mathrm{prod.map} (\mathrm{Pi.map}\; (\lambda i: \{ x:I\mid P x\} \;\mapsto\; f\,i.\text{val})) (\mathrm{Pi.map}\; (\lambda i: \{ x:I\mid \neg P x\} \;\mapsto\; f\,i.\text{val})) \\\; \circ \Big(\mathrm{Pi.binaryFanOfPropIsLimit} \, Y \, P\Big).conePointUniqueUpToIso (\mathrm{prodIsProd} \;\ldots) .inv$$$
Lean4
theorem map_eq_prod_map [∀ i, Decidable (P i)] :
Pi.map f =
((Pi.binaryFanOfPropIsLimit X P).conePointUniqueUpToIso (prodIsProd _ _)).hom ≫
prod.map (Pi.map (fun (i : { x : I // P x }) ↦ f i.val)) (Pi.map (fun (i : { x : I // ¬P x }) ↦ f i.val)) ≫
((Pi.binaryFanOfPropIsLimit Y P).conePointUniqueUpToIso (prodIsProd _ _)).inv :=
by
rw [← Category.assoc, Iso.eq_comp_inv]
dsimp only [IsLimit.conePointUniqueUpToIso, binaryFanOfProp, prodIsProd]
apply prod.hom_ext
all_goals cat_disch
