English
A morphism in a product category is an isomorphism if and only if both its component morphisms are isomorphisms.
Русский
Морфизм в произведении является изоморфизмом тогда и только тогда, когда обе его компоненты являются изоморфизмами.
LaTeX
$$$\mathrm{IsIso}(f) \iff (\mathrm{IsIso}(f.1) \wedge \mathrm{IsIso}(f.2))$$$
Lean4
theorem isIso_prod_iff {P Q : C} {S T : D} {f : (P, S) ⟶ (Q, T)} : IsIso f ↔ IsIso f.1 ∧ IsIso f.2 :=
by
constructor
· rintro ⟨g, hfg, hgf⟩
simp? at hfg hgf says simp only [prod_Hom, prod_comp, prod_id, Prod.mk.injEq] at hfg hgf
rcases hfg with ⟨hfg₁, hfg₂⟩
rcases hgf with ⟨hgf₁, hgf₂⟩
exact ⟨⟨⟨g.1, hfg₁, hgf₁⟩⟩, ⟨⟨g.2, hfg₂, hgf₂⟩⟩⟩
· rintro ⟨⟨g₁, hfg₁, hgf₁⟩, ⟨g₂, hfg₂, hgf₂⟩⟩
dsimp at hfg₁ hgf₁ hfg₂ hgf₂
refine ⟨⟨(g₁, g₂), ?_, ?_⟩⟩
repeat { simp; constructor; assumption; assumption
}
