Weak equalizers

These are weak limits for diagrams of shape WalkingParallelPair.

@[reducible, inline]

abbrev CategoryTheory.Limits.HasWeakEqualizer {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} (f g : X ⟶ Y) : Prop

Two parallel morphisms f and g have a weak equalizer if the diagram parallelPair f g has a weak limit.

Equations

• CategoryTheory.Limits.HasWeakEqualizer f g = CategoryTheory.Limits.HasWeakLimit (CategoryTheory.Limits.parallelPair f g)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.weakEqualizer {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} (f g : X ⟶ Y) [HasWeakEqualizer f g] : C

If a weak equalizer of f and g exists, we can access an arbitrary choice of such by saying weakEqualizer f g.

Equations

• CategoryTheory.Limits.weakEqualizer f g = CategoryTheory.Limits.weakLimit (CategoryTheory.Limits.parallelPair f g)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.weakEqualizer.ι {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} (f g : X ⟶ Y) [HasWeakEqualizer f g] : weakEqualizer f g ⟶ X

If a weak equalizer of f and g exists, we can access the morphism weakEqualizer f g ⟶ X by saying weakEqualizer.ι f g.

Equations

• CategoryTheory.Limits.weakEqualizer.ι f g = CategoryTheory.Limits.weakLimit.π (CategoryTheory.Limits.parallelPair f g) CategoryTheory.Limits.WalkingParallelPair.zero

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.weakEqualizer.fork {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} (f g : X ⟶ Y) [HasWeakEqualizer f g] : Fork f g

A weak equalizer cone for a parallel pair f and g

Equations

• CategoryTheory.Limits.weakEqualizer.fork f g = CategoryTheory.Limits.weakLimit.cone (CategoryTheory.Limits.parallelPair f g)

@[simp]

theorem CategoryTheory.Limits.weakEqualizer.fork_ι {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} (f g : X ⟶ Y) [HasWeakEqualizer f g] : (fork f g).ι = ι f g

@[simp]

theorem CategoryTheory.Limits.weakEqualizer.fork_π_app_zero {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} (f g : X ⟶ Y) [HasWeakEqualizer f g] : (fork f g).π.app WalkingParallelPair.zero = ι f g

theorem CategoryTheory.Limits.weakEqualizer.condition {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} (f g : X ⟶ Y) [HasWeakEqualizer f g] : CategoryStruct.comp (ι f g) f = CategoryStruct.comp (ι f g) g

theorem CategoryTheory.Limits.weakEqualizer.condition_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} (f g : X ⟶ Y) [HasWeakEqualizer f g] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (ι f g) (CategoryStruct.comp f h) = CategoryStruct.comp (ι f g) (CategoryStruct.comp g h)

noncomputable def CategoryTheory.Limits.weakEqualizerIsWeakEqualizer {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} (f g : X ⟶ Y) [HasWeakEqualizer f g] : IsWeakLimit (Fork.ofι (weakEqualizer.ι f g) ⋯)

The weak equalizer built from weakEqualizer.ι f g is weakly limiting.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.weakEqualizer.lift {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} {f g : X ⟶ Y} [HasWeakEqualizer f g] {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = CategoryStruct.comp k g) : W ⟶ weakEqualizer f g

A morphism k : W ⟶ X satisfying k ≫ f = k ≫ g factors through the weak equalizer of f and g via weakEqualizer.lift : W ⟶ weakEqualizer f g.

Equations

• CategoryTheory.Limits.weakEqualizer.lift k h = CategoryTheory.Limits.weakLimit.lift (CategoryTheory.Limits.parallelPair f g) (CategoryTheory.Limits.Fork.ofι k h)

theorem CategoryTheory.Limits.weakEqualizer.lift_ι {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} {f g : X ⟶ Y} [HasWeakEqualizer f g] {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = CategoryStruct.comp k g) : CategoryStruct.comp (lift k h) (ι f g) = k

