SSet is RegularEpiCategory

Stream: new members

[Fedor Pavutnitskiy]

I am trying to prove instance : RegularEpiCategory SSet, but somehow I got lost, my code so far is

import Mathlib.Tactic
import Mathlib.AlgebraicTopology.SimplicialSet
import Mathlib.CategoryTheory.Adjunction.Evaluation

open CategoryTheory
open Limits

noncomputable section

instance : RegularEpiCategory SSet := by
  refine { regularEpiOfEpi := ?_ }
  intro X Y f epi_f
  rw [NatTrans.epi_iff_epi_app] at epi_f
  have helper : ∀ (c : SimplexCategoryᵒᵖ), RegularEpi (f.app c) := by
    intro c
    exact regularEpiOfEpi (f.app c)
    done
  apply regularEpiOfKernelPair
  apply evaluationJointlyReflectsColimits
  intro c
  specialize helper c
  refine IsColimit.equivOfNatIsoOfIso ?α _ _ ?w helper.isColimit
  · refine parallelPair.ext ?α.zero ?α.one ?α.left ?α.right
    · simp only [parallelPair_obj_zero, Functor.comp_obj, evaluation_obj_obj]
      sorry
    · simp only [parallelPair_obj_one, Functor.comp_obj, evaluation_obj_obj]
      exact Iso.refl _
    · simp only [parallelPair_obj_zero, Functor.comp_obj, parallelPair_obj_one, evaluation_obj_obj,
      parallelPair_map_left, id_eq, Iso.refl_hom, Category.comp_id, Cofork.ofπ_pt,
      Functor.const_obj_obj, Cofork.π_ofπ, Iso.trans_hom, Iso.symm_hom, Functor.comp_map,
      evaluation_obj_map, Category.assoc]
      sorry
    · simp only [parallelPair_obj_zero, Functor.comp_obj, parallelPair_obj_one, evaluation_obj_obj,
      parallelPair_map_right, id_eq, Iso.refl_hom, Category.comp_id, Cofork.ofπ_pt,
      Functor.const_obj_obj, Cofork.π_ofπ, Iso.trans_hom, Iso.symm_hom, Functor.comp_map,
      evaluation_obj_map, Category.assoc]
      sorry
  · sorry
  done

In my naive understanding it should be trivial, am I missing something obvious here?

[Kevin Buzzard]

Can you add any imports and opens to make this a #mwe and thus make it easier for people to answer your question?

[Dagur Asgeirsson]

I guess you want to use the fact that the kernel pair diagram of a regular epi is a coequaliser diagram. This doesn't seem to be stated explicitly, but it can be extracted from docs#CategoryTheory.regularEpiOfEffectiveEpi

[Fedor Pavutnitskiy]

Kevin Buzzard said:

Can you add any imports and opens to make this a #mwe and thus make it easier for people to answer your question?

you are absolutely right, it slipped my mind. I added the imports.

[Fedor Pavutnitskiy]

Dagur Asgeirsson said:

I guess you want to use the fact that the kernel pair diagram of a regular epi is a coequaliser diagram. This doesn't seem to be stated explicitly, but it can be extracted from docs#CategoryTheory.regularEpiOfEffectiveEpi

I have checked EffectiveEpi, but on the first glance did not find what I was looking for. I will meditate some more on it. In my understanding the problem is that we need to show that the choices of RegularEpi.W can be made functorial. So even if we have a statement like def coeq_pull {W X : Type} {l r : W ⟶ X} {c : Cofork l r} (h : IsColimit c) : W ≅ pullback (c.π) (c.π) := sorry, we need to show the naturality of this isomorphism.

[Dean Young]

