Basic

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

Statistics

Metric	Count
Definitions injectivePresentationOfMap, mapInjectivePresentation, injectivePresentationOfMapInjectivePresentation, d, factorThru, instSyzygies, syzygies, under, ι, InjectivePresentation, J, f, isInjective	13
Theorems injective_of_map_injective, map_injective, of_adjunction, of_equivalence, presentation, enoughInjectives_iff, map_injective_iff, injective_of_map_injective, enoughInjectives, comp_factorThru, comp_factorThru_assoc, enoughInjectives_of_enoughProjectives_op, enoughProjectives_of_enoughInjectives_op, exists_presentation, injective_iff_preservesEpimorphisms_yoneda_obj, injective_iff_projective_op, injective_of_adjoint, injective_under, instBiprod, instBiproduct, instEnoughInjectivesOppositeOfEnoughProjectives, instEnoughProjectivesOppositeOfEnoughInjectives, instOfNonempty, instOppositeOpOfProjective, instPiObj, instProd, instProjectiveOppositeOp, instProjectiveUnopOfOpposite, instUnopOfProjectiveOpposite, isZero_under, iso_iff, of_iso, projective_iff_injective_op, zero_injective, ι_mono, injective, mono, injective	38
Total	51

CategoryTheory

Definitions

Name	Category	Theorems
InjectivePresentation 📖	CompData	1 math math: EnoughInjectives.presentation
isInjective 📖	CompOp	—

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
injectivePresentationOfMap 📖	CompOp	—
mapInjectivePresentation 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective_of_map_injective 📖	mathematical	—	CategoryTheory.Injective	—	CategoryTheory.Injective.factors CategoryTheory.Functor.map_mono CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimitsOfSize0.preservesFiniteLimits rightAdjoint_preservesLimits instIsIsoAppCounitOfFullOfFaithful CategoryTheory.Functor.map_injective CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_isIso CategoryTheory.Functor.map_inv inv_counit_map unit_naturality_assoc right_triangle_components CategoryTheory.Category.comp_id
map_injective 📖	mathematical	—	CategoryTheory.Injective CategoryTheory.Functor.obj	—	CategoryTheory.Injective.factors CategoryTheory.Functor.map_mono unit_naturality_assoc CategoryTheory.Functor.map_comp right_triangle_components CategoryTheory.Category.comp_id

CategoryTheory.EnoughInjectives

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_adjunction 📖	mathematical	—	CategoryTheory.EnoughInjectives	—	presentation
of_equivalence 📖	mathematical	—	CategoryTheory.EnoughInjectives	—	of_adjunction CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.reflectsMonomorphisms_of_reflectsLimitsOfShape CategoryTheory.Limits.ReflectsFiniteLimits.reflects CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimits CategoryTheory.Limits.fullyFaithful_reflectsLimits CategoryTheory.Equivalence.full_functor CategoryTheory.Equivalence.faithful_functor
presentation 📖	mathematical	—	CategoryTheory.InjectivePresentation	—	—

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
injectivePresentationOfMapInjectivePresentation 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
enoughInjectives_iff 📖	mathematical	—	CategoryTheory.EnoughInjectives	—	CategoryTheory.EnoughInjectives.of_adjunction CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence isEquivalence_functor CategoryTheory.reflectsMonomorphisms_of_reflectsLimitsOfShape CategoryTheory.Limits.ReflectsFiniteLimits.reflects CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimits CategoryTheory.Limits.fullyFaithful_reflectsLimits full_functor faithful_functor
map_injective_iff 📖	mathematical	—	CategoryTheory.Injective CategoryTheory.Functor.obj functor	—	CategoryTheory.Adjunction.injective_of_map_injective full_inverse faithful_inverse CategoryTheory.Adjunction.map_injective CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence isEquivalence_functor

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective_of_map_injective 📖	mathematical	—	CategoryTheory.Injective	—	CategoryTheory.Injective.factors map_mono map_injective map_comp map_preimage

CategoryTheory.Injective

Definitions

