Loogle!

Result

Found 124 declarations mentioning CategoryTheory.Projective.

CategoryTheory.Projective 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] (P : C) : Prop
CategoryTheory.Projective.inst 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
(X : Type u) : CategoryTheory.Projective X
CategoryTheory.Limits.IsZero.projective 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (h : CategoryTheory.Limits.IsZero X) : CategoryTheory.Projective X
CategoryTheory.Projective.projective_over 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnoughProjectives C] (X : C) : CategoryTheory.Projective (CategoryTheory.Projective.over X)
CategoryTheory.ProjectivePresentation.projective 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (self : CategoryTheory.ProjectivePresentation X) : CategoryTheory.Projective self.p
CategoryTheory.Projective.of_iso 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {P Q : C} (i : P ≅ Q) : CategoryTheory.Projective P → CategoryTheory.Projective Q
CategoryTheory.Projective.zero_projective 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Projective 0
CategoryTheory.Retract.projective 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract X Y) [p : CategoryTheory.Projective Y] : CategoryTheory.Projective X
CategoryTheory.Projective.iso_iff 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {P Q : C} (i : P ≅ Q) : CategoryTheory.Projective P ↔ CategoryTheory.Projective Q
CategoryTheory.Projective.instSigmaObj 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type v} (g : β → C) [CategoryTheory.Limits.HasCoproduct g] [∀ (b : β), CategoryTheory.Projective (g b)] : CategoryTheory.Projective (∐ g)
CategoryTheory.Projective.instCoprod 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {P Q : C} [CategoryTheory.Limits.HasBinaryCoproduct P Q] [CategoryTheory.Projective P] [CategoryTheory.Projective Q] : CategoryTheory.Projective (P ⨿ Q)
CategoryTheory.ProjectivePresentation.mk 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (p : C) [projective : CategoryTheory.Projective p] (f : p ⟶ X) [epi : CategoryTheory.Epi f] : CategoryTheory.ProjectivePresentation X
CategoryTheory.Projective.instBiproduct 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type v} (g : β → C) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBiproduct g] [∀ (b : β), CategoryTheory.Projective (g b)] : CategoryTheory.Projective (⨁ g)
CategoryTheory.Equivalence.map_projective_iff 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : C ≌ D) (P : C) : CategoryTheory.Projective (F.functor.obj P) ↔ CategoryTheory.Projective P
CategoryTheory.Projective.instBiprod 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {P Q : C} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproduct P Q] [CategoryTheory.Projective P] [CategoryTheory.Projective Q] : CategoryTheory.Projective (P ⊞ Q)
CategoryTheory.Projective.projective_iff_preservesEpimorphisms_coyoneda_obj 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] (P : C) : CategoryTheory.Projective P ↔ (CategoryTheory.coyoneda.obj (Opposite.op P)).PreservesEpimorphisms
CategoryTheory.Projective.instSyzygies 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnoughProjectives C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] : CategoryTheory.Projective (CategoryTheory.Projective.syzygies f)
CategoryTheory.Projective.factorThru 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {P X E : C} [CategoryTheory.Projective P] (f : P ⟶ X) (e : E ⟶ X) [CategoryTheory.Epi e] : P ⟶ E
CategoryTheory.Adjunction.map_projective 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [G.PreservesEpimorphisms] (P : C) (hP : CategoryTheory.Projective P) : CategoryTheory.Projective (F.obj P)
CategoryTheory.Functor.projective_of_map_projective 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] [F.PreservesEpimorphisms] {P : C} (hP : CategoryTheory.Projective (F.obj P)) : CategoryTheory.Projective P
CategoryTheory.Adjunction.projective_of_map_projective 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Full] [F.Faithful] (P : C) (hP : CategoryTheory.Projective (F.obj P)) : CategoryTheory.Projective P
CategoryTheory.Projective.factorThru_comp 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {P X E : C} [CategoryTheory.Projective P] (f : P ⟶ X) (e : E ⟶ X) [CategoryTheory.Epi e] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Projective.factorThru f e) e = f
CategoryTheory.Projective.factors 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {P : C} [self : CategoryTheory.Projective P] {E X : C} (f : P ⟶ X) (e : E ⟶ X) [CategoryTheory.Epi e] : ∃ f', CategoryTheory.CategoryStruct.comp f' e = f
CategoryTheory.Projective.mk 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} (factors : ∀ {E X : C} (f : P ⟶ X) (e : E ⟶ X) [CategoryTheory.Epi e], ∃ f', CategoryTheory.CategoryStruct.comp f' e = f) : CategoryTheory.Projective P
CategoryTheory.Projective.factorThru_comp_assoc 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {P X E : C} [CategoryTheory.Projective P] (f : P ⟶ X) (e : E ⟶ X) [CategoryTheory.Epi e] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Projective.factorThru f e) (CategoryTheory.CategoryStruct.comp e h) = CategoryTheory.CategoryStruct.comp f h
CategoryTheory.Injective.instOppositeOpOfProjective 📋 Mathlib.CategoryTheory.Preadditive.Injective.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : C} [CategoryTheory.Projective P] : CategoryTheory.Injective (Opposite.op P)
CategoryTheory.Injective.instProjectiveOppositeOp 📋 Mathlib.CategoryTheory.Preadditive.Injective.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : C} [CategoryTheory.Injective J] : CategoryTheory.Projective (Opposite.op J)
CategoryTheory.Injective.injective_iff_projective_op 📋 Mathlib.CategoryTheory.Preadditive.Injective.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : C} : CategoryTheory.Injective J ↔ CategoryTheory.Projective (Opposite.op J)
CategoryTheory.Injective.projective_iff_injective_op 📋 Mathlib.CategoryTheory.Preadditive.Injective.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : C} : CategoryTheory.Projective P ↔ CategoryTheory.Injective (Opposite.op P)
CategoryTheory.Injective.instProjectiveUnopOfOpposite 📋 Mathlib.CategoryTheory.Preadditive.Injective.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Cᵒᵖ} [CategoryTheory.Injective J] : CategoryTheory.Projective (Opposite.unop J)
CategoryTheory.Injective.instUnopOfProjectiveOpposite 📋 Mathlib.CategoryTheory.Preadditive.Injective.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : Cᵒᵖ} [CategoryTheory.Projective P] : CategoryTheory.Injective (Opposite.unop P)
CategoryTheory.ShortComplex.Exact.liftFromProjective 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) {P : C} (f : P ⟶ S.X₂) [CategoryTheory.Projective P] (hf : CategoryTheory.CategoryStruct.comp f S.g = 0) : P ⟶ S.X₁
CategoryTheory.ShortComplex.Exact.liftFromProjective_comp 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) {P : C} (f : P ⟶ S.X₂) [CategoryTheory.Projective P] (hf : CategoryTheory.CategoryStruct.comp f S.g = 0) : CategoryTheory.CategoryStruct.comp (hS.liftFromProjective f hf) S.f = f
CategoryTheory.ShortComplex.Exact.liftFromProjective_comp_assoc 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) {P : C} (f : P ⟶ S.X₂) [CategoryTheory.Projective P] (hf : CategoryTheory.CategoryStruct.comp f S.g = 0) {Z : C} (h : S.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (hS.liftFromProjective f hf) (CategoryTheory.CategoryStruct.comp S.f h) = CategoryTheory.CategoryStruct.comp f h
CategoryTheory.ShortComplex.ShortExact.splittingOfProjective 📋 Mathlib.Algebra.Homology.ShortComplex.ShortExact
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) [CategoryTheory.Projective S.X₃] [CategoryTheory.Balanced C] : S.Splitting
ModuleCat.projective_of_categoryTheory_projective 📋 Mathlib.Algebra.Category.ModuleCat.Projective
{R : Type u} [Ring R] (P : ModuleCat R) [Module.Projective R ↑P] : CategoryTheory.Projective P
ModuleCat.projective_of_free 📋 Mathlib.Algebra.Category.ModuleCat.Projective
{R : Type u} [Ring R] {M : ModuleCat R} {ι : Type w} (b : Module.Basis ι R ↑M) : CategoryTheory.Projective M
ModuleCat.projective_of_module_projective 📋 Mathlib.Algebra.Category.ModuleCat.Projective
{R : Type u} [Ring R] (P : ModuleCat R) [Small.{v, u} R] [CategoryTheory.Projective P] : Module.Projective R ↑P
IsProjective.iff_projective 📋 Mathlib.Algebra.Category.ModuleCat.Projective
{R : Type u} [Ring R] [Small.{v, u} R] (P : Type v) [AddCommGroup P] [Module R P] : Module.Projective R P ↔ CategoryTheory.Projective (ModuleCat.of R P)
HomologicalComplex.instProjectiveXObjSingle 📋 Mathlib.Algebra.Homology.HomologicalComplexAbelian
{C : Type u_1} {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [DecidableEq ι] (i j : ι) (P : C) [CategoryTheory.Projective P] : CategoryTheory.Projective (((HomologicalComplex.single C c i).obj P).X j)
HomologicalComplex.instProjectiveXExtend 📋 Mathlib.Algebra.Homology.Embedding.Extend
{ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (e : c.Embedding c') (K : HomologicalComplex C c) [∀ (i : ι), CategoryTheory.Projective (K.X i)] (i' : ι') : CategoryTheory.Projective ((K.extend e).X i')
CategoryTheory.Abelian.Ext.subsingleton_of_projective 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (P Y : C) [CategoryTheory.Projective P] (n : ℕ) : Subsingleton (CategoryTheory.Abelian.Ext P Y (n + 1))
CategoryTheory.Abelian.Ext.eq_zero_of_projective 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {P Y : C} {n : ℕ} [CategoryTheory.Projective P] (e : CategoryTheory.Abelian.Ext P Y (n + 1)) : e = 0
CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} [CategoryTheory.Projective P] {K : CochainComplex C ℤ} {i : ℤ} (π : K ⟶ (CochainComplex.singleFunctor C i).obj P) [K.IsStrictlyLE i] [QuasiIsoAt π i] : CategoryTheory.IsSplitEpi π
CategoryTheory.Abelian.Ext.one_subsingleton_iff_of_projective 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (X : C) (S : CategoryTheory.ShortComplex C) (S_exact : S.ShortExact) (proj : CategoryTheory.Projective S.X₂) : Subsingleton (CategoryTheory.Abelian.Ext S.X₃ X 1) ↔ Function.Surjective ⇑((CategoryTheory.Abelian.Ext.mk₀ S.f).precomp X ⋯)
DerivedCategory.from_singleFunctor_obj_eq_zero_of_projective 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {P : C} [CategoryTheory.Projective P] {L : CochainComplex C ℤ} {i : ℤ} (φ : DerivedCategory.Q.obj ((CochainComplex.singleFunctor C i).obj P) ⟶ DerivedCategory.Q.obj L) (n : ℤ) (hn : n < i) [L.IsStrictlyLE n] : φ = 0
precomp_extClass_surjective_of_projective_X₂ 📋 Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting
{R : Type u} [Ring R] [Small.{v, u} R] (M : ModuleCat R) {S : CategoryTheory.ShortComplex (ModuleCat R)} (h : S.ShortExact) (n : ℕ) [CategoryTheory.Projective S.X₂] : Function.Surjective ⇑(h.extClass.precomp M ⋯)
ModuleCat.instProjectiveObjFree 📋 Mathlib.Algebra.Category.ModuleCat.LeftResolution
(R : Type u) [Ring R] (X : Type u) : CategoryTheory.Projective ((ModuleCat.free R).obj X)
CategoryTheory.instHasProjectiveDimensionLTOfNatNatOfProjective 📋 Mathlib.CategoryTheory.Abelian.Projective.Dimension
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : C) [CategoryTheory.Projective X] : CategoryTheory.HasProjectiveDimensionLT X 1
CategoryTheory.instProjectiveOfHasProjectiveDimensionLTOfNatNat 📋 Mathlib.CategoryTheory.Abelian.Projective.Dimension
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : C) [CategoryTheory.HasProjectiveDimensionLT X 1] : CategoryTheory.Projective X
CategoryTheory.projective_iff_hasProjectiveDimensionLE_zero 📋 Mathlib.CategoryTheory.Abelian.Projective.Dimension
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : C) : CategoryTheory.Projective X ↔ CategoryTheory.HasProjectiveDimensionLE X 0
CategoryTheory.projective_iff_hasProjectiveDimensionLT_one 📋 Mathlib.CategoryTheory.Abelian.Projective.Dimension
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} : CategoryTheory.Projective X ↔ CategoryTheory.HasProjectiveDimensionLT X 1
CategoryTheory.projective_iff_subsingleton_ext_one 📋 Mathlib.CategoryTheory.Abelian.Projective.Dimension
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} [CategoryTheory.HasExt C] : CategoryTheory.Projective X ↔ ∀ ⦃Y : C⦄, Subsingleton (CategoryTheory.Abelian.Ext X Y 1)
CategoryTheory.Projective.projectiveDimension_le_zero 📋 Mathlib.CategoryTheory.Abelian.Projective.Dimension
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : C) [CategoryTheory.Projective X] : CategoryTheory.projectiveDimension X ≤ 0
CategoryTheory.projectiveDimension_eq_zero_iff 📋 Mathlib.CategoryTheory.Abelian.Projective.Dimension
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : C) : CategoryTheory.projectiveDimension X = 0 ↔ CategoryTheory.Projective X ∧ ¬CategoryTheory.Limits.IsZero X
CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iff 📋 Mathlib.CategoryTheory.Abelian.Projective.Dimension
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n : ℕ) (h₂ : CategoryTheory.Projective S.X₂) : CategoryTheory.HasProjectiveDimensionLT S.X₃ (n + 2) ↔ CategoryTheory.HasProjectiveDimensionLT S.X₁ (n + 1)
CategoryTheory.ShortComplex.ShortExact.projectiveDimension_X₃_eq_succ_of_not_projective 📋 Mathlib.CategoryTheory.Abelian.Projective.Dimension
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (p : CategoryTheory.Projective S.X₂) (np : ¬CategoryTheory.Projective S.X₃) : CategoryTheory.projectiveDimension S.X₃ = CategoryTheory.projectiveDimension S.X₁ + 1
ModuleCat.projectiveDimension_eq_zero_of_projective 📋 Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
{R : Type u} [Ring R] (M : ModuleCat R) [Nontrivial ↑M] [CategoryTheory.Projective M] : CategoryTheory.projectiveDimension M = 0
CategoryTheory.Functor.projective_obj 📋 Mathlib.CategoryTheory.Preadditive.Projective.Preserves
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.PreservesProjectiveObjects] (X : C) [CategoryTheory.Projective X] : CategoryTheory.Projective (F.obj X)
CategoryTheory.Functor.projective_obj_of_projective 📋 Mathlib.CategoryTheory.Preadditive.Projective.Preserves
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.PreservesProjectiveObjects] {X : C} (h : CategoryTheory.Projective X) : CategoryTheory.Projective (F.obj X)
CategoryTheory.Functor.PreservesProjectiveObjects.mk 📋 Mathlib.CategoryTheory.Preadditive.Projective.Preserves
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (projective_obj : ∀ {X : C}, CategoryTheory.Projective X → CategoryTheory.Projective (F.obj X)) : F.PreservesProjectiveObjects
CategoryTheory.Functor.PreservesProjectiveObjects.projective_obj 📋 Mathlib.CategoryTheory.Preadditive.Projective.Preserves
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {F : CategoryTheory.Functor C D} [self : F.PreservesProjectiveObjects] {X : C} : CategoryTheory.Projective X → CategoryTheory.Projective (F.obj X)
CochainComplex.isKProjective_of_projective 📋 Mathlib.Algebra.Homology.HomotopyCategory.KProjective
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : CochainComplex C ℤ) (d : ℤ) [K.IsStrictlyLE d] [∀ (n : ℤ), CategoryTheory.Projective (K.X n)] : K.IsKProjective
CochainComplex.instIsKProjectiveExtendNatIntEmbeddingDownNatOfProjectiveX 📋 Mathlib.Algebra.Homology.HomotopyCategory.KProjective
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : ChainComplex C ℕ) [∀ (n : ℕ), CategoryTheory.Projective (K.X n)] : CochainComplex.IsKProjective (HomologicalComplex.extend K ComplexShape.embeddingDownNat)
ChainComplex.quasiIso_iff_of_projective 📋 Mathlib.Algebra.Homology.DerivedCategory.KProjective
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {K L : ChainComplex C ℕ} [∀ (n : ℕ), CategoryTheory.Projective (K.X n)] [∀ (n : ℕ), CategoryTheory.Projective (L.X n)] (f : K ⟶ L) : QuasiIso f ↔ HomologicalComplex.homotopyEquivalences C (ComplexShape.down ℕ) f
CategoryTheory.ProjectiveResolution.self 📋 Mathlib.CategoryTheory.Preadditive.Projective.Resolution
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (Z : C) [CategoryTheory.Projective Z] : CategoryTheory.ProjectiveResolution Z
CategoryTheory.ProjectiveResolution.projective 📋 Mathlib.CategoryTheory.Preadditive.Projective.Resolution
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (self : CategoryTheory.ProjectiveResolution Z) (n : ℕ) : CategoryTheory.Projective (self.complex.X n)
CategoryTheory.ProjectiveResolution.self_complex 📋 Mathlib.CategoryTheory.Preadditive.Projective.Resolution
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (Z : C) [CategoryTheory.Projective Z] : (CategoryTheory.ProjectiveResolution.self Z).complex = (ChainComplex.single₀ C).obj Z
CategoryTheory.ProjectiveResolution.self_π 📋 Mathlib.CategoryTheory.Preadditive.Projective.Resolution
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (Z : C) [CategoryTheory.Projective Z] : (CategoryTheory.ProjectiveResolution.self Z).π = CategoryTheory.CategoryStruct.id ((ChainComplex.single₀ C).obj Z)
CategoryTheory.ProjectiveResolution.mk 📋 Mathlib.CategoryTheory.Preadditive.Projective.Resolution
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (complex : ChainComplex C ℕ) (projective : ∀ (n : ℕ), CategoryTheory.Projective (complex.X n) := by infer_instance) [hasHomology : ∀ (i : ℕ), HomologicalComplex.HasHomology complex i] (π : complex ⟶ (ChainComplex.single₀ C).obj Z) (quasiIso : QuasiIso π := by infer_instance) : CategoryTheory.ProjectiveResolution Z
CategoryTheory.ProjectiveResolution.instProjectiveXNatOfComplex 📋 Mathlib.CategoryTheory.Abelian.Projective.Resolution
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] (Z : C) (n : ℕ) : CategoryTheory.Projective ((CategoryTheory.ProjectiveResolution.ofComplex Z).X n)
CategoryTheory.Functor.isZero_leftDerived_obj_projective_succ 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) (X : C) [CategoryTheory.Projective X] : CategoryTheory.Limits.IsZero ((F.leftDerived (n + 1)).obj X)
CategoryTheory.instIsIsoAppFromLeftDerivedZeroOfProjective 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (X : C) [CategoryTheory.Projective X] : CategoryTheory.IsIso (F.fromLeftDerivedZero.app X)
CategoryTheory.ProjectiveResolution.instIsIsoFromLeftDerivedZero'Self 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (X : C) [CategoryTheory.Projective X] : CategoryTheory.IsIso ((CategoryTheory.ProjectiveResolution.self X).fromLeftDerivedZero' F)
isZero_Ext_succ_of_projective 📋 Mathlib.CategoryTheory.Abelian.Ext
{R : Type u_1} [Ring R] {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear R C] [CategoryTheory.EnoughProjectives C] (X Y : C) [CategoryTheory.Projective X] (n : ℕ) : CategoryTheory.Limits.IsZero (((Ext R C (n + 1)).obj (Opposite.op X)).obj Y)
CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj 📋 Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (P : C) : CategoryTheory.Projective P ↔ (CategoryTheory.preadditiveCoyoneda.obj (Opposite.op P)).PreservesEpimorphisms
CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj 📋 Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (P : C) : CategoryTheory.Projective P ↔ (CategoryTheory.preadditiveCoyonedaObj P).PreservesEpimorphisms
CategoryTheory.preservesFiniteColimits_preadditiveCoyonedaObj_of_projective 📋 Mathlib.CategoryTheory.Abelian.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : C) [hP : CategoryTheory.Projective P] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveCoyonedaObj P)
CategoryTheory.projective_of_preservesFiniteColimits_preadditiveCoyonedaObj 📋 Mathlib.CategoryTheory.Abelian.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : C) [hP : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveCoyonedaObj P)] : CategoryTheory.Projective P
CategoryTheory.preservesHomology_preadditiveCoyonedaObj_of_projective 📋 Mathlib.CategoryTheory.Abelian.Projective.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : C) [hP : CategoryTheory.Projective P] : (CategoryTheory.preadditiveCoyonedaObj P).PreservesHomology
CategoryTheory.Abelian.full_comp_preadditiveCoyonedaObj 📋 Mathlib.CategoryTheory.Abelian.Yoneda
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor D C) [F.Full] {G : C} [CategoryTheory.Projective G] (hG : CategoryTheory.IsSeparator G) (hG₂ : ∀ (X : D), ∃ p, CategoryTheory.Epi p) : (F.comp (CategoryTheory.preadditiveCoyonedaObj G)).Full
CategoryTheory.Abelian.preadditiveCoyonedaObj_map_surjective 📋 Mathlib.CategoryTheory.Abelian.Yoneda
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {G : C} [CategoryTheory.Projective G] (hG : CategoryTheory.IsSeparator G) {X : C} (p : G ⟶ X) [CategoryTheory.Epi p] {Y : C} : Function.Surjective (CategoryTheory.preadditiveCoyonedaObj G).map
CategoryTheory.Abelian.has_projective_separator 📋 Mathlib.CategoryTheory.Generator.Abelian
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.EnoughProjectives C] (G : C) (hG : CategoryTheory.IsCoseparator G) : ∃ G, CategoryTheory.Projective G ∧ CategoryTheory.IsSeparator G
CategoryTheory.ProjectiveResolution.instProjectiveXIntCochainComplex 📋 Mathlib.CategoryTheory.Abelian.Projective.Extend
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] {X : C} (R : CategoryTheory.ProjectiveResolution X) (n : ℤ) : CategoryTheory.Projective (R.cochainComplex.X n)
CategoryTheory.isZero_Tor'_succ_of_projective 📋 Mathlib.CategoryTheory.Monoidal.Tor
(C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (X Y : C) [CategoryTheory.Projective X] (n : ℕ) : CategoryTheory.Limits.IsZero (((CategoryTheory.Tor' C (n + 1)).obj X).obj Y)
CategoryTheory.isZero_Tor_succ_of_projective 📋 Mathlib.CategoryTheory.Monoidal.Tor
(C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (X Y : C) [CategoryTheory.Projective Y] (n : ℕ) : CategoryTheory.Limits.IsZero (((CategoryTheory.Tor C (n + 1)).obj X).obj Y)
CategoryTheory.projective_iff_llp_epimorphisms_of_isZero 📋 Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Z : C} (i : Z ⟶ P) (hZ : CategoryTheory.Limits.IsZero Z) : CategoryTheory.Projective P ↔ (CategoryTheory.MorphismProperty.epimorphisms C).llp i
CategoryTheory.Projective.hasLiftingProperty_of_isZero 📋 Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
{C : Type u} [CategoryTheory.Category.{v, u} C] {Z P X Y : C} (i : Z ⟶ P) (p : X ⟶ Y) [CategoryTheory.Epi p] [CategoryTheory.Projective P] (hZ : CategoryTheory.Limits.IsZero Z) : CategoryTheory.HasLiftingProperty i p
CategoryTheory.Projective.instHasLiftingPropertyOfEpi 📋 Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y P : C} (p : X ⟶ Y) [CategoryTheory.Epi p] [CategoryTheory.Projective P] [CategoryTheory.Limits.HasZeroObject C] (i : 0 ⟶ P) : CategoryTheory.HasLiftingProperty i p
CategoryTheory.projective_iff_llp_epimorphisms_zero 📋 Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (P : C) : CategoryTheory.Projective P ↔ (CategoryTheory.MorphismProperty.epimorphisms C).llp 0
CategoryTheory.regularTopology.isSheafFor_regular_of_projective 📋 Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X : C} (S : CategoryTheory.Presieve X) [S.regular] [CategoryTheory.Projective X] (F : CategoryTheory.Functor Cᵒᵖ (Type u_4)) : CategoryTheory.Presieve.IsSheafFor F S
CategoryTheory.regularTopology.isSheaf_of_projective 📋 Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Preregular C] [∀ (X : C), CategoryTheory.Projective X] : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.regularTopology C) F
CategoryTheory.Presheaf.instHasSheafComposeCoherentTopologyOfProjectiveOfPreservesFiniteProducts 📋 Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (s : CategoryTheory.Functor A B) [CategoryTheory.Preregular C] [CategoryTheory.FinitaryExtensive C] [∀ (X : C), CategoryTheory.Projective X] [CategoryTheory.Limits.PreservesFiniteProducts s] : (CategoryTheory.coherentTopology C).HasSheafCompose s
CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_of_projective 📋 Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] (F : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Preregular C] [CategoryTheory.FinitaryExtensive C] [∀ (X : C), CategoryTheory.Projective X] : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F ↔ CategoryTheory.Limits.PreservesFiniteProducts F
CategoryTheory.Presheaf.isSheaf_iff_extensiveSheaf_of_projective 📋 Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] (F : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Preregular C] [CategoryTheory.FinitaryExtensive C] [∀ (X : C), CategoryTheory.Projective X] : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F ↔ CategoryTheory.Presheaf.IsSheaf (CategoryTheory.extensiveTopology C) F
CategoryTheory.Presheaf.isSheaf_coherent_of_projective_comp 📋 Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] (F : CategoryTheory.Functor Cᵒᵖ A) {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (s : CategoryTheory.Functor A B) [CategoryTheory.Preregular C] [CategoryTheory.FinitaryExtensive C] [∀ (X : C), CategoryTheory.Projective X] [CategoryTheory.Limits.PreservesFiniteProducts s] (hF : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F) : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) (F.comp s)
CategoryTheory.Presheaf.isSheaf_coherent_of_projective_of_comp 📋 Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] (F : CategoryTheory.Functor Cᵒᵖ A) {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (s : CategoryTheory.Functor A B) [CategoryTheory.Preregular C] [CategoryTheory.FinitaryExtensive C] [∀ (X : C), CategoryTheory.Projective X] [CategoryTheory.Limits.ReflectsFiniteProducts s] (hF : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) (F.comp s)) : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F
CategoryTheory.Presheaf.coherentExtensiveEquivalence 📋 Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] [CategoryTheory.Preregular C] [CategoryTheory.FinitaryExtensive C] [∀ (X : C), CategoryTheory.Projective X] : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A ≌ CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) A
CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_obj_obj 📋 Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] [CategoryTheory.Preregular C] [CategoryTheory.FinitaryExtensive C] [∀ (X : C), CategoryTheory.Projective X] (X : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) A) : (CategoryTheory.Presheaf.coherentExtensiveEquivalence.inverse.obj X).obj = X.obj
CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_obj_obj 📋 Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] [CategoryTheory.Preregular C] [CategoryTheory.FinitaryExtensive C] [∀ (X : C), CategoryTheory.Projective X] (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A) : (CategoryTheory.Presheaf.coherentExtensiveEquivalence.functor.obj X).obj = X.obj
CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_map_hom 📋 Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] [CategoryTheory.Preregular C] [CategoryTheory.FinitaryExtensive C] [∀ (X : C), CategoryTheory.Projective X] {X✝ Y✝ : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) A} (f : X✝ ⟶ Y✝) : (CategoryTheory.Presheaf.coherentExtensiveEquivalence.inverse.map f).hom = f.hom
CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_map_hom 📋 Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] [CategoryTheory.Preregular C] [CategoryTheory.FinitaryExtensive C] [∀ (X : C), CategoryTheory.Projective X] {X✝ Y✝ : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A} (f : X✝ ⟶ Y✝) : (CategoryTheory.Presheaf.coherentExtensiveEquivalence.functor.map f).hom = f.hom
CategoryTheory.Presheaf.coherentExtensiveEquivalence_unitIso_hom_app_hom_app 📋 Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] [CategoryTheory.Preregular C] [CategoryTheory.FinitaryExtensive C] [∀ (X : C), CategoryTheory.Projective X] (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A) (X✝ : Cᵒᵖ) : (CategoryTheory.Presheaf.coherentExtensiveEquivalence.unitIso.hom.app X).hom.app X✝ = CategoryTheory.CategoryStruct.id (X.obj.obj X✝)
CategoryTheory.Presheaf.coherentExtensiveEquivalence_unitIso_inv_app_hom_app 📋 Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] [CategoryTheory.Preregular C] [CategoryTheory.FinitaryExtensive C] [∀ (X : C), CategoryTheory.Projective X] (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A) (X✝ : Cᵒᵖ) : (CategoryTheory.Presheaf.coherentExtensiveEquivalence.unitIso.inv.app X).hom.app X✝ = CategoryTheory.CategoryStruct.id (X.obj.obj X✝)
CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso_hom_app_hom_app 📋 Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] [CategoryTheory.Preregular C] [CategoryTheory.FinitaryExtensive C] [∀ (X : C), CategoryTheory.Projective X] (X : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) A) (X✝ : Cᵒᵖ) : (CategoryTheory.Presheaf.coherentExtensiveEquivalence.counitIso.hom.app X).hom.app X✝ = CategoryTheory.CategoryStruct.id (X.obj.obj X✝)
CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso_inv_app_hom_app 📋 Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] [CategoryTheory.Preregular C] [CategoryTheory.FinitaryExtensive C] [∀ (X : C), CategoryTheory.Projective X] (X : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) A) (X✝ : Cᵒᵖ) : (CategoryTheory.Presheaf.coherentExtensiveEquivalence.counitIso.inv.app X).hom.app X✝ = CategoryTheory.CategoryStruct.id (X.obj.obj X✝)
CompHaus.projective_ultrafilter 📋 Mathlib.Topology.Category.CompHaus.Projective
(X : Type u_1) : CategoryTheory.Projective (CompHaus.of (Ultrafilter X))
CompHaus.toStonean 📋 Mathlib.Topology.Category.Stonean.Basic
(X : CompHaus) [CategoryTheory.Projective X] : Stonean
Stonean.instProjective 📋 Mathlib.Topology.Category.Stonean.Basic
(X : Stonean) : CategoryTheory.Projective X
CompHaus.instExtremallyDisconnectedCarrierToTopTrueOfProjective 📋 Mathlib.Topology.Category.Stonean.Basic
(X : CompHaus) [CategoryTheory.Projective X] : ExtremallyDisconnected ↑X.toTop
CompHaus.Gleason 📋 Mathlib.Topology.Category.Stonean.Basic
(X : CompHaus) : CategoryTheory.Projective X ↔ ExtremallyDisconnected ↑X.toTop
Stonean.instProjectiveCompHausCompHaus 📋 Mathlib.Topology.Category.Stonean.Basic
(X : Stonean) : CategoryTheory.Projective (Stonean.toCompHaus.obj X)
CompHaus.toStonean_toTop 📋 Mathlib.Topology.Category.Stonean.Basic
(X : CompHaus) [CategoryTheory.Projective X] : X.toStonean.toTop = X.toTop
Stonean.instProjectiveProfiniteObjToProfinite 📋 Mathlib.Topology.Category.Stonean.Basic
(X : Stonean) : CategoryTheory.Projective (Stonean.toProfinite.obj X)
Profinite.projective_of_extrDisc 📋 Mathlib.Topology.Category.Stonean.Basic
{X : Profinite} (hX : ExtremallyDisconnected ↑X.toTop) : CategoryTheory.Projective X
Rep.free_projective 📋 Mathlib.RepresentationTheory.Rep.Iso
{k : Type u} {G : Type v} [CommRing k] [Monoid G] {α : Type (max w u)} : CategoryTheory.Projective (Rep.free k G α)
Rep.leftRegular_projective 📋 Mathlib.RepresentationTheory.Rep.Iso
{k : Type u} [CommRing k] {G : Type u} [Group G] : CategoryTheory.Projective (Rep.leftRegular k G)
Rep.diagonal_succ_projective 📋 Mathlib.RepresentationTheory.Rep.Iso
{k : Type u} [CommRing k] {G : Type u} [Group G] {n : ℕ} : CategoryTheory.Projective (Rep.diagonal k G (n + 1))
Rep.trivial_projective_of_subsingleton 📋 Mathlib.RepresentationTheory.Rep.Iso
{k : Type u} [CommRing k] {G : Type u} [Group G] [Subsingleton G] : CategoryTheory.Projective (Rep.trivial k G k)
Rep.instProjective 📋 Mathlib.RepresentationTheory.FinGroupCharZero
{k : Type u} [Field k] {G : Type u} [Finite G] [Group G] [NeZero ↑(Nat.card G)] (V : Rep.{u, u, u} k G) : CategoryTheory.Projective V
FDRep.instProjectiveOfNeZeroCastCard 📋 Mathlib.RepresentationTheory.FinGroupCharZero
{k : Type u} [Field k] {G : Type u} [Finite G] [Group G] [NeZero ↑(Nat.card G)] (V : FDRep k G) : CategoryTheory.Projective V
Rep.standardComplex.x_projective 📋 Mathlib.RepresentationTheory.Homological.Resolution
(k : Type u) [CommRing k] (G : Type u) [Group G] (n : ℕ) : CategoryTheory.Projective ((Rep.standardComplex k G).X n)
Rep.isZero_Tor_succ_of_projective 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
{k G : Type u} [CommRing k] [Group G] (X Y : Rep.{u, u, u} k G) [CategoryTheory.Projective Y] (n : ℕ) : CategoryTheory.Limits.IsZero (((Rep.Tor k G (n + 1)).obj X).obj Y)
Profinite.projective_ultrafilter 📋 Mathlib.Topology.Category.Profinite.Projective
(X : Type u) : CategoryTheory.Projective (Profinite.of (Ultrafilter X))

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.
You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c