English
In a finitaryPreExtensive setting, a similar isomorphism holds for the full SigmaDesc map constructed from f and g.
Русский
В конечной преф-extensive установке аналогичный изоморфизм справедлив для полного SigmaDesc отображения, построенного из f и g.
LaTeX
$$IsIso( Sigma.desc π_map )$$
Lean4
/-- If `C` has pullbacks and is finitary (pre-)extensive, pullbacks distribute over finite
coproducts, i.e., `∐ (Xᵢ ×[S] Xⱼ) ≅ (∐ Xᵢ) ×[S] (∐ Xⱼ)`.
For an `IsPullback` version, see `FinitaryPreExtensive.isPullback_sigmaDesc`. -/
instance isIso_sigmaDesc_map [HasPullbacks C] [FinitaryPreExtensive C] {ι ι' : Type*} [Finite ι] [Finite ι'] {S : C}
{X : ι → C} {Y : ι' → C} (f : ∀ i, X i ⟶ S) (g : ∀ i, Y i ⟶ S) :
IsIso
(Sigma.desc fun (p : ι × ι') ↦
pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι _ p.1) (Sigma.ι _ p.2) (𝟙 S) (by simp)
(by simp)) :=
by
let c : Cofan _ :=
Cofan.mk _ <| fun (p : ι × ι') ↦
pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι _ p.1) (Sigma.ι _ p.2) (𝟙 S) (by simp)
(by simp)
apply c.isColimit_iff_isIso_sigmaDesc.mpr
refine
IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone (a := Cofan.mk _ <| fun i ↦ Sigma.ι _ i) (b :=
Cofan.mk _ <| fun i ↦ Sigma.ι _ i) ?_ ?_ f g (Sigma.desc f) (Sigma.desc g) (fun i j ↦ (pullback.cone (f i) (g j)))
(fun i j ↦ pullback.isLimit (f i) (g j)) (pullback.cone _ _) ?_ (Iso.refl _)
· exact FinitaryPreExtensive.isUniversal_finiteCoproducts (coproductIsCoproduct X)
· exact FinitaryPreExtensive.isUniversal_finiteCoproducts (coproductIsCoproduct Y)
· exact pullback.isLimit (Sigma.desc f) (Sigma.desc g)
