Structures · Category theory
CategoryTheory.Injective
An object J is injective iff every morphism into J can be obtained by extending a monomorphism.
- Shape
- One type argument · adds factors
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances7
- ModuleCat
- AddCommGrpCat
- Rep
- LightProfinite
- Profinite
- FDRep
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by48
- CategoryTheory.Injective.factorThru
- CategoryTheory.Injective.comp_factorThru
- CategoryTheory.Injective.factors
- CategoryTheory.ShortComplex.Exact.comp_descToInjective
- CategoryTheory.ShortComplex.Exact.descToInjective
- CategoryTheory.Abelian.Ext.eq_zero_of_injective
- CategoryTheory.InjectiveResolution.self
- Module.injective_module_of_injective_object
- CategoryTheory.Injective.hasLiftingProperty_of_isZero
- CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective
- CochainComplex.injective_opcycles
- CategoryTheory.Injective.factorThru.congr_simp
- CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.exists_d_comp_eq_d
- CategoryTheory.Injective.comp_factorThru_assoc
- CategoryTheory.ShortComplex.ShortExact.splittingOfInjective
- DerivedCategory.to_singleFunctor_obj_eq_zero_of_injective
- CochainComplex.isKInjective_of_injective_aux
- CategoryTheory.Retract.injective
- CochainComplex.isKInjective_of_injective
- postcomp_extClass_surjective_of_projective_X₂
- CochainComplex.quasiIso_iff_of_injective
- CategoryTheory.InjectiveResolution.self_ι
- CategoryTheory.preservesHomology_preadditiveYonedaObj_of_injective
- CategoryTheory.ShortComplex.Exact.comp_descToInjective_assoc
- ModuleCat.ulift_injective_of_injective
- CategoryTheory.ShortComplex.Exact.descToInjective.congr_simp
- CategoryTheory.instHasInjectiveDimensionLTOfNatNatOfInjective
- CategoryTheory.Injective.injective_of_adjoint
- CochainComplex.instIsKInjectiveExtendNatIntEmbeddingUpNatOfInjectiveX
- HomotopyCategory.Plus.instIsIsoAppOfInjectiveXIntAsHomologicalComplexUpHomotopicObjPlus
- CategoryTheory.Functor.isZero_rightDerived_obj_injective_succ
- CategoryTheory.Injective.instHasLiftingPropertyOfMono
- CategoryTheory.Injective.instPiObj
- HomologicalComplex.instInjectiveXExtend
- CategoryTheory.InjectiveResolution.instIsIsoToRightDerivedZero'Self
- CategoryTheory.InjectiveResolution.self_cocomplex
- CategoryTheory.Injective.instProjectiveUnopOfOpposite
- HomologicalComplex.instInjectiveXObjSingle
- CategoryTheory.Injective.instBiproduct
- CategoryTheory.Injective.instProd
- HomotopyCategory.Plus.instInjectiveXIntAsHomologicalComplexUpHomotopicObjPlusObjPlusQuotientOfCochainComplexPlus
- CategoryTheory.Sheaf.instSubsingletonHHAddNatOfNat
- CategoryTheory.Injective.instProjectiveOppositeOp
- CategoryTheory.Functor.injective_obj
- CategoryTheory.preservesFiniteColimits_preadditiveYonedaObj_of_injective
- CategoryTheory.instIsIsoAppToRightDerivedZeroOfInjective
- CategoryTheory.Abelian.Ext.subsingleton_of_injective
- CategoryTheory.Injective.instBiprod
Ancestors0
No ancestors.