Basic

📁 Source: Mathlib/CategoryTheory/Preadditive/Projective/Basic.lean

Statistics

Metric	Count
Definitions mapProjectivePresentation, projectivePresentationOfMapProjectivePresentation, d, factorThru, over, syzygies, π, ProjectivePresentation, f, p, isProjective	11
Theorems map_projective, projective_of_map_projective, presentation, enoughProjectives_iff, map_projective_iff, projective_of_map_projective, projective, enoughProjectives, factorThru_comp, factorThru_comp_assoc, inst, instBiprod, instBiproduct, instCoprod, instSigmaObj, instSyzygies, iso_iff, of_iso, projective_iff_preservesEpimorphisms_coyoneda_obj, projective_over, zero_projective, π_epi, epi, projective	24
Total	35

CategoryTheory

Definitions

Name	Category	Theorems
ProjectivePresentation 📖	CompData	1 math math: EnoughProjectives.presentation
isProjective 📖	CompOp	—

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
mapProjectivePresentation 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_projective 📖	mathematical	—	CategoryTheory.Projective CategoryTheory.Functor.obj	—	CategoryTheory.Projective.factors CategoryTheory.Functor.map_epi CategoryTheory.Category.assoc counit_naturality CategoryTheory.Functor.map_comp left_triangle_components_assoc
projective_of_map_projective 📖	mathematical	—	CategoryTheory.Projective	—	CategoryTheory.Projective.factors CategoryTheory.Functor.map_epi CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits CategoryTheory.Limits.PreservesColimitsOfSize0.preservesFiniteColimits leftAdjoint_preservesColimits instIsIsoAppUnitOfFullOfFaithful CategoryTheory.Functor.map_injective CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_isIso CategoryTheory.Functor.map_inv inv_map_unit counit_naturality_assoc left_triangle_components_assoc

CategoryTheory.EnoughProjectives

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
presentation 📖	mathematical	—	CategoryTheory.ProjectivePresentation	—	—

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
projectivePresentationOfMapProjectivePresentation 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
enoughProjectives_iff 📖	mathematical	—	CategoryTheory.EnoughProjectives	—	CategoryTheory.EnoughProjectives.presentation
map_projective_iff 📖	mathematical	—	CategoryTheory.Projective CategoryTheory.Functor.obj functor	—	CategoryTheory.Adjunction.projective_of_map_projective full_functor faithful_functor CategoryTheory.Adjunction.map_projective CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence isEquivalence_inverse

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
projective_of_map_projective 📖	mathematical	—	CategoryTheory.Projective	—	CategoryTheory.Projective.factors map_epi map_injective map_comp map_preimage

CategoryTheory.Limits.IsZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
projective 📖	mathematical	CategoryTheory.Limits.IsZero	CategoryTheory.Projective	—	eq_of_src

CategoryTheory.Projective

Definitions

Name	Category	Theorems
d 📖	CompOp	2 math math: CategoryTheory.ProjectiveResolution.ofComplex_d_1_0, CategoryTheory.exact_d_f
factorThru 📖	CompOp	2 math math: factorThru_comp_assoc, factorThru_comp
over 📖	CompOp	3 math math: CategoryTheory.ProjectiveResolution.ofComplex_d_1_0, projective_over, π_epi
syzygies 📖	CompOp	2 math math: instSyzygies, CategoryTheory.exact_d_f
π 📖	CompOp	3 math math: CategoryTheory.ProjectiveResolution.ofComplex_d_1_0, CategoryTheory.ProjectiveResolution.of_def, π_epi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
factorThru_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct factorThru	—	factors
factorThru_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct factorThru	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' factorThru_comp
inst 📖	mathematical	—	CategoryTheory.Projective CategoryTheory.types	—	CategoryTheory.surjective_of_epi
instBiprod 📖	mathematical	—	CategoryTheory.Projective CategoryTheory.Limits.biprod	—	CategoryTheory.Limits.biprod.hom_ext' CategoryTheory.Limits.biprod.inl_desc_assoc factorThru_comp CategoryTheory.Limits.biprod.inr_desc_assoc
instBiproduct 📖	mathematical	CategoryTheory.Projective	CategoryTheory.Limits.biproduct	—	CategoryTheory.Limits.biproduct.hom_ext' CategoryTheory.Limits.biproduct.ι_desc_assoc factorThru_comp
instCoprod 📖	mathematical	—	CategoryTheory.Projective CategoryTheory.Limits.coprod	—	CategoryTheory.Limits.coprod.desc_comp factorThru_comp CategoryTheory.Limits.coprod.hom_ext CategoryTheory.Limits.colimit.ι_desc
instSigmaObj 📖	mathematical	CategoryTheory.Projective	CategoryTheory.Limits.sigmaObj	—	CategoryTheory.Limits.Sigma.hom_ext CategoryTheory.Limits.colimit.ι_desc_assoc factorThru_comp
instSyzygies 📖	mathematical	—	CategoryTheory.Projective syzygies	—	projective_over
iso_iff 📖	mathematical	—	CategoryTheory.Projective	—	of_iso
of_iso 📖	mathematical	—	CategoryTheory.Projective	—	factors CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc
projective_iff_preservesEpimorphisms_coyoneda_obj 📖	mathematical	—	CategoryTheory.Projective CategoryTheory.Functor.PreservesEpimorphisms CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda Opposite.op	—	CategoryTheory.epi_iff_surjective factorThru_comp CategoryTheory.Functor.map_epi
projective_over 📖	mathematical	—	CategoryTheory.Projective over	—	CategoryTheory.ProjectivePresentation.projective CategoryTheory.EnoughProjectives.presentation
zero_projective 📖	mathematical	—	CategoryTheory.Projective CategoryTheory.Limits.HasZeroObject.zero'	—	CategoryTheory.Limits.IsZero.projective CategoryTheory.Limits.isZero_zero
π_epi 📖	mathematical	—	CategoryTheory.Epi over π	—	CategoryTheory.ProjectivePresentation.epi CategoryTheory.EnoughProjectives.presentation

CategoryTheory.Projective.Type

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
enoughProjectives 📖	mathematical	—	CategoryTheory.EnoughProjectives CategoryTheory.types	—	CategoryTheory.Projective.inst CategoryTheory.instEpiId

CategoryTheory.ProjectivePresentation

Definitions

Name	Category	Theorems
f 📖	CompOp	1 math math: epi
p 📖	CompOp	2 math math: projective, epi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi 📖	mathematical	—	CategoryTheory.Epi p f	—	—
projective 📖	mathematical	—	CategoryTheory.Projective p	—	—

---

← Back to Index