English
If J is a shape and W is stable under products of shape J, then W is stable under products of shape J.
Русский
Если J — форма, и W стабилен под произведениями формы J, то W стабилен под произведениями формы J.
LaTeX
$$W.IsStableUnderProductsOfShape J$$
Lean4
theorem mk (J : Type*) [W.RespectsIso]
(hW :
∀ (X₁ X₂ : J → C) [HasProduct X₁] [HasProduct X₂] (f : ∀ j, X₁ j ⟶ X₂ j) (_ : ∀ (j : J), W (f j)),
W (Limits.Pi.map f)) :
W.IsStableUnderProductsOfShape J where
condition X₁ X₂ c₁ c₂ hc₁ hc₂ f hf α
hα := by
let φ := fun j => f.app (Discrete.mk j)
have : HasLimit X₁ := ⟨c₁, hc₁⟩
have : HasLimit X₂ := ⟨c₂, hc₂⟩
have : HasProduct fun j ↦ X₁.obj (Discrete.mk j) := hasLimit_of_iso (Discrete.natIso (fun j ↦ Iso.refl (X₁.obj j)))
have : HasProduct fun j ↦ X₂.obj (Discrete.mk j) := hasLimit_of_iso (Discrete.natIso (fun j ↦ Iso.refl (X₂.obj j)))
have hf' := hW _ _ φ (fun j => hf (Discrete.mk j))
refine (W.arrow_mk_iso_iff ?_).2 hf'
refine
Arrow.isoMk (IsLimit.conePointUniqueUpToIso hc₁ (limit.isLimit X₁) ≪≫ (Pi.isoLimit X₁).symm)
(IsLimit.conePointUniqueUpToIso hc₂ (limit.isLimit X₂) ≪≫ (Pi.isoLimit _).symm) ?_
apply limit.hom_ext
rintro ⟨j⟩
simp [φ, hα]
