category_theory.limits.preserves.shapes.equalizers

source

def category_theory.limits.is_limit_map_cone_fork_equiv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} {f g : X ⟶ Y} {h : Z ⟶ X} (w : h ≫ f = h ≫ g) :

category_theory.limits.is_limit (G.map_cone (category_theory.limits.fork.of_ι h w)) ≃ category_theory.limits.is_limit (category_theory.limits.fork.of_ι (G.map h) _)

The map of a fork is a limit iff the fork consisting of the mapped morphisms is a limit. This essentially lets us commute fork.of_ι with functor.map_cone.

Equations

source

def category_theory.limits.is_limit_fork_map_of_is_limit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} {f g : X ⟶ Y} {h : Z ⟶ X} (w : h ≫ f = h ≫ g) [category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f g) G] (l : category_theory.limits.is_limit (category_theory.limits.fork.of_ι h w)) :

category_theory.limits.is_limit (category_theory.limits.fork.of_ι (G.map h) _)

The property of preserving equalizers expressed in terms of forks.

Equations

category_theory.limits.is_limit_fork_map_of_is_limit G w l = ⇑(category_theory.limits.is_limit_map_cone_fork_equiv G w) (category_theory.limits.preserves_limit.preserves l)

source

def category_theory.limits.is_limit_of_is_limit_fork_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} {f g : X ⟶ Y} {h : Z ⟶ X} (w : h ≫ f = h ≫ g) [category_theory.limits.reflects_limit (category_theory.limits.parallel_pair f g) G] (l : category_theory.limits.is_limit (category_theory.limits.fork.of_ι (G.map h) _)) :

category_theory.limits.is_limit (category_theory.limits.fork.of_ι h w)

The property of reflecting equalizers expressed in terms of forks.

Equations

category_theory.limits.is_limit_of_is_limit_fork_map G w l = category_theory.limits.reflects_limit.reflects (⇑((category_theory.limits.is_limit_map_cone_fork_equiv G w).symm) l)

source

noncomputable def category_theory.limits.is_limit_of_has_equalizer_of_preserves_limit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_equalizer f g] [category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f g) G] :

category_theory.limits.is_limit (category_theory.limits.fork.of_ι (G.map (category_theory.limits.equalizer.ι f g)) _)

If G preserves equalizers and C has them, then the fork constructed of the mapped morphisms of a fork is a limit.

Equations

category_theory.limits.is_limit_of_has_equalizer_of_preserves_limit G f g = category_theory.limits.is_limit_fork_map_of_is_limit G _ (category_theory.limits.equalizer_is_equalizer f g)

source

noncomputable def category_theory.limits.preserves_equalizer.of_iso_comparison {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_equalizer f g] [category_theory.limits.has_equalizer (G.map f) (G.map g)] [i : category_theory.is_iso (category_theory.limits.equalizer_comparison f g G)] :

category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f g) G

If the equalizer comparison map for G at (f,g) is an isomorphism, then G preserves the equalizer of (f,g).

Equations

category_theory.limits.preserves_equalizer.of_iso_comparison G f g = category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.equalizer_is_equalizer f g) (⇑((category_theory.limits.is_limit_map_cone_fork_equiv G _).symm) (category_theory.limits.limit.is_limit (category_theory.limits.parallel_pair (G.map f) (G.map g))).of_point_iso)

source

noncomputable def category_theory.limits.preserves_equalizer.iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_equalizer f g] [category_theory.limits.has_equalizer (G.map f) (G.map g)] [category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f g) G] :

G.obj (category_theory.limits.equalizer f g) ≅ category_theory.limits.equalizer (G.map f) (G.map g)

If G preserves the equalizer of (f,g), then the equalizer comparison map for G at (f,g) is an isomorphism.

Equations

category_theory.limits.preserves_equalizer.iso G f g = (category_theory.limits.is_limit_of_has_equalizer_of_preserves_limit G f g).cone_point_unique_up_to_iso (category_theory.limits.limit.is_limit (category_theory.limits.parallel_pair (G.map f) (G.map g)))

source

@[simp]