Name	Category	Theorems
d 📖	CompOp	2 math math: CategoryTheory.InjectiveResolution.ofCocomplex_d_0_1, CategoryTheory.exact_f_d
factorThru 📖	CompOp	2 math math: comp_factorThru_assoc, comp_factorThru
instSyzygies 📖	CompOp	—
syzygies 📖	CompOp	1 math math: CategoryTheory.exact_f_d
under 📖	CompOp	6 math math: ι_mono, injective_under, isZero_under, CategoryTheory.InjectiveResolution.ofCocomplex_d_0_1, CochainComplex.cm5b.I_d, CochainComplex.cm5b.I_X
ι 📖	CompOp	5 math math: ι_mono, CategoryTheory.InjectiveResolution.of_def, CategoryTheory.InjectiveResolution.ofCocomplex_d_0_1, CochainComplex.cm5b.i_f_comp, CochainComplex.cm5b.i_f_comp_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_factorThru 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct factorThru	—	factors
comp_factorThru_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct factorThru	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_factorThru
enoughInjectives_of_enoughProjectives_op 📖	mathematical	—	CategoryTheory.EnoughInjectives	—	instUnopOfProjectiveOpposite CategoryTheory.Projective.projective_over CategoryTheory.unop_mono_of_epi CategoryTheory.Projective.π_epi
enoughProjectives_of_enoughInjectives_op 📖	mathematical	—	CategoryTheory.EnoughProjectives	—	instProjectiveUnopOfOpposite injective_under CategoryTheory.unop_epi_of_mono ι_mono
exists_presentation 📖	mathematical	—	CategoryTheory.Limits.IsZero CategoryTheory.InjectivePresentation.J	—	CategoryTheory.Limits.IsZero.injective CategoryTheory.instMonoId CategoryTheory.EnoughInjectives.presentation
injective_iff_preservesEpimorphisms_yoneda_obj 📖	mathematical	—	CategoryTheory.Injective CategoryTheory.Functor.PreservesEpimorphisms Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda	—	injective_iff_projective_op CategoryTheory.Projective.projective_iff_preservesEpimorphisms_coyoneda_obj CategoryTheory.Functor.preservesEpimorphisms.iso_iff
injective_iff_projective_op 📖	mathematical	—	CategoryTheory.Injective CategoryTheory.Projective Opposite CategoryTheory.Category.opposite Opposite.op	—	instProjectiveOppositeOp instUnopOfProjectiveOpposite
injective_of_adjoint 📖	mathematical	—	CategoryTheory.Injective CategoryTheory.Functor.obj	—	CategoryTheory.Functor.map_mono Equiv.injective factorThru.congr_simp CategoryTheory.Adjunction.homEquiv_counit CategoryTheory.Adjunction.homEquiv_unit CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.Adjunction.counit_naturality CategoryTheory.Adjunction.left_triangle_components_assoc comp_factorThru
injective_under 📖	mathematical	—	CategoryTheory.Injective under	—	CategoryTheory.InjectivePresentation.injective exists_presentation
instBiprod 📖	mathematical	—	CategoryTheory.Injective CategoryTheory.Limits.biprod	—	CategoryTheory.Limits.biprod.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.biprod.lift_fst comp_factorThru CategoryTheory.Limits.biprod.lift_snd
instBiproduct 📖	mathematical	CategoryTheory.Injective	CategoryTheory.Limits.biproduct	—	CategoryTheory.Limits.biproduct.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.biproduct.lift_π comp_factorThru
instEnoughInjectivesOppositeOfEnoughProjectives 📖	mathematical	—	CategoryTheory.EnoughInjectives Opposite CategoryTheory.Category.opposite	—	instOppositeOpOfProjective CategoryTheory.Projective.projective_over CategoryTheory.op_mono_of_epi CategoryTheory.Projective.π_epi
instEnoughProjectivesOppositeOfEnoughInjectives 📖	mathematical	—	CategoryTheory.EnoughProjectives Opposite CategoryTheory.Category.opposite	—	instProjectiveOppositeOp injective_under CategoryTheory.op_epi_of_mono ι_mono
instOfNonempty 📖	mathematical	—	CategoryTheory.Injective CategoryTheory.types	—	CategoryTheory.types_ext CategoryTheory.mono_iff_injective
instOppositeOpOfProjective 📖	mathematical	—	CategoryTheory.Injective Opposite CategoryTheory.Category.opposite Opposite.op	—	CategoryTheory.unop_epi_of_mono CategoryTheory.Projective.factorThru_comp
instPiObj 📖	mathematical	CategoryTheory.Injective	CategoryTheory.Limits.piObj	—	CategoryTheory.Limits.Pi.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π comp_factorThru
instProd 📖	mathematical	—	CategoryTheory.Injective CategoryTheory.Limits.prod	—	CategoryTheory.Limits.prod.comp_lift comp_factorThru CategoryTheory.Limits.prod.hom_ext CategoryTheory.Limits.prod.lift_fst CategoryTheory.Limits.prod.lift_snd
instProjectiveOppositeOp 📖	mathematical	—	CategoryTheory.Projective Opposite CategoryTheory.Category.opposite Opposite.op	—	CategoryTheory.unop_mono_of_epi comp_factorThru
instProjectiveUnopOfOpposite 📖	mathematical	—	CategoryTheory.Projective	—	CategoryTheory.op_mono_of_epi comp_factorThru
instUnopOfProjectiveOpposite 📖	mathematical	—	CategoryTheory.Injective	—	CategoryTheory.op_epi_of_mono CategoryTheory.Projective.factorThru_comp
isZero_under 📖	mathematical	CategoryTheory.Limits.IsZero	under	—	exists_presentation
iso_iff 📖	mathematical	—	CategoryTheory.Injective	—	of_iso
of_iso 📖	mathematical	—	CategoryTheory.Injective	—	factors CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
projective_iff_injective_op 📖	mathematical	—	CategoryTheory.Projective CategoryTheory.Injective Opposite CategoryTheory.Category.opposite Opposite.op	—	instOppositeOpOfProjective instProjectiveUnopOfOpposite
zero_injective 📖	mathematical	—	CategoryTheory.Injective CategoryTheory.Limits.HasZeroObject.zero'	—	CategoryTheory.Limits.IsZero.injective CategoryTheory.Limits.isZero_zero
ι_mono 📖	mathematical	—	CategoryTheory.Mono under ι	—	CategoryTheory.InjectivePresentation.mono exists_presentation

CategoryTheory.Injective.Type

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
enoughInjectives 📖	mathematical	—	CategoryTheory.EnoughInjectives CategoryTheory.types	—	CategoryTheory.Injective.instOfNonempty CategoryTheory.mono_iff_injective WithBot.coe_injective

CategoryTheory.InjectivePresentation

Definitions

Name	Category	Theorems
J 📖	CompOp	3 math math: injective, mono, CategoryTheory.Injective.exists_presentation
f 📖	CompOp	1 math math: mono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective 📖	mathematical	—	CategoryTheory.Injective J	—	—
mono 📖	mathematical	—	CategoryTheory.Mono J f	—	—

CategoryTheory.Limits.IsZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective 📖	mathematical	CategoryTheory.Limits.IsZero	CategoryTheory.Injective	—	eq_of_tgt

---

← Back to Index