Formal mathematics laboratory

Lumenary.LimitsColimits

Limits and colimits

Back to the formal lab Open the lessonMathlib

Formal library

equalizer_universaltheoremProved here from basic factsQuot.sound

equalizer_universalLean 4Proved here from basic factsFormally verified

/-- **The equaliser in the category of types** of `f g : X → Y` is the subtype
`{x // f x = g x}` with its inclusion. Universal property: every `h : W → X` with
`f ∘ h = g ∘ h` factors through the inclusion by exactly one map `u`, namely
`u w = ⟨h w, _⟩`; uniqueness holds because an element of a subtype is determined by its value. -/
theorem equalizer_universal (f g : X → Y) (h : W → X) (hh : f ∘ h = g ∘ h) :
    ∃! u : W → {x : X // f x = g x}, Subtype.val ∘ u = h := by
  refine ⟨fun w => ⟨h w, congr_fun hh w⟩, rfl, ?_⟩
  intro u hu
  funext w
  exact Subtype.ext (congr_fun hu w)

Axioms used: Quot.soundformal/Lumenary/LimitsColimits.leanTry it in the Lean web editor

homEqualizerEquivdefDefinitionQuot.sound

homEqualizerEquivLean 4Formally verified

/-- **Maps into an equaliser are maps that equalise.** For every type `W`, maps
`W → {x // f x = g x}` correspond bijectively to maps `h : W → X` with `f ∘ h = g ∘ h`. In other
words the hom functor `Hom(W, −)` sends the equaliser of `f, g` to the equaliser of
`f ∘ −, g ∘ −` — the simplest case of "hom functors preserve limits". -/
def homEqualizerEquiv (f g : X → Y) (W : Type u) :
    (W → {x : X // f x = g x}) ≃ {h : W → X // f ∘ h = g ∘ h} where
  toFun u := ⟨Subtype.val ∘ u, funext fun w => (u w).2⟩
  invFun h := fun w => ⟨h.1 w, congr_fun h.2 w⟩
  left_inv _ := rfl
  right_inv _ := rfl

Axioms used: Quot.soundformal/Lumenary/LimitsColimits.leanTry it in the Lean web editor

pullback_universaltheoremProved here from basic factsQuot.sound

pullback_universalLean 4Proved here from basic factsFormally verified

/-- **The pullback in the category of types** of `f : A → C` and `g : B → C` is the subtype
`{(a, b) // f a = g b}` of `A × B` — the equaliser of `f ∘ fst` and `g ∘ snd`, exactly the
construction "limits from products and equalisers". Universal property: maps `a : W → A`,
`b : W → B` with `f ∘ a = g ∘ b` factor through it by exactly one map, `w ↦ (a w, b w)`. -/
theorem pullback_universal (f : A → C) (g : B → C) (a : W → A) (b : W → B)
    (hab : f ∘ a = g ∘ b) :
    ∃! u : W → {p : A × B // f p.1 = g p.2},
      (fun w => (u w).1.1) = a ∧ (fun w => (u w).1.2) = b := by
  refine ⟨fun w => ⟨(a w, b w), congr_fun hab w⟩, ⟨rfl, rfl⟩, ?_⟩
  rintro u ⟨h₁, h₂⟩
  funext w
  exact Subtype.ext (Prod.ext (congr_fun h₁ w) (congr_fun h₂ w))

Axioms used: Quot.soundformal/Lumenary/LimitsColimits.leanTry it in the Lean web editor

CoeqReldefDefinitionNo axioms

CoeqRelLean 4Formally verified

/-- The relation generating the **coequaliser** of `f g : X → Y`: `f x` is related to `g x`. -/
def CoeqRel (f g : X → Y) : Y → Y → Prop :=
  fun y y' => ∃ x, f x = y ∧ g x = y'

Axioms used: No axiomsformal/Lumenary/LimitsColimits.leanTry it in the Lean web editor

coequalizer_universaltheoremProved here from basic factsQuot.sound

coequalizer_universalLean 4Proved here from basic factsFormally verified

/-- **The coequaliser in the category of types** is the quotient `Quot (CoeqRel f g)` of `Y` by
the equivalence relation generated by `f x ~ g x`, with the quotient map. Universal property:
every `h : Y → Z` with `h ∘ f = h ∘ g` factors through the quotient by exactly one map
(`Quot.lift`); uniqueness holds because every element of the quotient is a class `[y]`. Colimits
of types glue, limits of types carve out. -/
theorem coequalizer_universal (f g : X → Y) (h : Y → Z) (hh : h ∘ f = h ∘ g) :
    ∃! u : Quot (CoeqRel f g) → Z, u ∘ Quot.mk _ = h := by
  refine ⟨Quot.lift h ?_, rfl, ?_⟩
  · rintro _ _ ⟨x, rfl, rfl⟩
    exact congr_fun hh x
  · intro u hu
    funext q
    induction q using Quot.ind with
    | mk y => exact congr_fun hu y

Axioms used: Quot.soundformal/Lumenary/LimitsColimits.leanTry it in the Lean web editor

cone_naturalitytheoremApplies a library theorempropext, Classical.choice, Quot.sound

cone_naturalityLean 4Applies a library theoremFormally verified

/-- **A cone is a natural transformation from a constant functor.** A cone over `F : J ⥤ C` has
an apex and legs `c.π.app j : apex ⟶ F j`; naturality of `c.π : const apex ⟶ F` at
`f : j ⟶ j'` says exactly that the legs are compatible: `F f ∘ π_j = π_j'`. This is Mathlib's
`Cone.w`. -/
theorem cone_naturality {J : Type*} [Category J] {C : Type*} [Category C] {F : J ⥤ C}
    (c : Cone F) {j j' : J} (f : j ⟶ j') : c.π.app j ≫ F.map f = c.π.app j' :=
  c.w f