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} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : MorphismProperty C) (F : 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} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P Q : MorphismProperty C) (F : 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} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] (W : MorphismProperty C₁) (F : Functor C₁ C₂) (hF : W.IsInvertedBy F) (G : Functor C₂ C₃) : W.IsInvertedBy (F.comp G)

theorem CategoryTheory.MorphismProperty.IsInvertedBy.of_comp_of_reflectsIsomorphisms {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {W : MorphismProperty C} {F : Functor C D} {E : Type u_1} [Category.{v_1, u_1} E] (G : Functor D E) [G.ReflectsIsomorphisms] (h : W.IsInvertedBy (F.comp G)) : W.IsInvertedBy F

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

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

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

theorem CategoryTheory.MorphismProperty.IsInvertedBy.unop {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {W : MorphismProperty C} {L : 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} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {E₁ : Type u_3} {E₂ : Type u_4} [Category.{v_3, u_3} E₁] [Category.{v_4, u_4} E₂] {F₁ : Functor C₁ E₁} {F₂ : 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) → Category.{v, u} (C j)] [(j : J) → Category.{v', u'} (D j)] (W : (j : J) → MorphismProperty (C j)) (F : (j : J) → Functor (C j) (D j)) (hF : ∀ (j : J), (W j).IsInvertedBy (F j)) : (MorphismProperty.pi W).IsInvertedBy (Functor.pi F)

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

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

Equations

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

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

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

@[instance_reducible]

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

Equations

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

@[simp]

theorem CategoryTheory.MorphismProperty.FunctorsInverting.id_hom {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {W : MorphismProperty C} (F : W.FunctorsInverting D) : (CategoryStruct.id F).hom = CategoryStruct.id F.obj

@[simp]

theorem CategoryTheory.MorphismProperty.FunctorsInverting.comp_hom {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {W : MorphismProperty C} {F₁ F₂ F₃ : W.FunctorsInverting D} (f : F₁ ⟶ F₂) (g : F₂ ⟶ F₃) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

theorem CategoryTheory.MorphismProperty.FunctorsInverting.comp_hom_assoc {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {W : MorphismProperty C} {F₁ F₂ F₃ : W.FunctorsInverting D} (f : F₁ ⟶ F₂) (g : F₂ ⟶ F₃) {Z : Functor C D} (h : F₃.obj ⟶ Z) : CategoryStruct.comp (CategoryStruct.comp f g).hom h = CategoryStruct.comp f.hom (CategoryStruct.comp g.hom h)

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

theorem CategoryTheory.MorphismProperty.FunctorsInverting.hom_ext_iff {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {W : MorphismProperty C} {F₁ F₂ : W.FunctorsInverting D} {α β : F₁ ⟶ F₂} : α = β ↔ α.hom.app = β.hom.app

def CategoryTheory.MorphismProperty.FunctorsInverting.mk {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {D : Type u_1} [Category.{v_1, u_1} D] (F : 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} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (W : MorphismProperty C) {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) : W.IsInvertedBy F₁ ↔ W.IsInvertedBy F₂

@[simp]

theorem CategoryTheory.MorphismProperty.IsInvertedBy.isoClosure_iff {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (W : MorphismProperty C) (F : 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} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] (W : MorphismProperty C₁) (F : Functor C₁ C₂) (G : Functor C₂ C₃) [G.ReflectsIsomorphisms] : W.IsInvertedBy (F.comp G) ↔ W.IsInvertedBy F

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

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

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

theorem CategoryTheory.MorphismProperty.isInvertedBy_isomorphisms {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor C D) : (isomorphisms C).IsInvertedBy F