finitaryExtensive_TopCat — Mathlib

English

TopCat is finitely extensive, supporting finite coproduct distributions through pullbacks.

Русский

TopCat является конечной расширяемой и поддерживает распределение конечных копроизводов через вытягивания.

LaTeX

$$$FinitaryExtensive\; TopCat$$$

Lean4

instance finitaryExtensive_TopCat : FinitaryExtensive TopCat.{u} :=
  by
  rw [finitaryExtensive_iff_of_isTerminal TopCat.{u} _ TopCat.isTerminalPUnit _ (TopCat.binaryCofanIsColimit _ _)]
  apply
    BinaryCofan.isVanKampen_mk _ _ (fun X Y => TopCat.binaryCofanIsColimit X Y) _ fun f g =>
      TopCat.pullbackConeIsLimit f g
  · intro X' Y' αX αY f hαX hαY
    constructor
    · refine ⟨⟨hαX.symm⟩, ⟨PullbackCone.isLimitAux' _ ?_⟩⟩
      intro s
      have : ∀ x, ∃! y, s.fst x = Sum.inl y := by
        intro x
        rcases h : s.fst x with val | val
        · exact ⟨val, rfl, fun y h => Sum.inl_injective h.symm⟩
        · apply_fun f at h
          cases
            ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans (ConcreteCategory.congr_hom hαY val :).symm
      delta ExistsUnique at this
      choose l hl hl' using this
      refine
        ⟨TopCat.ofHom ⟨l, ?_⟩, TopCat.ext fun a => (hl a).symm, TopCat.isTerminalPUnit.hom_ext _ _, fun {l'} h₁ _ =>
          TopCat.ext fun x => hl' x (l' x) (ConcreteCategory.congr_hom h₁ x).symm⟩
      apply (IsEmbedding.inl (X := X') (Y := Y')).isInducing.continuous_iff.mpr
      convert s.fst.hom.2 using 1
      exact (funext hl).symm
    · refine ⟨⟨hαY.symm⟩, ⟨PullbackCone.isLimitAux' _ ?_⟩⟩
      intro s
      have : ∀ x, ∃! y, s.fst x = Sum.inr y := by
        intro x
        rcases h : s.fst x with val | val
        · apply_fun f at h
          cases
            ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans (ConcreteCategory.congr_hom hαX val :).symm
        · exact ⟨val, rfl, fun y h => Sum.inr_injective h.symm⟩
      delta ExistsUnique at this
      choose l hl hl' using this
      refine
        ⟨TopCat.ofHom ⟨l, ?_⟩, TopCat.ext fun a => (hl a).symm, TopCat.isTerminalPUnit.hom_ext _ _, fun {l'} h₁ _ =>
          TopCat.ext fun x => hl' x (l' x) (ConcreteCategory.congr_hom h₁ x).symm⟩
      apply (IsEmbedding.inr (X := X') (Y := Y')).isInducing.continuous_iff.mpr
      convert s.fst.hom.2 using 1
      exact (funext hl).symm
  · intro Z f
    exact finitaryExtensiveTopCatAux Z f

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