theorem category_theory.limits.preserves_equalizer.iso_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_equalizer f g] [category_theory.limits.has_equalizer (G.map f) (G.map g)] [category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f g) G] :

(category_theory.limits.preserves_equalizer.iso G f g).hom = category_theory.limits.equalizer_comparison f g G

source

@[protected, instance]

def category_theory.limits.equalizer_comparison.category_theory.is_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_equalizer f g] [category_theory.limits.has_equalizer (G.map f) (G.map g)] [category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f g) G] :

category_theory.is_iso (category_theory.limits.equalizer_comparison f g G)

source

def category_theory.limits.is_colimit_map_cocone_cofork_equiv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} {f g : X ⟶ Y} {h : Y ⟶ Z} (w : f ≫ h = g ≫ h) :

category_theory.limits.is_colimit (G.map_cocone (category_theory.limits.cofork.of_π h w)) ≃ category_theory.limits.is_colimit (category_theory.limits.cofork.of_π (G.map h) _)

The map of a cofork is a colimit iff the cofork consisting of the mapped morphisms is a colimit. This essentially lets us commute cofork.of_π with functor.map_cocone.

Equations

source

def category_theory.limits.is_colimit_cofork_map_of_is_colimit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} {f g : X ⟶ Y} {h : Y ⟶ Z} (w : f ≫ h = g ≫ h) [category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f g) G] (l : category_theory.limits.is_colimit (category_theory.limits.cofork.of_π h w)) :

category_theory.limits.is_colimit (category_theory.limits.cofork.of_π (G.map h) _)

The property of preserving coequalizers expressed in terms of coforks.

Equations

category_theory.limits.is_colimit_cofork_map_of_is_colimit G w l = ⇑(category_theory.limits.is_colimit_map_cocone_cofork_equiv G w) (category_theory.limits.preserves_colimit.preserves l)

source

def category_theory.limits.is_colimit_of_is_colimit_cofork_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} {f g : X ⟶ Y} {h : Y ⟶ Z} (w : f ≫ h = g ≫ h) [category_theory.limits.reflects_colimit (category_theory.limits.parallel_pair f g) G] (l : category_theory.limits.is_colimit (category_theory.limits.cofork.of_π (G.map h) _)) :

category_theory.limits.is_colimit (category_theory.limits.cofork.of_π h w)

The property of reflecting coequalizers expressed in terms of coforks.

Equations

category_theory.limits.is_colimit_of_is_colimit_cofork_map G w l = category_theory.limits.reflects_colimit.reflects (⇑((category_theory.limits.is_colimit_map_cocone_cofork_equiv G w).symm) l)

source

noncomputable def category_theory.limits.is_colimit_of_has_coequalizer_of_preserves_colimit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_coequalizer f g] [category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f g) G] :

category_theory.limits.is_colimit (category_theory.limits.cofork.of_π (G.map (category_theory.limits.coequalizer.π f g)) _)

If G preserves coequalizers and C has them, then the cofork constructed of the mapped morphisms of a cofork is a colimit.

Equations

category_theory.limits.is_colimit_of_has_coequalizer_of_preserves_colimit G f g = category_theory.limits.is_colimit_cofork_map_of_is_colimit G _ (category_theory.limits.coequalizer_is_coequalizer f g)

source

noncomputable def category_theory.limits.of_iso_comparison {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_coequalizer f g] [category_theory.limits.has_coequalizer (G.map f) (G.map g)] [i : category_theory.is_iso (category_theory.limits.coequalizer_comparison f g G)] :

category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f g) G

If the coequalizer comparison map for G at (f,g) is an isomorphism, then G preserves the coequalizer of (f,g).

Equations

category_theory.limits.of_iso_comparison G f g = category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (category_theory.limits.coequalizer_is_coequalizer f g) (⇑((category_theory.limits.is_colimit_map_cocone_cofork_equiv G _).symm) (category_theory.limits.colimit.is_colimit (category_theory.limits.parallel_pair (G.map f) (G.map g))).of_point_iso)

source

noncomputable def category_theory.limits.preserves_coequalizer.iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_coequalizer f g] [category_theory.limits.has_coequalizer (G.map f) (G.map g)] [category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f g) G] :

