English
For a finitaryPreExtensive C, the map described by Sigma.desc and pullback.fst in the fst slot is an isomorphism whenever the data is compatible.
Русский
Для finitaryPreExtensive C отображение, задаваемое Sigma.desc и pullback.fst в первом слоте, является изоморфизмом при совместимости данных.
LaTeX
$$IsIso( Sigma.desc π_fst )$$
Lean4
theorem isIso_sigmaDesc_fst [FinitaryPreExtensive C] {α : Type} [Finite α] {X : C} {Z : α → C} (π : (a : α) → Z a ⟶ X)
{Y : C} (f : Y ⟶ X) (hπ : IsIso (Sigma.desc π)) :
IsIso (Sigma.desc ((fun _ ↦ pullback.fst _ _) : (a : α) → pullback f (π a) ⟶ _)) :=
by
let c := (Cofan.mk _ ((fun _ ↦ pullback.fst _ _) : (a : α) → pullback f (π a) ⟶ _))
apply c.isColimit_iff_isIso_sigmaDesc.mpr
have hau : IsUniversalColimit (Cofan.mk X π) :=
FinitaryPreExtensive.isUniversal_finiteCoproducts ((Cofan.isColimit_iff_isIso_sigmaDesc _).mp hπ).some
refine
hau.nonempty_isColimit_of_pullbackCone_left _ (𝟙 _) _ _ (fun i ↦ ?_) (PullbackCone.mk (𝟙 _) f (by simp))
(IsPullback.id_horiz f).isLimit _ (Iso.refl _) (by simp) (by simp [c]) (by simp [pullback.condition, c])
exact pullback.isLimit _ _
