Documentation

Mathlib.CategoryTheory.Localization.Resolution

Resolutions for a morphism of localizers #

Given a morphism of localizers Φ : LocalizerMorphism W₁ W₂ (i.e. W₁ and W₂ are morphism properties on categories C₁ and C₂, and we have a functor Φ.functor : C₁ ⥤ C₂ which sends morphisms in W₁ to morphisms in W₂), we introduce the notion of right resolutions of objects in C₂: if X₂ : C₂. A right resolution consists of an object X₁ : C₁ and a morphism w : X₂ ⟶ Φ.functor.obj X₁ that is in W₂. Then, the typeclass Φ.HasRightResolutions holds when any X₂ : C₂ has a right resolution.

The type of right resolutions Φ.RightResolution X₂ is endowed with a category structure when the morphism property W₁ is multiplicative.

Similar definitions are done from left resolutions.

Future works #

References #

The category of right resolutions of an object in the target category of a localizer morphism.

  • X₁ : C₁

    an object in the source category

  • w : X₂ Φ.functor.obj self.X₁

    a morphism to an object of the form Φ.functor.obj X₁

  • hw : W₂ self.w
Instances For
    theorem CategoryTheory.LocalizerMorphism.RightResolution.hw {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} (self : Φ.RightResolution X₂) :
    W₂ self.w

    The category of left resolutions of an object in the target category of a localizer morphism.

    • X₁ : C₁

      an object in the source category

    • w : Φ.functor.obj self.X₁ X₂

      a morphism from an object of the form Φ.functor.obj X₁

    • hw : W₂ self.w
    Instances For
      theorem CategoryTheory.LocalizerMorphism.LeftResolution.hw {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} (self : Φ.LeftResolution X₂) :
      W₂ self.w
      theorem CategoryTheory.LocalizerMorphism.RightResolution.mk_surjective {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} (R : Φ.RightResolution X₂) :
      ∃ (X₁ : C₁) (w : X₂ Φ.functor.obj X₁) (hw : W₂ w), R = CategoryTheory.LocalizerMorphism.RightResolution.mk w hw
      theorem CategoryTheory.LocalizerMorphism.LeftResolution.mk_surjective {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} (L : Φ.LeftResolution X₂) :
      ∃ (X₁ : C₁) (w : Φ.functor.obj X₁ X₂) (hw : W₂ w), L = CategoryTheory.LocalizerMorphism.LeftResolution.mk w hw
      @[reducible, inline]

      A localizer morphism has right resolutions when any object has a right resolution.

      Equations
      • Φ.HasRightResolutions = ∀ (X₂ : C₂), Nonempty (Φ.RightResolution X₂)
      Instances For
        @[reducible, inline]

        A localizer morphism has right resolutions when any object has a right resolution.

        Equations
        • Φ.HasLeftResolutions = ∀ (X₂ : C₂), Nonempty (Φ.LeftResolution X₂)
        Instances For
          theorem CategoryTheory.LocalizerMorphism.RightResolution.Hom.ext {C₁ : Type u_1} {C₂ : Type u_2} :
          ∀ {inst : CategoryTheory.Category.{u_5, u_1} C₁} {inst_1 : CategoryTheory.Category.{u_6, u_2} C₂} {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} {R R' : Φ.RightResolution X₂} {x y : R.Hom R'}, x.f = y.fx = y
          theorem CategoryTheory.LocalizerMorphism.RightResolution.Hom.ext_iff {C₁ : Type u_1} {C₂ : Type u_2} :
          ∀ {inst : CategoryTheory.Category.{u_5, u_1} C₁} {inst_1 : CategoryTheory.Category.{u_6, u_2} C₂} {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} {R R' : Φ.RightResolution X₂} {x y : R.Hom R'}, x = y x.f = y.f
          structure CategoryTheory.LocalizerMorphism.RightResolution.Hom {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} (R : Φ.RightResolution X₂) (R' : Φ.RightResolution X₂) :
          Type u_5

          The type of morphisms in the category Φ.RightResolution X₂ (when W₁ is multiplicative).

          Instances For
            theorem CategoryTheory.LocalizerMorphism.RightResolution.Hom.hf {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} {R : Φ.RightResolution X₂} {R' : Φ.RightResolution X₂} (self : R.Hom R') :
            W₁ self.f
            @[simp]
            theorem CategoryTheory.LocalizerMorphism.RightResolution.Hom.comm {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} {R : Φ.RightResolution X₂} {R' : Φ.RightResolution X₂} (self : R.Hom R') :
            CategoryTheory.CategoryStruct.comp R.w (Φ.functor.map self.f) = R'.w
            @[simp]
            theorem CategoryTheory.LocalizerMorphism.RightResolution.Hom.comm_assoc {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} {R : Φ.RightResolution X₂} {R' : Φ.RightResolution X₂} (self : R.Hom R') {Z : C₂} (h : Φ.functor.obj R'.X₁ Z) :
            def CategoryTheory.LocalizerMorphism.RightResolution.Hom.id {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [W₁.ContainsIdentities] (R : Φ.RightResolution X₂) :
            R.Hom R

            The identity of a object in Φ.RightResolution X₂.

            Equations
            Instances For
              @[simp]
              theorem CategoryTheory.LocalizerMorphism.RightResolution.Hom.comp_f {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [W₁.IsMultiplicative] {R : Φ.RightResolution X₂} {R' : Φ.RightResolution X₂} {R'' : Φ.RightResolution X₂} (φ : R.Hom R') (ψ : R'.Hom R'') :
              (φ.comp ψ).f = CategoryTheory.CategoryStruct.comp φ.f ψ.f
              def CategoryTheory.LocalizerMorphism.RightResolution.Hom.comp {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [W₁.IsMultiplicative] {R : Φ.RightResolution X₂} {R' : Φ.RightResolution X₂} {R'' : Φ.RightResolution X₂} (φ : R.Hom R') (ψ : R'.Hom R'') :
              R.Hom R''

              The composition of morphisms in Φ.RightResolution X₂.

              Equations
              Instances For
                Equations
                theorem CategoryTheory.LocalizerMorphism.RightResolution.comp_f_assoc {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [W₁.IsMultiplicative] {R : Φ.RightResolution X₂} {R' : Φ.RightResolution X₂} {R'' : Φ.RightResolution X₂} (φ : R R') (ψ : R' R'') {Z : C₁} (h : R''.X₁ Z) :
                @[simp]
                theorem CategoryTheory.LocalizerMorphism.RightResolution.comp_f {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [W₁.IsMultiplicative] {R : Φ.RightResolution X₂} {R' : Φ.RightResolution X₂} {R'' : Φ.RightResolution X₂} (φ : R R') (ψ : R' R'') :
                theorem CategoryTheory.LocalizerMorphism.RightResolution.hom_ext_iff {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [W₁.IsMultiplicative] {R : Φ.RightResolution X₂} {R' : Φ.RightResolution X₂} {φ₁ : R R'} {φ₂ : R R'} :
                φ₁ = φ₂ φ₁.f = φ₂.f
                theorem CategoryTheory.LocalizerMorphism.RightResolution.hom_ext {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [W₁.IsMultiplicative] {R : Φ.RightResolution X₂} {R' : Φ.RightResolution X₂} {φ₁ : R R'} {φ₂ : R R'} (h : φ₁.f = φ₂.f) :
                φ₁ = φ₂
                theorem CategoryTheory.LocalizerMorphism.LeftResolution.Hom.ext_iff {C₁ : Type u_1} {C₂ : Type u_2} :
                ∀ {inst : CategoryTheory.Category.{u_5, u_1} C₁} {inst_1 : CategoryTheory.Category.{u_6, u_2} C₂} {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} {L L' : Φ.LeftResolution X₂} {x y : L.Hom L'}, x = y x.f = y.f
                theorem CategoryTheory.LocalizerMorphism.LeftResolution.Hom.ext {C₁ : Type u_1} {C₂ : Type u_2} :
                ∀ {inst : CategoryTheory.Category.{u_5, u_1} C₁} {inst_1 : CategoryTheory.Category.{u_6, u_2} C₂} {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} {L L' : Φ.LeftResolution X₂} {x y : L.Hom L'}, x.f = y.fx = y
                structure CategoryTheory.LocalizerMorphism.LeftResolution.Hom {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} (L : Φ.LeftResolution X₂) (L' : Φ.LeftResolution X₂) :
                Type u_5

                The type of morphisms in the category Φ.LeftResolution X₂ (when W₁ is multiplicative).

                Instances For
                  theorem CategoryTheory.LocalizerMorphism.LeftResolution.Hom.hf {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} {L : Φ.LeftResolution X₂} {L' : Φ.LeftResolution X₂} (self : L.Hom L') :
                  W₁ self.f
                  @[simp]
                  theorem CategoryTheory.LocalizerMorphism.LeftResolution.Hom.comm {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} {L : Φ.LeftResolution X₂} {L' : Φ.LeftResolution X₂} (self : L.Hom L') :
                  CategoryTheory.CategoryStruct.comp (Φ.functor.map self.f) L'.w = L.w
                  @[simp]
                  theorem CategoryTheory.LocalizerMorphism.LeftResolution.Hom.comm_assoc {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} {L : Φ.LeftResolution X₂} {L' : Φ.LeftResolution X₂} (self : L.Hom L') {Z : C₂} (h : X₂ Z) :
                  def CategoryTheory.LocalizerMorphism.LeftResolution.Hom.id {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [W₁.ContainsIdentities] (L : Φ.LeftResolution X₂) :
                  L.Hom L

                  The identity of a object in Φ.LeftResolution X₂.

                  Equations
                  Instances For
                    @[simp]
                    theorem CategoryTheory.LocalizerMorphism.LeftResolution.Hom.comp_f {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [W₁.IsMultiplicative] {L : Φ.LeftResolution X₂} {L' : Φ.LeftResolution X₂} {L'' : Φ.LeftResolution X₂} (φ : L.Hom L') (ψ : L'.Hom L'') :
                    (φ.comp ψ).f = CategoryTheory.CategoryStruct.comp φ.f ψ.f
                    def CategoryTheory.LocalizerMorphism.LeftResolution.Hom.comp {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [W₁.IsMultiplicative] {L : Φ.LeftResolution X₂} {L' : Φ.LeftResolution X₂} {L'' : Φ.LeftResolution X₂} (φ : L.Hom L') (ψ : L'.Hom L'') :
                    L.Hom L''

                    The composition of morphisms in Φ.LeftResolution X₂.

                    Equations
                    Instances For
                      Equations
                      theorem CategoryTheory.LocalizerMorphism.LeftResolution.comp_f_assoc {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [W₁.IsMultiplicative] {L : Φ.LeftResolution X₂} {L' : Φ.LeftResolution X₂} {L'' : Φ.LeftResolution X₂} (φ : L L') (ψ : L' L'') {Z : C₁} (h : L''.X₁ Z) :
                      @[simp]
                      theorem CategoryTheory.LocalizerMorphism.LeftResolution.comp_f {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [W₁.IsMultiplicative] {L : Φ.LeftResolution X₂} {L' : Φ.LeftResolution X₂} {L'' : Φ.LeftResolution X₂} (φ : L L') (ψ : L' L'') :
                      theorem CategoryTheory.LocalizerMorphism.LeftResolution.hom_ext_iff {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [W₁.IsMultiplicative] {L : Φ.LeftResolution X₂} {L' : Φ.LeftResolution X₂} {φ₁ : L L'} {φ₂ : L L'} :
                      φ₁ = φ₂ φ₁.f = φ₂.f
                      theorem CategoryTheory.LocalizerMorphism.LeftResolution.hom_ext {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [W₁.IsMultiplicative] {L : Φ.LeftResolution X₂} {L' : Φ.LeftResolution X₂} {φ₁ : L L'} {φ₂ : L L'} (h : φ₁.f = φ₂.f) :
                      φ₁ = φ₂
                      @[simp]
                      theorem CategoryTheory.LocalizerMorphism.LeftResolution.op_w {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} (L : Φ.LeftResolution X₂) :
                      L.op.w = L.w.op
                      @[simp]
                      theorem CategoryTheory.LocalizerMorphism.LeftResolution.op_X₁ {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} (L : Φ.LeftResolution X₂) :
                      L.op.X₁ = Opposite.op L.X₁
                      def CategoryTheory.LocalizerMorphism.LeftResolution.op {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} (L : Φ.LeftResolution X₂) :
                      Φ.op.RightResolution (Opposite.op X₂)

                      The canonical map Φ.LeftResolution X₂ → Φ.op.RightResolution (Opposite.op X₂).

                      Equations
                      Instances For
                        @[simp]
                        theorem CategoryTheory.LocalizerMorphism.LeftResolution.unop_w {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂ᵒᵖ} (L : Φ.op.LeftResolution X₂) :
                        L.unop.w = L.w.unop
                        @[simp]
                        theorem CategoryTheory.LocalizerMorphism.LeftResolution.unop_X₁ {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂ᵒᵖ} (L : Φ.op.LeftResolution X₂) :
                        L.unop.X₁ = Opposite.unop L.X₁
                        def CategoryTheory.LocalizerMorphism.LeftResolution.unop {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂ᵒᵖ} (L : Φ.op.LeftResolution X₂) :
                        Φ.RightResolution (Opposite.unop X₂)

                        The canonical map Φ.op.LeftResolution X₂ → Φ.RightResolution X₂.

                        Equations
                        Instances For
                          @[simp]
                          theorem CategoryTheory.LocalizerMorphism.RightResolution.op_w {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} (L : Φ.RightResolution X₂) :
                          L.op.w = L.w.op
                          @[simp]
                          theorem CategoryTheory.LocalizerMorphism.RightResolution.op_X₁ {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} (L : Φ.RightResolution X₂) :
                          L.op.X₁ = Opposite.op L.X₁
                          def CategoryTheory.LocalizerMorphism.RightResolution.op {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} (L : Φ.RightResolution X₂) :
                          Φ.op.LeftResolution (Opposite.op X₂)

                          The canonical map Φ.RightResolution X₂ → Φ.op.LeftResolution (Opposite.op X₂).

                          Equations
                          Instances For
                            @[simp]
                            theorem CategoryTheory.LocalizerMorphism.RightResolution.unop_X₁ {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂ᵒᵖ} (L : Φ.op.RightResolution X₂) :
                            L.unop.X₁ = Opposite.unop L.X₁
                            @[simp]
                            theorem CategoryTheory.LocalizerMorphism.RightResolution.unop_w {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂ᵒᵖ} (L : Φ.op.RightResolution X₂) :
                            L.unop.w = L.w.unop
                            def CategoryTheory.LocalizerMorphism.RightResolution.unop {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂ᵒᵖ} (L : Φ.op.RightResolution X₂) :
                            Φ.LeftResolution (Opposite.unop X₂)

                            The canonical map Φ.op.RightResolution X₂ → Φ.LeftResolution X₂.

                            Equations
                            Instances For
                              @[simp]
                              theorem CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor_map_f {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (X₂ : C₂) [W₁.IsMultiplicative] :
                              ∀ {X Y : (Φ.LeftResolution X₂)ᵒᵖ} (φ : X Y), ((CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor Φ X₂).map φ).f = φ.unop.f.op
                              def CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (X₂ : C₂) [W₁.IsMultiplicative] :
                              CategoryTheory.Functor (Φ.LeftResolution X₂)ᵒᵖ (Φ.op.RightResolution (Opposite.op X₂))

                              The functor (Φ.LeftResolution X₂)ᵒᵖ ⥤ Φ.op.RightResolution (Opposite.op X₂).

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[simp]
                                theorem CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor_map_f {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (X₂ : C₂ᵒᵖ) [W₁.IsMultiplicative] :
                                ∀ {X Y : (Φ.op.RightResolution X₂)ᵒᵖ} (φ : X Y), ((CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor Φ X₂).map φ).f = φ.unop.f.unop
                                def CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (X₂ : C₂ᵒᵖ) [W₁.IsMultiplicative] :
                                CategoryTheory.Functor (Φ.op.RightResolution X₂)ᵒᵖ (Φ.LeftResolution (Opposite.unop X₂))

                                The functor (Φ.op.RightResolution X₂)ᵒᵖ ⥤ Φ.LeftResolution X₂.unop.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  def CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (X₂ : C₂) [W₁.IsMultiplicative] :
                                  (Φ.LeftResolution X₂)ᵒᵖ Φ.op.RightResolution (Opposite.op X₂)

                                  The equivalence of categories (Φ.LeftResolution X₂)ᵒᵖ ≌ Φ.op.RightResolution (Opposite.op X₂).

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    theorem CategoryTheory.LocalizerMorphism.essSurj_of_hasRightResolutions {C₁ : Type u_1} {C₂ : Type u_2} {D₂ : Type u_3} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] [Φ.HasRightResolutions] :
                                    (Φ.functor.comp L₂).EssSurj
                                    theorem CategoryTheory.LocalizerMorphism.isIso_iff_of_hasRightResolutions {C₁ : Type u_1} {C₂ : Type u_2} {D₂ : Type u_3} {H : Type u_4} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D₂] [CategoryTheory.Category.{u_8, u_4} H] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] [Φ.HasRightResolutions] {F : CategoryTheory.Functor D₂ H} {G : CategoryTheory.Functor D₂ H} (α : F G) :
                                    CategoryTheory.IsIso α ∀ (X₁ : C₁), CategoryTheory.IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
                                    theorem CategoryTheory.LocalizerMorphism.essSurj_of_hasLeftResolutions {C₁ : Type u_1} {C₂ : Type u_2} {D₂ : Type u_3} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] [Φ.HasLeftResolutions] :
                                    (Φ.functor.comp L₂).EssSurj
                                    theorem CategoryTheory.LocalizerMorphism.isIso_iff_of_hasLeftResolutions {C₁ : Type u_1} {C₂ : Type u_2} {D₂ : Type u_3} {H : Type u_4} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D₂] [CategoryTheory.Category.{u_8, u_4} H] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] [Φ.HasLeftResolutions] {F : CategoryTheory.Functor D₂ H} {G : CategoryTheory.Functor D₂ H} (α : F G) :
                                    CategoryTheory.IsIso α ∀ (X₁ : C₁), CategoryTheory.IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))