Theorems · Definition · category theory

CategoryTheory.Projective.over

{C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.EnoughProjectives C] → C → C

Projective.over X provides an arbitrarily chosen projective object equipped with an epimorphism Projective.π : Projective.over X ⟶ X.

Defined in: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Cited by: 4 results in Mathlib
Foundations: Depth 3 from the axioms · uses Classical.choice
Assumes: CategoryTheory.Category CategoryTheory.EnoughProjectives

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
Nonempty.someproof · cited by 340
CategoryTheory.EnoughProjectivesstatement and proof · cited by 13
CategoryTheory.ProjectivePresentation.pproof · cited by 1

Cited by7

Results whose statement or proof uses this declaration.

CategoryTheory.Projective.πstatement · cited by 7
CategoryTheory.Projective.syzygiesproof · cited by 3
CategoryTheory.ProjectiveResolution.ofComplexproof · cited by 3
CategoryTheory.Functor.preservesEpimorphisms_of_adjunction_of_preservesProjectiveObjectsproof · cited by 0
CategoryTheory.ProjectiveResolution.ofComplex_d_1_0statement and proof · cited by 0
CategoryTheory.ProjectiveResolution.ofComplex_exactAt_succproof · cited by 0
CategoryTheory.Injective.enoughInjectives_of_enoughProjectives_opproof · cited by 0