Would it be easier to first use the construction of a constituent of Category SSet? Just skip this if it's of no use.

  def horn_filling_condition (X : SSet) (n i : Nat): Prop :=
    ∀ f : Λ[n, i] ⟶ X, ∃ g : Δ[n] ⟶ X,
    f = SSet.hornInclusion n i ≫ g

  -- def inner_horn_filling_condition (X : SSet) : Prop :=
  --   ∀ (n i : Nat), n ≥ 2 ∧ 0 < i ∧ i < n →
  --   ∀ f : Λ[n, i] ⟶ X, ∃ g : Δ[n] ⟶ X,
  --   f = SSet.hornInclusion n i ≫ g

  /-- A simplicial set is called an ∞-category if it has the extension property
  for all inner horn inclusions `Λ[n, i] ⟶ Δ[n]`, n ≥ 2, 0 < i < n. -/
  def InfCategory := {X : SSet //
    ∀ (n i : Nat), n ≥ 2 ∧ 0 < i ∧ i < n → horn_filling_condition X n i}

  /-- A Kan complex is a simplicial set X which has the extension property
  for horn inclusions `Λ[n, i] ⟶ Δ[n]` for 0 ≤ i ≤ n. -/
  def KanComplex := {X : SSet //
    ∀ (n i : Nat), 0 ≤ i ∧ i ≤ n → horn_filling_condition X n i}

  #check (inferInstance : Category SSet)
  -- #check (inferInstance : Category InfCategory)
  -- instance : Category InfCategory := inferInstance -- ?
  -- instance : Category InfCategory := by -- ?
  --   dsimp only [InfCategory]
  --   infer_instance
  instance : Category InfCategory where -- reference: https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Functor/Category.html
    Hom X Y := NatTrans X.1 Y.1
    id X := NatTrans.id X.1
    comp α β := NatTrans.vcomp α β
  instance : Category KanComplex where
    Hom X Y := NatTrans X.1 Y.1
    id X := NatTrans.id X.1
    comp α β := NatTrans.vcomp α β
  #check (inferInstance : Category InfCategory)
  #check (inferInstance : Category KanComplex)

end InfCategory

[Joël Riou]

At first glance, the result should not depend on the simplex category at all: this should hold for any category of functors to Type*.

[Fedor Pavutnitskiy]

Dean Young said:

constituent

interesting that you mentioned the Kan condition. This is precisely my application in mind: I am translating our old project with Diana Kalinichenko on the formalization of the Moore's lemma from Lean 3 to Lean 4. Coequalizer description of the horn is the last missing piece and the fact that every epi is regular in SSet is a crucial part. But I can not see immediately how swtiching to infinity categories will help.

[Fedor Pavutnitskiy]

Joël Riou said:

At first glance, the result should not depend on the simplex category at all: this should hold for any category of functors to Type*.

of course. I kept SSet just for simplicity. It will be nice to have a general statement in mathlib of course.

[Joël Riou]

I would start the proof like this:

import Mathlib.CategoryTheory.Limits.Shapes.RegularMono
import Mathlib.CategoryTheory.Limits.FunctorToTypes

universe w v u

namespace CategoryTheory

open Limits

variable {C : Type u} [Category.{v} C]
  {F G : C ⥤ Type w} (f : F ⟶ G)

noncomputable instance [Epi f] : RegularEpi f where
  W := pullback f f
  left := pullback.fst
  right := pullback.snd
  w := pullback.condition
  isColimit := evaluationJointlyReflectsColimits _ (fun X => by
    sorry)

noncomputable instance : RegularEpiCategory (C ⥤ Type w) where
  regularEpiOfEpi _ _ := inferInstance

end CategoryTheory

[Fedor Pavutnitskiy]

Joël Riou said:

I would start the proof like this:

import Mathlib.CategoryTheory.Limits.Shapes.RegularMono
import Mathlib.CategoryTheory.Limits.FunctorToTypes

universe w v u

namespace CategoryTheory

open Limits

variable {C : Type u} [Category.{v} C]
  {F G : C ⥤ Type w} (f : F ⟶ G)

noncomputable instance [Epi f] : RegularEpi f where
  W := pullback f f
  left := pullback.fst
  right := pullback.snd
  w := pullback.condition
  isColimit := evaluationJointlyReflectsColimits _ (fun X => by
    sorry)

noncomputable instance : RegularEpiCategory (C ⥤ Type w) where
  regularEpiOfEpi _ _ := inferInstance

end CategoryTheory

Yep. It more or less equivalent to my code specialized to SSet (modulo using regularEpiOfKernelPair instead of expicit RegularEpi structure). My trouble is to show an equivalence of IsColimit goal in your code to RegularEpiCategory.regularEpiOfEpi (f.app X), which we have from the fact that our functors land in Type w. I used IsColimit.equivOfNatIsoOfIso for that, but perhaps there is a better way?

[Andrew Yang]

I think the best way to start is

import Mathlib

open CategoryTheory CategoryTheory.Limits
variable {C D} [Category C] [Category D] [∀ {X Y : D} (f : X ⟶ Y), HasPullback f f]
variable {F G : C ⥤ D} (α : F ⟶ G)

