limits-colimits

Umiejętność wspierająca pracę nad zadaniami z granic i kogranic w teorii kategorii. Zawiera algorytm decyzyjny do identyfikacji typów granic (produkt, korektor, pullback, obiekt terminalny), weryfikacji własności uniwersalnej oraz obliczania granic konkretnie w kategorii Set. Integruje się z Lean 4 i narzędziami do obliczeń symbolicznych, umożliwiając zarówno formalne dowody, jak i praktyczne przykłady.

1. Zainstaluj umiejętność w katalogu .claude/skills/math/category-theory/ swojego projektu Claude. Upewnij się, że masz dostęp do Lean 4 i biblioteki CategoryTheory.Limits.

2. Zidentyfikuj typ granicy, którą chcesz badać: produkt (limit diagramu dyskretnego), korektor (limit pary równoległych morfizmów), pullback (limit A → C ← B), lub obiekt terminalny (limit diagramu pustego). Dla każdego typu umiejętność sugeruje odpowiednie polecenia Lean 4 z przestrzeni nazw CategoryTheory.Limits.

3. Zweryfikuj własność uniwersalną granicy: sprawdź, czy istnieje stożek z L z projekcjami pi_i: L → D_i, i dla każdego innego stożka z X istnieje unikalny morfizm u: X → L taki, że trójkąty komutują. Użyj IsLimit.lift w Lean 4 do uzyskania tego morfizmu.

4. Jeśli pracujesz w kategorii Set, oblicz granicę konkretnie: produkt to iloczyn kartezjański, korektor to zbiór {x | f(x) = g(x)}, pullback to {(a,b) | f(a) = g(b)}. Do obliczeń symbolicznych uruchom uv run python -m runtime.harness scripts/sympy_compute.py solve "f(a) == g(b)".

5. Dla kogranic zastosuj dualność: koprodukt, korektor, pushout i obiekt początkowy. Pamiętaj, że prawy sprzężony funktor zachowuje granice, a lewy sprzężony zachowuje kogranice — użyj Adjunction.rightAdjointPreservesLimits w Lean 4.

6. Zweryfikuj swoje rozwiązanie poleceniem lake build, które uruchamia kompilator Lean 4 i potwierdza poprawność formalną dowodów.