isPullback_sigmaDesc — Mathlib

English

In a finitaryPreExtensive context, the Sigma-desc constructed pullbacks yield a pullback square for the corresponding data f and g.

Русский

В контексте конечной преф-extensive конструкция Sigma-desc порождает пуллбек-квадрат для соответствующих данных f и g.

LaTeX

$$IsPullback( Sigma.desc f, Sigma.desc g, Sigma.desc f, Sigma.desc g )$$

Lean4

/-- If `C` has pullbacks and is finitary (pre-)extensive, pullbacks distribute over finite
coproducts, i.e., `∐ (Xᵢ ×[S] Xⱼ) ≅ (∐ Xᵢ) ×[S] (∐ Xⱼ)`.
For a variant, see `FinitaryPreExtensive.isIso_sigmaDesc_map`. -/
theorem isPullback_sigmaDesc [HasPullbacks C] [FinitaryPreExtensive C] {ι ι' : Type*} [Finite ι] [Finite ι'] {S : C}
    {X : ι → C} {Y : ι' → C} (f : ∀ i, X i ⟶ S) (g : ∀ i, Y i ⟶ S) :
    IsPullback (Limits.Sigma.desc fun (p : ι × ι') ↦ pullback.fst (f p.1) (g p.2) ≫ Sigma.ι X p.1)
      (Limits.Sigma.desc fun (p : ι × ι') ↦ pullback.snd (f p.1) (g p.2) ≫ Sigma.ι Y p.2) (Limits.Sigma.desc f)
      (Limits.Sigma.desc g) :=
  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)
  convert
    IsUniversalColimit.isPullback_prod_of_isColimit (d :=
      Cofan.mk _ (Sigma.ι fun (p : ι × ι') ↦ pullback (f p.1) (g p.2))) (hd :=
      coproductIsCoproduct (fun (p : ι × ι') ↦ pullback (f p.1) (g p.2))) (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 ↦ IsPullback.of_hasPullback (f i) (g j))
  · ext
    simp [Cofan.IsColimit.desc, Sigma.ι, coproductIsCoproduct]
  · ext
    simp [Cofan.IsColimit.desc, Sigma.ι, coproductIsCoproduct]
  · exact FinitaryPreExtensive.isUniversal_finiteCoproducts (coproductIsCoproduct X)
  · exact FinitaryPreExtensive.isUniversal_finiteCoproducts (coproductIsCoproduct Y)

Похожие утверждения