category_theory.limits.coequalizer (G.map f) (G.map g) ≅ G.obj (category_theory.limits.coequalizer f g)

If G preserves the coequalizer of (f,g), then the coequalizer comparison map for G at (f,g) is an isomorphism.

Equations

category_theory.limits.preserves_coequalizer.iso G f g = (category_theory.limits.colimit.is_colimit (category_theory.limits.parallel_pair (G.map f) (G.map g))).cocone_point_unique_up_to_iso (category_theory.limits.is_colimit_of_has_coequalizer_of_preserves_colimit G f g)

source

@[simp]

theorem category_theory.limits.preserves_coequalizer.iso_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_coequalizer f g] [category_theory.limits.has_coequalizer (G.map f) (G.map g)] [category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f g) G] :

(category_theory.limits.preserves_coequalizer.iso G f g).hom = category_theory.limits.coequalizer_comparison f g G

source

@[protected, instance]

def category_theory.limits.coequalizer_comparison.category_theory.is_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_coequalizer f g] [category_theory.limits.has_coequalizer (G.map f) (G.map g)] [category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f g) G] :

category_theory.is_iso (category_theory.limits.coequalizer_comparison f g G)

source

@[protected, instance]

def category_theory.limits.map_π_epi {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_coequalizer f g] [category_theory.limits.has_coequalizer (G.map f) (G.map g)] [category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f g) G] :

category_theory.epi (G.map (category_theory.limits.coequalizer.π f g))

source

theorem category_theory.limits.map_π_preserves_coequalizer_inv_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_coequalizer f g] [category_theory.limits.has_coequalizer (G.map f) (G.map g)] [category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f g) G] {X' : D} (f' : category_theory.limits.coequalizer (G.map f) (G.map g) ⟶ X') :

G.map (category_theory.limits.coequalizer.π f g) ≫ (category_theory.limits.preserves_coequalizer.iso G f g).inv ≫ f' = category_theory.limits.coequalizer.π (G.map f) (G.map g) ≫ f'

source

theorem category_theory.limits.map_π_preserves_coequalizer_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_coequalizer f g] [category_theory.limits.has_coequalizer (G.map f) (G.map g)] [category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f g) G] :

G.map (category_theory.limits.coequalizer.π f g) ≫ (category_theory.limits.preserves_coequalizer.iso G f g).inv = category_theory.limits.coequalizer.π (G.map f) (G.map g)

source

theorem category_theory.limits.map_π_preserves_coequalizer_inv_desc_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_coequalizer f g] [category_theory.limits.has_coequalizer (G.map f) (G.map g)] [category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f g) G] {W : D} (k : G.obj Y ⟶ W) (wk : G.map f ≫ k = G.map g ≫ k) {X' : D} (f' : W ⟶ X') :

G.map (category_theory.limits.coequalizer.π f g) ≫ (category_theory.limits.preserves_coequalizer.iso G f g).inv ≫ category_theory.limits.coequalizer.desc k wk ≫ f' = k ≫ f'

source

theorem category_theory.limits.map_π_preserves_coequalizer_inv_desc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_coequalizer f g] [category_theory.limits.has_coequalizer (G.map f) (G.map g)] [category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f g) G] {W : D} (k : G.obj Y ⟶ W) (wk : G.map f ≫ k = G.map g ≫ k) :

G.map (category_theory.limits.coequalizer.π f g) ≫ (category_theory.limits.preserves_coequalizer.iso G f g).inv ≫ category_theory.limits.coequalizer.desc k wk = k

source

theorem category_theory.limits.map_π_preserves_coequalizer_inv_colim_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_coequalizer f g] [category_theory.limits.has_coequalizer (G.map f) (G.map g)] [category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f g) G] {X' Y' : D} (f' g' : X' ⟶ Y') [category_theory.limits.has_coequalizer f' g'] (p : G.obj X ⟶ X') (q : G.obj Y ⟶ Y') (wf : G.map f ≫ q = p ≫ f') (wg : G.map g ≫ q = p ≫ g') :