lemma effectiveEpi_of_effectiveEpi_app [h : ∀ X, EffectiveEpi (α.app X)] :
    EffectiveEpi α := by
  have (X) : HasLimit ((cospan α α).flip.obj X) :=
    @hasLimitOfIso _ _ _ _ _ _ (by dsimp; infer_instance) (diagramIsoCospan _).symm
  have : Limits.HasPullback α α := Limits.HasLimit.mk
      { cone := combineCones _ fun _ => getLimitCone _
        isLimit := combinedIsLimit _ _ }
  apply effectiveEpiOfKernelPair
  apply Limits.evaluationJointlyReflectsColimits
  intro X
  let e : parallelPair (X := pullback α α) pullback.fst pullback.snd ⋙ (evaluation C D).obj X ≅
      parallelPair (X := pullback (α.app X) (α.app X)) pullback.fst pullback.snd := sorry
  refine (IsColimit.precomposeHomEquiv e.symm _) ?_
  refine IsColimit.ofIsoColimit (CategoryTheory.RegularEpi.isColimit (f := α.app X)) ?_
  sorry

[Joël Riou]

I feel it would be convenient to generalize the definition regularEpiOfEffectiveEpi so that we may apply it to any limit pullback cone (rather than the chosen one). It would facilitate the study of the behaviour of these notions with functors which commute to certain limits/colimits.

[Fedor Pavutnitskiy]

Andrew Yang said:

I think the best way to start is ...

Thank you very much for this generalization, I was able to prove the statement with a more restrictive assumption of having all pullbacks in D. It was needed for limitObjIsoLimitCompEvaluation. The key ingredient was to explicitly state the isomorphism (pullback α α).obj X ≅ pullback (α.app X) (α.app X), so it can be simp'ed.

import Mathlib.Tactic

import Mathlib.CategoryTheory.EffectiveEpi.RegularEpi
import Mathlib.CategoryTheory.Limits.FunctorCategory

open CategoryTheory CategoryTheory.Limits

variable {C D} [Category C] [Category D] [HasLimitsOfShape WalkingCospan D]
-- variable [∀ {X Y : D} (f : X ⟶ Y), HasPullback f f]
variable {F G : C ⥤ D} (α : F ⟶ G)



lemma effectiveEpi_of_effectiveEpi_app [h : ∀ X, EffectiveEpi (α.app X)] : EffectiveEpi α := by
  have (X) : HasLimit ((cospan α α).flip.obj X) :=
    @hasLimitOfIso _ _ _ _ _ _ (by dsimp; infer_instance) (diagramIsoCospan _).symm
  have : Limits.HasPullback α α := Limits.HasLimit.mk
      { cone := combineCones _ fun _ ↦ getLimitCone _
        isLimit := combinedIsLimit _ _ }
  apply effectiveEpiOfKernelPair
  apply Limits.evaluationJointlyReflectsColimits
  intro X
  let e : parallelPair (X := pullback α α) pullback.fst pullback.snd ⋙ (evaluation C D).obj X ≅
      parallelPair (X := pullback (α.app X) (α.app X)) pullback.fst pullback.snd := by
        refine parallelPair.ext ?α.zero ?α.one ?α.left ?α.right
        · simp only [Functor.comp_obj, parallelPair_obj_zero, evaluation_obj_obj]
          exact limitObjIsoLimitCompEvaluation _ _ ≪≫ HasLimit.isoOfNatIso (cospanCompIso _ _ _)
        · simp only [Functor.comp_obj, parallelPair_obj_one, evaluation_obj_obj]
          exact Iso.refl _
        · aesop
        · aesop
  refine (IsColimit.precomposeHomEquiv e.symm _) ?_
  refine IsColimit.ofIsoColimit (CategoryTheory.RegularEpi.isColimit (f := α.app X)) ?_
  simp only [Iso.symm_hom]
  refine Cofork.ext ?i ?w
  · simp only [Cofork.ofπ_pt, Cocones.precompose_obj_pt, Functor.mapCocone_pt, evaluation_obj_obj]
    exact Iso.refl _
  · simp only [parallelPair_obj_one, evaluation, Functor.comp_obj, parallelPair_obj_zero, id_eq,
    cospan_left, cospanCompIso_hom_app_left, cospan_right, cospanCompIso_hom_app_right,
    Cocones.precompose, Functor.mapCocone, Cocones.functoriality, Functor.const_obj_obj,
    Functor.comp_map, Functor.const_obj_map, NatTrans.comp_app, eq_mpr_eq_cast, cast_eq,
    Cofork.ofπ_pt, Cofork.ofπ_ι_app, Cofork.π, Iso.refl_hom, Category.comp_id,
    parallelPair.ext_inv_app, Iso.refl_inv, Category.id_comp, e]

Should we consider commiting it to mathlib ?