Morphism properties that are inverted by a functor

In this file, we introduce the predicate P.IsInvertedBy F which expresses that the morphisms satisfying P : MorphismProperty C are mapped to isomorphisms by a functor F : C ⥤ D.

This is used in the localization of categories API (folder CategoryTheory.Localization).

def CategoryTheory.MorphismProperty.IsInvertedBy {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D) : Prop

If P : MorphismProperty C and F : C ⥤ D, then P.IsInvertedBy F means that all morphisms in P are mapped by F to isomorphisms in D.

Equations

• P.IsInvertedBy F = ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P f → CategoryTheory.IsIso (F.map f)

theorem CategoryTheory.MorphismProperty.IsInvertedBy.of_le {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.MorphismProperty C) (Q : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D) (hQ : Q.IsInvertedBy F) (h : P ≤ Q) : P.IsInvertedBy F

theorem CategoryTheory.MorphismProperty.IsInvertedBy.of_comp {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} C₃] (W : CategoryTheory.MorphismProperty C₁) (F : CategoryTheory.Functor C₁ C₂) (hF : W.IsInvertedBy F) (G : CategoryTheory.Functor C₂ C₃) : W.IsInvertedBy (F.comp G)

theorem CategoryTheory.MorphismProperty.IsInvertedBy.op {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {W : CategoryTheory.MorphismProperty C} {L : CategoryTheory.Functor C D} (h : W.IsInvertedBy L) : W.op.IsInvertedBy L.op

theorem CategoryTheory.MorphismProperty.IsInvertedBy.rightOp {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {W : CategoryTheory.MorphismProperty C} {L : CategoryTheory.Functor Cᵒᵖ D} (h : W.op.IsInvertedBy L) : W.IsInvertedBy L.rightOp

theorem CategoryTheory.MorphismProperty.IsInvertedBy.leftOp {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {W : CategoryTheory.MorphismProperty C} {L : CategoryTheory.Functor C Dᵒᵖ} (h : W.IsInvertedBy L) : W.op.IsInvertedBy L.leftOp

theorem CategoryTheory.MorphismProperty.IsInvertedBy.unop {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {W : CategoryTheory.MorphismProperty C} {L : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (h : W.op.IsInvertedBy L) : W.IsInvertedBy L.unop

theorem CategoryTheory.MorphismProperty.IsInvertedBy.prod {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₂} {E₁ : Type u_3} {E₂ : Type u_4} [CategoryTheory.Category.{u_7, u_3} E₁] [CategoryTheory.Category.{u_8, u_4} E₂] {F₁ : CategoryTheory.Functor C₁ E₁} {F₂ : CategoryTheory.Functor C₂ E₂} (h₁ : W₁.IsInvertedBy F₁) (h₂ : W₂.IsInvertedBy F₂) : (W₁.prod W₂).IsInvertedBy (F₁.prod F₂)

theorem CategoryTheory.MorphismProperty.IsInvertedBy.pi {J : Type w} {C : J → Type u} {D : J → Type u'} [(j : J) → CategoryTheory.Category.{v, u} (C j)] [(j : J) → CategoryTheory.Category.{v', u'} (D j)] (W : (j : J) → CategoryTheory.MorphismProperty (C j)) (F : (j : J) → CategoryTheory.Functor (C j) (D j)) (hF : ∀ (j : J), (W j).IsInvertedBy (F j)) : (CategoryTheory.MorphismProperty.pi W).IsInvertedBy (CategoryTheory.Functor.pi F)

def CategoryTheory.MorphismProperty.FunctorsInverting {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] : Type (max (max (max u u_1) v) u_2)

The full subcategory of C ⥤ D consisting of functors inverting morphisms in W

Equations

• W.FunctorsInverting D = CategoryTheory.FullSubcategory fun (F : CategoryTheory.Functor C D) => W.IsInvertedBy F

theorem CategoryTheory.MorphismProperty.FunctorsInverting.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {W : CategoryTheory.MorphismProperty C} {F₁ : W.FunctorsInverting D} {F₂ : W.FunctorsInverting D} (h : F₁.obj = F₂.obj) : F₁ = F₂

instance CategoryTheory.MorphismProperty.instCategoryFunctorsInverting {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] : CategoryTheory.Category.{max u u_2, max (max (max u_2 u_1) u) v} (W.FunctorsInverting D)

Equations

• W.instCategoryFunctorsInverting D = CategoryTheory.FullSubcategory.category fun (F : CategoryTheory.Functor C D) => W.IsInvertedBy F

theorem CategoryTheory.MorphismProperty.FunctorsInverting.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {W : CategoryTheory.MorphismProperty C} {F₁ : W.FunctorsInverting D} {F₂ : W.FunctorsInverting D} {α : F₁ ⟶ F₂} {β : F₁ ⟶ F₂} (h : α.app = β.app) : α = β

def CategoryTheory.MorphismProperty.FunctorsInverting.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (F : CategoryTheory.Functor C D) (hF : W.IsInvertedBy F) : W.FunctorsInverting D

A constructor for W.FunctorsInverting D

Equations

• CategoryTheory.MorphismProperty.FunctorsInverting.mk F hF = { obj := F, property := hF }

theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (W : CategoryTheory.MorphismProperty C) {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) : W.IsInvertedBy F₁ ↔ W.IsInvertedBy F₂

@[simp]

theorem CategoryTheory.MorphismProperty.IsInvertedBy.isoClosure_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (W : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D) : W.isoClosure.IsInvertedBy F ↔ W.IsInvertedBy F

@[simp]

theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_comp {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} C₃] (W : CategoryTheory.MorphismProperty C₁) (F : CategoryTheory.Functor C₁ C₂) (G : CategoryTheory.Functor C₂ C₃) [G.ReflectsIsomorphisms] : W.IsInvertedBy (F.comp G) ↔ W.IsInvertedBy F

theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_le_inverseImage_isomorphisms {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (W : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D) : W.IsInvertedBy F ↔ W ≤ (CategoryTheory.MorphismProperty.isomorphisms D).inverseImage F

theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_map_le_isomorphisms {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (W : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D) : W.IsInvertedBy F ↔ W.map F ≤ CategoryTheory.MorphismProperty.isomorphisms D

theorem CategoryTheory.MorphismProperty.IsInvertedBy.map_iff {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} C₃] (W : CategoryTheory.MorphismProperty C₁) (F : CategoryTheory.Functor C₁ C₂) (G : CategoryTheory.Functor C₂ C₃) : (W.map F).IsInvertedBy G ↔ W.IsInvertedBy (F.comp G)