G.map (category_theory.limits.coequalizer.π f g) ≫ (category_theory.limits.preserves_coequalizer.iso G f g).inv ≫ category_theory.limits.colim_map (category_theory.limits.parallel_pair_hom (G.map f) (G.map g) f' g' p q wf wg) = q ≫ category_theory.limits.coequalizer.π f' g'

source

theorem category_theory.limits.map_π_preserves_coequalizer_inv_colim_map_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_coequalizer f g] [category_theory.limits.has_coequalizer (G.map f) (G.map g)] [category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f g) G] {X' Y' : D} (f' g' : X' ⟶ Y') [category_theory.limits.has_coequalizer f' g'] (p : G.obj X ⟶ X') (q : G.obj Y ⟶ Y') (wf : G.map f ≫ q = p ≫ f') (wg : G.map g ≫ q = p ≫ g') {X'_1 : D} (f'_1 : category_theory.limits.colimit (category_theory.limits.parallel_pair f' g') ⟶ X'_1) :

G.map (category_theory.limits.coequalizer.π f g) ≫ (category_theory.limits.preserves_coequalizer.iso G f g).inv ≫ category_theory.limits.colim_map (category_theory.limits.parallel_pair_hom (G.map f) (G.map g) f' g' p q wf wg) ≫ f'_1 = q ≫ category_theory.limits.coequalizer.π f' g' ≫ f'_1

source

theorem category_theory.limits.map_π_preserves_coequalizer_inv_colim_map_desc_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_coequalizer f g] [category_theory.limits.has_coequalizer (G.map f) (G.map g)] [category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f g) G] {X' Y' : D} (f' g' : X' ⟶ Y') [category_theory.limits.has_coequalizer f' g'] (p : G.obj X ⟶ X') (q : G.obj Y ⟶ Y') (wf : G.map f ≫ q = p ≫ f') (wg : G.map g ≫ q = p ≫ g') {Z' : D} (h : Y' ⟶ Z') (wh : f' ≫ h = g' ≫ h) {X'_1 : D} (f'_1 : Z' ⟶ X'_1) :

G.map (category_theory.limits.coequalizer.π f g) ≫ (category_theory.limits.preserves_coequalizer.iso G f g).inv ≫ category_theory.limits.colim_map (category_theory.limits.parallel_pair_hom (G.map f) (G.map g) f' g' p q wf wg) ≫ category_theory.limits.coequalizer.desc h wh ≫ f'_1 = q ≫ h ≫ f'_1

source

theorem category_theory.limits.map_π_preserves_coequalizer_inv_colim_map_desc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_coequalizer f g] [category_theory.limits.has_coequalizer (G.map f) (G.map g)] [category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f g) G] {X' Y' : D} (f' g' : X' ⟶ Y') [category_theory.limits.has_coequalizer f' g'] (p : G.obj X ⟶ X') (q : G.obj Y ⟶ Y') (wf : G.map f ≫ q = p ≫ f') (wg : G.map g ≫ q = p ≫ g') {Z' : D} (h : Y' ⟶ Z') (wh : f' ≫ h = g' ≫ h) :

G.map (category_theory.limits.coequalizer.π f g) ≫ (category_theory.limits.preserves_coequalizer.iso G f g).inv ≫ category_theory.limits.colim_map (category_theory.limits.parallel_pair_hom (G.map f) (G.map g) f' g' p q wf wg) ≫ category_theory.limits.coequalizer.desc h wh = q ≫ h

source

@[protected, instance]

noncomputable def category_theory.limits.preserves_split_coequalizers {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y : C} (f g : X ⟶ Y) [category_theory.has_split_coequalizer f g] :

category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f g) G

Any functor preserves coequalizers of split pairs.

Equations

category_theory.limits.preserves_split_coequalizers G f g = category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (category_theory.has_split_coequalizer.is_split_coequalizer f g).is_coequalizer (⇑((category_theory.limits.is_colimit_map_cocone_cofork_equiv G _).symm) ((category_theory.has_split_coequalizer.is_split_coequalizer f g).map G).is_coequalizer)

mathlib3 documentation

Preserving (co)equalizers #