Category Theory in Mathlib: Functors, Limits, and Sheaves

-- The Category type class
#check CategoryTheory.Category
-- Category C : has Hom sets, identity morphisms, composition, and the usual axioms

-- Small categories (morphisms form a type in the same universe)
#check CategoryTheory.SmallCategory
-- SmallCategory C : Category C where ∀ X Y : C, Hom X Y : Type*

-- Isomorphisms
#check CategoryTheory.Iso
-- Iso X Y : a pair of inverse morphisms X ⟶ Y and Y ⟶ X

-- The opposite category
#check CategoryTheory.Opposite   -- Cᵒᵖ : reverses all morphisms

-- Functors
#check CategoryTheory.Functor
-- Functor C D : maps objects and morphisms, preserving id and composition
-- Written F : C ⥤ D in Lean

-- Functor composition
#check CategoryTheory.Functor.comp   -- F ⋙ G

-- Natural transformations
#check CategoryTheory.NatTrans
-- NatTrans F G : a family of morphisms αX : F X ⟶ G X, natural in X
-- Written α : F ⟶ G (using Lean's morphism notation)

-- Natural isomorphisms
#check CategoryTheory.NatIso    -- F ≅ G : a natural transformation with iso components

-- The functor category
-- [C, D] or C ⥤ D : category whose objects are functors and morphisms are nat. trans.

-- The Yoneda embedding
#check CategoryTheory.yoneda
-- yoneda : C ⥤ (Cᵒᵖ ⥤ Type*)
-- yoneda.obj X = Hom(–, X) : the representable presheaf

-- Yoneda lemma: natural transformations from Hom(–, X) to F correspond to F X
#check CategoryTheory.yonedaEquiv
-- yonedaEquiv : (yoneda.obj X ⟶ F) ≃ F.obj X

-- Fully faithful embedding
#check CategoryTheory.yoneda.isFaithful
#check CategoryTheory.yoneda.isFull

-- Adjunction F ⊣ G : F is left adjoint to G
#check CategoryTheory.Adjunction
-- Adjunction F G : has unit η : 𝟭 C ⟶ G ⋙ F and counit ε : F ⋙ G ⟶ 𝟭 D

-- Unit and counit
#check CategoryTheory.Adjunction.unit
#check CategoryTheory.Adjunction.counit

-- Left adjoints preserve colimits, right adjoints preserve limits
#check CategoryTheory.IsLeftAdjoint   -- type class: has a right adjoint
#check CategoryTheory.IsRightAdjoint  -- type class: has a left adjoint

-- Monads (from adjunctions)
#check CategoryTheory.Monad   -- A monad T on C with μ : T² ⟹ T, η : Id ⟹ T

-- Limits
#check CategoryTheory.Limits.IsLimit
-- IsLimit c : c is a limit cone for a diagram F

#check CategoryTheory.Limits.IsColimit
-- IsColimit c : c is a colimit cocone for F

-- Existence (via HasLimit and HasColimit type classes)
#check CategoryTheory.Limits.HasLimit
#check CategoryTheory.Limits.HasColimit

-- Specific limits
#check CategoryTheory.Limits.prod         -- Binary product X × Y
#check CategoryTheory.Limits.equalizer    -- Equalizer of f, g : X ⟶ Y
#check CategoryTheory.Limits.pullback     -- Pullback / fiber product
#check CategoryTheory.Limits.terminal     -- Terminal object

-- Specific colimits
#check CategoryTheory.Limits.coprod       -- Binary coproduct X ⊔ Y
#check CategoryTheory.Limits.coequalizer  -- Coequalizer
#check CategoryTheory.Limits.pushout      -- Pushout
#check CategoryTheory.Limits.initial      -- Initial object

-- Monoidal category: has a tensor product ⊗ and unit object
#check CategoryTheory.MonoidalCategory
-- MonoidalCategory C : C has ⊗, 𝟙, and coherence isomorphisms

-- Braided monoidal category
#check CategoryTheory.BraidedCategory

-- Symmetric monoidal category
#check CategoryTheory.SymmetricCategory

-- Cartesian closed category
#check CategoryTheory.MonoidalClosed

-- Examples:
-- ModuleCat R is symmetric monoidal under ⊗[R]
-- Finset is monoidal under disjoint union

-- Abelian category
#check CategoryTheory.Abelian
-- An additive category with all finite limits/colimits, where every
-- mono is a kernel and every epi is a cokernel

-- Preadditive categories
#check CategoryTheory.Preadditive  -- Hom sets are abelian groups

-- Additive categories
#check CategoryTheory.Additive     -- Has finite biproducts

-- The category of R-modules is abelian
-- instance : Abelian (ModuleCat R) := ...

-- Exact sequences
#check CategoryTheory.ShortComplex.ShortExact
-- 0 ⟶ A ⟶ B ⟶ C ⟶ 0 is a short exact sequence

-- Chain complexes
#check ChainComplex
-- ChainComplex C ℕ : sequence ... A₂ → A₁ → A₀ with d² = 0

-- Homology of a complex
#check HomologicalComplex.homology

-- Derived functors live in the derived category (partially formalized)

-- Ext groups via projective resolutions
-- (see Mathlib.Algebra.Category.ModuleCat.Ext)

-- A Grothendieck topology on a category C
#check CategoryTheory.GrothendieckTopology
-- Assigns to each object X a collection of covering sieves

-- Sieves
#check CategoryTheory.Sieve   -- A sieve on X : a subfunctor of Hom(–, X)

-- Presheaves and sheaves
#check CategoryTheory.Presheaf    -- A functor Cᵒᵖ ⥤ D
#check CategoryTheory.Sheaf       -- A presheaf satisfying the sheaf condition

-- Sheafification
#check CategoryTheory.GrothendieckTopology.sheafify

-- The category of sheaves (a topos when D = Type*)
#check CategoryTheory.Sheaf.category

-- Triangulated category
-- (partially formalized, see Mathlib.CategoryTheory.Triangulated)
#check CategoryTheory.Pretriangulated.Triangle
-- A distinguished triangle X ⟶ Y ⟶ Z ⟶ X[1]

-- The homotopy category of an additive category
#check HomotopyCategory