Documentation

Mathlib.CategoryTheory.Comma.Over.StrictInitial

Over X when C has strict initial objects #

In this file we define the canonical equivalence of Over X with Discrete PUnit when C has strict initial objects. We also provide the variants for P.Over Q X and the dual versions.

source
noncomputable def CategoryTheory.overEquivOfIsInitial {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasStrictInitialObjects C] (X : C) (h : Limits.IsInitial X) :
Over X ≌ Discrete PUnit.{w + 1}

If C has strict initial objects and X is an initial object, the category Over X is equivalent to a point.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.overEquivOfIsInitial_counitIso {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasStrictInitialObjects C] (X : C) (h : Limits.IsInitial X) :
    (overEquivOfIsInitial.{w, v_1, u_1} X h).counitIso = Iso.refl ((Functor.fromPUnit (Over.mk (CategoryStruct.id X))).comp (Functor.star (Over X)))
    source
    @[simp]
    theorem CategoryTheory.overEquivOfIsInitial_functor {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasStrictInitialObjects C] (X : C) (h : Limits.IsInitial X) :
    (overEquivOfIsInitial.{w, v_1, u_1} X h).functor = Functor.star (Over X)
    source
    @[simp]
    theorem CategoryTheory.overEquivOfIsInitial_unitIso {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasStrictInitialObjects C] (X : C) (h : Limits.IsInitial X) :
    (overEquivOfIsInitial.{w, v_1, u_1} X h).unitIso = NatIso.ofComponents (fun (A : Over X) => Over.isoMk (asIso A.hom) ⋯) ⋯
    source
    @[simp]
    theorem CategoryTheory.overEquivOfIsInitial_inverse {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasStrictInitialObjects C] (X : C) (h : Limits.IsInitial X) :
    (overEquivOfIsInitial.{w, v_1, u_1} X h).inverse = Functor.fromPUnit (Over.mk (CategoryStruct.id X))
    source
    noncomputable def CategoryTheory.underEquivOfIsTerminal {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasStrictTerminalObjects C] (X : C) (h : Limits.IsTerminal X) :
    Under X ≌ Discrete PUnit.{w + 1}

    If C has strict terminal objects and X is a terminal object, the category Under X is equivalent to a point.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.underEquivOfIsTerminal_counitIso {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasStrictTerminalObjects C] (X : C) (h : Limits.IsTerminal X) :
      (underEquivOfIsTerminal.{w, v_1, u_1} X h).counitIso = Iso.refl ((Functor.fromPUnit (Under.mk (CategoryStruct.id X))).comp (Functor.star (Under X)))
      source
      @[simp]
      theorem CategoryTheory.underEquivOfIsTerminal_functor {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasStrictTerminalObjects C] (X : C) (h : Limits.IsTerminal X) :
      (underEquivOfIsTerminal.{w, v_1, u_1} X h).functor = Functor.star (Under X)
      source
      @[simp]
      theorem CategoryTheory.underEquivOfIsTerminal_inverse {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasStrictTerminalObjects C] (X : C) (h : Limits.IsTerminal X) :
      (underEquivOfIsTerminal.{w, v_1, u_1} X h).inverse = Functor.fromPUnit (Under.mk (CategoryStruct.id X))
      source
      @[simp]
      theorem CategoryTheory.underEquivOfIsTerminal_unitIso {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasStrictTerminalObjects C] (X : C) (h : Limits.IsTerminal X) :
      (underEquivOfIsTerminal.{w, v_1, u_1} X h).unitIso = NatIso.ofComponents (fun (A : Under X) => Under.isoMk (asIso A.hom).symm ⋯) ⋯
      source
      noncomputable def CategoryTheory.MorphismProperty.overEquivOfIsInitial {C : Type u_1} [Category.{v_1, u_1} C] (P Q : MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [Limits.HasStrictInitialObjects C] (X : C) (h : Limits.IsInitial X) :
      P.Over Q X ≌ Discrete PUnit.{w + 1}

      If C has strict initial objects and X is an initial object, the category P.Over Q X is equivalent to a point.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.MorphismProperty.overEquivOfIsInitial_inverse {C : Type u_1} [Category.{v_1, u_1} C] (P Q : MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [Limits.HasStrictInitialObjects C] (X : C) (h : Limits.IsInitial X) :
        (overEquivOfIsInitial.{w, v_1, u_1} P Q X h).inverse = Functor.fromPUnit (Over.mk Q (CategoryStruct.id X) ⋯)
        source
        @[simp]
        theorem CategoryTheory.MorphismProperty.overEquivOfIsInitial_counitIso {C : Type u_1} [Category.{v_1, u_1} C] (P Q : MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [Limits.HasStrictInitialObjects C] (X : C) (h : Limits.IsInitial X) :
        (overEquivOfIsInitial.{w, v_1, u_1} P Q X h).counitIso = Iso.refl ((Functor.fromPUnit (Over.mk Q (CategoryStruct.id X) ⋯)).comp (Functor.star (P.Over Q X)))
        source
        @[simp]
        theorem CategoryTheory.MorphismProperty.overEquivOfIsInitial_functor {C : Type u_1} [Category.{v_1, u_1} C] (P Q : MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [Limits.HasStrictInitialObjects C] (X : C) (h : Limits.IsInitial X) :
        (overEquivOfIsInitial.{w, v_1, u_1} P Q X h).functor = Functor.star (P.Over Q X)
        source
        @[simp]
        theorem CategoryTheory.MorphismProperty.overEquivOfIsInitial_unitIso {C : Type u_1} [Category.{v_1, u_1} C] (P Q : MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [Limits.HasStrictInitialObjects C] (X : C) (h : Limits.IsInitial X) :
        (overEquivOfIsInitial.{w, v_1, u_1} P Q X h).unitIso = NatIso.ofComponents (fun (A : P.Over Q X) => Over.isoMk (asIso A.hom) ⋯) ⋯
        source
        noncomputable def CategoryTheory.MorphismProperty.underEquivOfIsTerminal {C : Type u_1} [Category.{v_1, u_1} C] (P Q : MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [Limits.HasStrictTerminalObjects C] (X : C) (h : Limits.IsTerminal X) :
        P.Under Q X ≌ Discrete PUnit.{w + 1}

        If C has strict terminal objects and X is a terminal object, the category P.Under Q X is equivalent to a point.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.MorphismProperty.underEquivOfIsTerminal_functor {C : Type u_1} [Category.{v_1, u_1} C] (P Q : MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [Limits.HasStrictTerminalObjects C] (X : C) (h : Limits.IsTerminal X) :
          (underEquivOfIsTerminal.{w, v_1, u_1} P Q X h).functor = Functor.star (P.Under Q X)
          source
          @[simp]
          theorem CategoryTheory.MorphismProperty.underEquivOfIsTerminal_unitIso {C : Type u_1} [Category.{v_1, u_1} C] (P Q : MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [Limits.HasStrictTerminalObjects C] (X : C) (h : Limits.IsTerminal X) :
          (underEquivOfIsTerminal.{w, v_1, u_1} P Q X h).unitIso = NatIso.ofComponents (fun (A : P.Under Q X) => Under.isoMk (asIso A.hom).symm ⋯) ⋯
          source
          @[simp]
          theorem CategoryTheory.MorphismProperty.underEquivOfIsTerminal_inverse {C : Type u_1} [Category.{v_1, u_1} C] (P Q : MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [Limits.HasStrictTerminalObjects C] (X : C) (h : Limits.IsTerminal X) :
          (underEquivOfIsTerminal.{w, v_1, u_1} P Q X h).inverse = Functor.fromPUnit (Under.mk Q (CategoryStruct.id X) ⋯)
          source
          @[simp]
          theorem CategoryTheory.MorphismProperty.underEquivOfIsTerminal_counitIso {C : Type u_1} [Category.{v_1, u_1} C] (P Q : MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [Limits.HasStrictTerminalObjects C] (X : C) (h : Limits.IsTerminal X) :
          (underEquivOfIsTerminal.{w, v_1, u_1} P Q X h).counitIso = Iso.refl ((Functor.fromPUnit (Under.mk Q (CategoryStruct.id X) ⋯)).comp (Functor.star (P.Under Q X)))