theorem CategoryTheory.Limits.weakEqualizer.lift_ι_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} {f g : X ⟶ Y} [HasWeakEqualizer f g] {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = CategoryStruct.comp k g) {Z : C} (h✝ : X ⟶ Z) : CategoryStruct.comp (lift k h) (CategoryStruct.comp (ι f g) h✝) = CategoryStruct.comp k h✝

noncomputable def CategoryTheory.Limits.weakEqualizer.lift' {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} {f g : X ⟶ Y} [HasWeakEqualizer f g] {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = CategoryStruct.comp k g) : { l : W ⟶ weakEqualizer f g // CategoryStruct.comp l (ι f g) = k }

A morphism k : W ⟶ X satisfying k ≫ f = k ≫ g induces a morphism l : W ⟶ weakEqualizer f g satisfying l ≫ weakEqualizer.ι f g = k.

Equations

• CategoryTheory.Limits.weakEqualizer.lift' k h = ⟨CategoryTheory.Limits.weakEqualizer.lift k h, ⋯⟩

@[reducible, inline]

abbrev CategoryTheory.Limits.HasWeakEqualizers (C : Type u_1) [Category.{v_1, u_1} C] : Prop

A category HasWeakEqualizers if it has all weak limits of shape WalkingParallelPair, i.e. if it has a weak equalizer for every parallel pair of morphisms.

Equations

• CategoryTheory.Limits.HasWeakEqualizers C = CategoryTheory.Limits.HasWeakLimitsOfShape CategoryTheory.Limits.WalkingParallelPair C

@[instance 100]

instance CategoryTheory.Limits.HasWeakEqualizersOfHasEqualizers (C : Type u_1) [Category.{v_1, u_1} C] [HasEqualizers C] : HasWeakEqualizers C

A category with equalizers has weak equalizers.

theorem CategoryTheory.Limits.hasWeakEqualizers_of_hasWeakLimit_parallelPair (C : Type u_1) [Category.{v_1, u_1} C] [∀ {X Y : C} {f g : X ⟶ Y}, HasWeakLimit (parallelPair f g)] : HasWeakEqualizers C

If C has all weak limits of diagrams parallelPair f g, then it has all weak equalizers

def CategoryTheory.Limits.Fork.IsWeakLimit.mk {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} {f g : X ⟶ Y} (t : Fork f g) (lift : (s : Fork f g) → s.pt ⟶ t.pt) (fac : ∀ (s : Fork f g), CategoryStruct.comp (lift s) t.ι = s.ι) : IsWeakLimit t

This is a slightly more convenient method to verify that a fork is a weak limit cone. It only asks for a proof of facts that carry any mathematical content

Equations

• CategoryTheory.Limits.Fork.IsWeakLimit.mk t lift fac = { lift := lift, fac := ⋯ }

@[simp]

theorem CategoryTheory.Limits.Fork.IsWeakLimit.mk_lift {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} {f g : X ⟶ Y} (t : Fork f g) (lift : (s : Fork f g) → s.pt ⟶ t.pt) (fac : ∀ (s : Fork f g), CategoryStruct.comp (lift s) t.ι = s.ι) (s : Fork f g) : (mk t lift fac).lift s = lift s

def CategoryTheory.Limits.Fork.IsWeakLimit.mk' {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} {f g : X ⟶ Y} (t : Fork f g) (create : (s : Fork f g) → { l : s.pt ⟶ t.pt // CategoryStruct.comp l t.ι = s.ι }) : IsWeakLimit t

This is another convenient method to verify that a fork is a weak limit cone. It only asks for a proof of facts that carry any mathematical content, and allows access to the same s for all parts.

Equations

• CategoryTheory.Limits.Fork.IsWeakLimit.mk' t create = CategoryTheory.Limits.Fork.IsWeakLimit.mk t (fun (s : CategoryTheory.Limits.Fork f g) => ↑(create s)) ⋯