buildLimit — Mathlib

English

Given the appropriate product and equalizer cones, one can assemble a cone for F which is limiting if those cones are limiting.

Русский

Даны соответствующие конусы произведений и равноселителя, можно построить конус для F, который будет пределом при условии, что исходные конусы являются пределами.

LaTeX

$$$\text{buildLimit}(s,t,hs,ht,i) \in \mathrm{Cone}(F)$ and if\; t,i,s \text{ are limiting, then } \text{buildLimit}(s,t,hs,ht,i) \text{ is limit.}$$$

Lean4

/-- (Implementation) Given the appropriate product and equalizer cones, build the cone for `F` which is
limiting if the given cones are also.
-/
@[simps]
def buildLimit (hs : ∀ f : Σ p : J × J, p.1 ⟶ p.2, s ≫ c₂.π.app ⟨f⟩ = c₁.π.app ⟨f.1.1⟩ ≫ F.map f.2)
    (ht : ∀ f : Σ p : J × J, p.1 ⟶ p.2, t ≫ c₂.π.app ⟨f⟩ = c₁.π.app ⟨f.1.2⟩) (i : Fork s t) : Cone F
    where
  pt := i.pt
  π :=
    { app := fun _ => i.ι ≫ c₁.π.app ⟨_⟩
      naturality := fun j₁ j₂ f => by
        dsimp
        rw [Category.id_comp, Category.assoc, ← hs ⟨⟨_, _⟩, f⟩, i.condition_assoc, ht] }

Похожие утверждения