SmallShiftedHom

📁 Source: Mathlib/CategoryTheory/Localization/SmallShiftedHom.lean

Statistics

Metric	Count
Definitions HasSmallLocalizedShiftedHom, shift, SmallShiftedHom, chgUniv, comp, equiv, mk, mk₀, mk₀Inv, postcompEquiv, precompEquiv, shift, smallShiftedHomMap	13
Theorems equiv_shift, comp_assoc, comp_mk₀_id, equiv_apply, equiv_chgUniv, equiv_comp, equiv_mk, equiv_mk₀, equiv_mk₀Inv, equiv_shift, equiv_shift', mk₀Inv_comp_mk₀, mk₀_comp_mk₀Inv, mk₀_id_comp, postcompEquiv_apply, postcompEquiv_symm_apply, precompEquiv_apply, precompEquiv_symm_apply, hasSmallLocalizedHom_of_hasSmallLocalizedShiftedHom₀, hasSmallLocalizedShiftedHom_iff, hasSmallLocalizedShiftedHom_iff_source, hasSmallLocalizedShiftedHom_iff_target, instHasSmallLocalizedHomObjShiftFunctor, instHasSmallLocalizedHomObjShiftFunctor_1, instHasSmallLocalizedHomObjShiftFunctor_2, instHasSmallLocalizedHomObjShiftFunctor_3, equiv_smallShiftedHomMap, smallShiftedHomMap_comp, smallShiftedHomMap_mk, smallShiftedHomMap_mk₀	30
Total	43

CategoryTheory.Localization

Definitions

Name	Category	Theorems
HasSmallLocalizedShiftedHom 📖	MathDef	7 math math: CategoryTheory.ShortComplex.ShortExact.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoX₃CochainComplexMapSingleFunctorOfNatX₁, hasSmallLocalizedShiftedHom_iff_target, hasSmallLocalizedShiftedHom_iff_source, CategoryTheory.HasExt.hasSmallLocalizedShiftedHom_of_isLE_of_isGE, CategoryTheory.HasExt.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoOfIsGEOfIsLEOfNat, CategoryTheory.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoObjCochainComplexCompSingleFunctorOfNatOfHasExt, hasSmallLocalizedShiftedHom_iff
SmallShiftedHom 📖	CompOp	19 math math: CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective_apply, SmallShiftedHom.equiv_comp, CochainComplex.HomComplex.CohomologyClass.bijective_toSmallShiftedHom_of_isKProjective, CochainComplex.HomComplex.CohomologyClass.bijective_toSmallShiftedHom_of_isKInjective, CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective_symm_apply, SmallShiftedHom.equiv_mk, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, SmallShiftedHom.equiv_chgUniv, CategoryTheory.LocalizerMorphism.equiv_smallShiftedHomMap, SmallShiftedHom.equiv_shift, SmallShiftedHom.postcompEquiv_symm_apply, SmallShiftedHom.precompEquiv_symm_apply, CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective_symm_apply, SmallShiftedHom.precompEquiv_apply, SmallShiftedHom.equiv_mk₀Inv, SmallShiftedHom.equiv_mk₀, CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective_apply, SmallShiftedHom.equiv_apply, SmallShiftedHom.postcompEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasSmallLocalizedHom_of_hasSmallLocalizedShiftedHom₀ 📖	mathematical	HasSmallLocalizedShiftedHom	HasSmallLocalizedHom	—	hasSmallLocalizedHom_iff_of_isos
hasSmallLocalizedShiftedHom_iff 📖	mathematical	—	HasSmallLocalizedShiftedHom Small Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor	—	small_congr hasSmallLocalizedHom_iff
hasSmallLocalizedShiftedHom_iff_source 📖	mathematical	—	HasSmallLocalizedShiftedHom	—	hasSmallLocalizedHom_iff_source CategoryTheory.MorphismProperty.shift
hasSmallLocalizedShiftedHom_iff_target 📖	mathematical	—	HasSmallLocalizedShiftedHom	—	hasSmallLocalizedHom_iff_target CategoryTheory.MorphismProperty.shift
instHasSmallLocalizedHomObjShiftFunctor 📖	mathematical	HasSmallLocalizedShiftedHom	HasSmallLocalizedHom CategoryTheory.Functor.obj CategoryTheory.shiftFunctor	—	hasSmallLocalizedHom_iff_of_isos
instHasSmallLocalizedHomObjShiftFunctor_1 📖	mathematical	HasSmallLocalizedShiftedHom	HasSmallLocalizedHom CategoryTheory.Functor.obj CategoryTheory.shiftFunctor	—	hasSmallLocalizedHom_iff_of_isos
instHasSmallLocalizedHomObjShiftFunctor_2 📖	mathematical	HasSmallLocalizedShiftedHom	HasSmallLocalizedHom CategoryTheory.Functor.obj CategoryTheory.shiftFunctor	—	hasSmallLocalizedHom_iff_of_isos
instHasSmallLocalizedHomObjShiftFunctor_3 📖	mathematical	HasSmallLocalizedShiftedHom	HasSmallLocalizedHom CategoryTheory.Functor.obj CategoryTheory.shiftFunctor	—	hasSmallLocalizedHom_iff_of_isos

CategoryTheory.Localization.SmallHom

Definitions

Name	Category	Theorems
shift 📖	CompOp	1 math math: equiv_shift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equiv_shift 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Localization.SmallHom CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike equiv shift CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.CommShift.commShiftIso CategoryTheory.Functor.map CategoryTheory.Iso.inv	—	CategoryTheory.LocalizerMorphism.equiv_smallHomMap

CategoryTheory.Localization.SmallShiftedHom

Definitions

Name	Category	Theorems
chgUniv 📖	CompOp	1 math math: equiv_chgUniv
comp 📖	CompOp	11 math math: equiv_comp, comp_mk₀_id, mk₀_id_comp, comp_assoc, mk₀Inv_comp_mk₀, postcompEquiv_symm_apply, precompEquiv_symm_apply, precompEquiv_apply, CategoryTheory.LocalizerMorphism.smallShiftedHomMap_comp, mk₀_comp_mk₀Inv, postcompEquiv_apply
equiv 📖	CompOp	9 math math: equiv_comp, equiv_mk, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, equiv_chgUniv, CategoryTheory.LocalizerMorphism.equiv_smallShiftedHomMap, equiv_shift, equiv_mk₀Inv, equiv_mk₀, equiv_apply
mk 📖	CompOp	—
mk₀ 📖	CompOp	8 math math: comp_mk₀_id, mk₀_id_comp, mk₀Inv_comp_mk₀, precompEquiv_apply, mk₀_comp_mk₀Inv, equiv_mk₀, CategoryTheory.LocalizerMorphism.smallShiftedHomMap_mk₀, postcompEquiv_apply
mk₀Inv 📖	CompOp	5 math math: mk₀Inv_comp_mk₀, postcompEquiv_symm_apply, precompEquiv_symm_apply, equiv_mk₀Inv, mk₀_comp_mk₀Inv
postcompEquiv 📖	CompOp	2 math math: postcompEquiv_symm_apply, postcompEquiv_apply
precompEquiv 📖	CompOp	2 math math: precompEquiv_symm_apply, precompEquiv_apply
shift 📖	CompOp	2 math math: equiv_shift', equiv_shift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_assoc 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom AddSemigroup.toAdd AddMonoid.toAddSemigroup	comp	—	Equiv.injective CategoryTheory.Functor.q_isLocalization equiv_comp CategoryTheory.ShiftedHom.comp.congr_simp CategoryTheory.ShiftedHom.comp_assoc
comp_mk₀_id 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	comp mk₀ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	Equiv.injective CategoryTheory.Functor.q_isLocalization equiv_comp CategoryTheory.ShiftedHom.comp.congr_simp equiv_mk₀ CategoryTheory.ShiftedHom.mk₀.congr_simp CategoryTheory.Functor.map_id CategoryTheory.ShiftedHom.comp_mk₀_id
equiv_apply 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom	DFunLike.coe Equiv CategoryTheory.Localization.SmallShiftedHom CategoryTheory.ShiftedHom CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike equiv CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.shiftFunctor CategoryTheory.Functor.comp CategoryTheory.Localization.SmallHom CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Localization.SmallHom.equiv CategoryTheory.Iso.hom CategoryTheory.Iso.app CategoryTheory.Functor.CommShift.commShiftIso	—	—
equiv_chgUniv 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom	DFunLike.coe Equiv CategoryTheory.Localization.SmallShiftedHom CategoryTheory.ShiftedHom CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike equiv chgUniv	—	CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor CategoryTheory.Localization.SmallHom.equiv_chgUniv
equiv_comp 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom AddSemigroup.toAdd AddMonoid.toAddSemigroup	DFunLike.coe Equiv CategoryTheory.Localization.SmallShiftedHom CategoryTheory.ShiftedHom CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike equiv comp CategoryTheory.ShiftedHom.comp	—	CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor CategoryTheory.Localization.SmallHom.equiv_comp equiv_shift' CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Category.comp_id CategoryTheory.Functor.map_comp
equiv_mk 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom	DFunLike.coe Equiv CategoryTheory.Localization.SmallShiftedHom CategoryTheory.ShiftedHom CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike equiv CategoryTheory.ShiftedHom.map	—	Equiv.injective CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor Equiv.symm_apply_apply CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_app CategoryTheory.Category.comp_id
equiv_mk₀ 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	DFunLike.coe Equiv CategoryTheory.Localization.SmallShiftedHom CategoryTheory.ShiftedHom CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike equiv mk₀ CategoryTheory.ShiftedHom.mk₀ CategoryTheory.Functor.map	—	CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor CategoryTheory.Functor.map_comp CategoryTheory.Category.comp_id CategoryTheory.Functor.CommShift.commShiftIso_zero CategoryTheory.Functor.CommShift.isoZero_hom_app CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
equiv_mk₀Inv 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	DFunLike.coe Equiv CategoryTheory.Localization.SmallShiftedHom CategoryTheory.ShiftedHom CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike equiv mk₀Inv CategoryTheory.ShiftedHom.mk₀ CategoryTheory.Iso.inv CategoryTheory.Localization.isoOfHom	—	CategoryTheory.MorphismProperty.RespectsIso.precomp CategoryTheory.NatIso.hom_app_isIso CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor CategoryTheory.eq_whisker CategoryTheory.Localization.SmallHom.equiv_mkInv CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.Functor.commShiftIso_zero' CategoryTheory.Functor.CommShift.isoZero'_hom_app CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.Localization.isoOfHom_hom_inv_id_assoc
equiv_shift 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom AddSemigroup.toAdd AddMonoid.toAddSemigroup	DFunLike.coe Equiv CategoryTheory.Localization.SmallShiftedHom CategoryTheory.Functor.obj CategoryTheory.shiftFunctor CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor_2 CategoryTheory.ShiftedHom EquivLike.toFunLike Equiv.instEquivLike equiv shift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.CommShift.commShiftIso CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.shiftFunctorAdd'	—	CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor_2 CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor equiv_shift' CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Category.comp_id CategoryTheory.Functor.map_comp
equiv_shift' 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom AddSemigroup.toAdd AddMonoid.toAddSemigroup	DFunLike.coe Equiv CategoryTheory.Localization.SmallHom CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Localization.SmallHom.equiv shift CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.CommShift.commShiftIso CategoryTheory.Functor.map CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor CategoryTheory.Iso.inv CategoryTheory.shiftFunctorAdd'	—	CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor_3 CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor_2 CategoryTheory.Localization.SmallHom.equiv_comp CategoryTheory.Localization.SmallHom.equiv_shift CategoryTheory.Category.assoc CategoryTheory.Functor.commShiftIso_add' CategoryTheory.Functor.CommShift.isoAdd'_inv_app CategoryTheory.Iso.inv_hom_id_app_assoc CategoryTheory.Iso.hom_inv_id_app CategoryTheory.Category.comp_id
mk₀Inv_comp_mk₀ 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	comp mk₀Inv mk₀ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	Equiv.injective CategoryTheory.Functor.q_isLocalization equiv_comp CategoryTheory.ShiftedHom.comp.congr_simp equiv_mk₀Inv equiv_mk₀ CategoryTheory.ShiftedHom.mk₀_comp_mk₀ CategoryTheory.ShiftedHom.mk₀.congr_simp CategoryTheory.Localization.isoOfHom_inv_hom_id CategoryTheory.Functor.map_id
mk₀_comp_mk₀Inv 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	comp mk₀ mk₀Inv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	Equiv.injective CategoryTheory.Functor.q_isLocalization equiv_comp CategoryTheory.ShiftedHom.comp.congr_simp equiv_mk₀ equiv_mk₀Inv CategoryTheory.ShiftedHom.mk₀_comp_mk₀ CategoryTheory.ShiftedHom.mk₀.congr_simp CategoryTheory.Localization.isoOfHom_hom_inv_id CategoryTheory.Functor.map_id
mk₀_id_comp 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	comp mk₀ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	Equiv.injective CategoryTheory.Functor.q_isLocalization equiv_comp CategoryTheory.ShiftedHom.comp.congr_simp equiv_mk₀ CategoryTheory.ShiftedHom.mk₀.congr_simp CategoryTheory.Functor.map_id CategoryTheory.ShiftedHom.mk₀_id_comp
postcompEquiv_apply 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom	DFunLike.coe Equiv CategoryTheory.Localization.SmallShiftedHom EquivLike.toFunLike Equiv.instEquivLike postcompEquiv comp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass mk₀	—	CategoryTheory.Localization.HasSmallLocalizedHom.small CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor
postcompEquiv_symm_apply 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom	DFunLike.coe Equiv CategoryTheory.Localization.SmallShiftedHom EquivLike.toFunLike Equiv.instEquivLike Equiv.symm postcompEquiv comp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass mk₀Inv	—	CategoryTheory.Localization.HasSmallLocalizedHom.small CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor
precompEquiv_apply 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom	DFunLike.coe Equiv CategoryTheory.Localization.SmallShiftedHom EquivLike.toFunLike Equiv.instEquivLike precompEquiv comp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass mk₀	—	CategoryTheory.Localization.HasSmallLocalizedHom.small CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor
precompEquiv_symm_apply 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom	DFunLike.coe Equiv CategoryTheory.Localization.SmallShiftedHom EquivLike.toFunLike Equiv.instEquivLike Equiv.symm precompEquiv comp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass mk₀Inv	—	CategoryTheory.Localization.HasSmallLocalizedHom.small CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor

CategoryTheory.LocalizerMorphism

Definitions

Name	Category	Theorems
smallShiftedHomMap 📖	CompOp	4 math math: smallShiftedHomMap_mk, equiv_smallShiftedHomMap, smallShiftedHomMap_comp, smallShiftedHomMap_mk₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equiv_smallShiftedHomMap 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom	DFunLike.coe Equiv CategoryTheory.Localization.SmallShiftedHom CategoryTheory.ShiftedHom CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Localization.SmallShiftedHom.equiv smallShiftedHomMap CategoryTheory.ShiftedHom.comp CategoryTheory.Functor.comp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.ShiftedHom.mk₀ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct functor CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.ShiftedHom.map zero_add add_zero	—	CategoryTheory.Localization.hasSmallLocalizedHom_of_hasSmallLocalizedShiftedHom₀ Equiv.injective zero_add add_zero CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_app CategoryTheory.Category.comp_id equiv_smallHomMap' CategoryTheory.NatTrans.app_shift CategoryTheory.NatTrans.CommShift.of_iso_inv CategoryTheory.Functor.commShiftIso_comp_hom_app CategoryTheory.Functor.commShiftIso_comp_inv_app CategoryTheory.Functor.map_comp CategoryTheory.ShiftedHom.comp.congr_simp CategoryTheory.ShiftedHom.comp_mk₀ CategoryTheory.ShiftedHom.mk₀_comp CategoryTheory.Functor.commShiftIso_inv_naturality CategoryTheory.Functor.map_comp_assoc CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
smallShiftedHomMap_comp 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom AddSemigroup.toAdd AddMonoid.toAddSemigroup	smallShiftedHomMap CategoryTheory.Localization.SmallShiftedHom.comp	—	Equiv.injective CategoryTheory.Functor.q_isLocalization zero_add add_zero equiv_smallShiftedHomMap instCommShiftLocalizationHomFunctorIsoFunctorQLocalizedFunctor CategoryTheory.ShiftedHom.comp.congr_simp CategoryTheory.Localization.SmallShiftedHom.equiv_comp CategoryTheory.ShiftedHom.map_comp CategoryTheory.ShiftedHom.comp_assoc CategoryTheory.ShiftedHom.mk₀_comp_mk₀ CategoryTheory.ShiftedHom.mk₀.congr_simp CategoryTheory.Category.assoc CategoryTheory.Iso.map_hom_inv_id_assoc CategoryTheory.Iso.inv_hom_id_app CategoryTheory.ShiftedHom.mk₀_id_comp
smallShiftedHomMap_mk 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom	smallShiftedHomMap CategoryTheory.ShiftedHom.comp CategoryTheory.Functor.obj functor AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.ShiftedHom.mk₀ CategoryTheory.Iso.inv CategoryTheory.ShiftedHom.map CategoryTheory.Iso.hom zero_add add_zero	—	Equiv.injective CategoryTheory.Functor.q_isLocalization zero_add add_zero equiv_smallShiftedHomMap instCommShiftLocalizationHomFunctorIsoFunctorQLocalizedFunctor CategoryTheory.ShiftedHom.comp.congr_simp CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.ShiftedHom.comp_mk₀ CategoryTheory.NatTrans.shift_app CategoryTheory.NatTrans.CommShift.of_iso_inv CategoryTheory.Functor.commShiftIso_comp_inv_app CategoryTheory.Functor.commShiftIso_comp_hom_app CategoryTheory.Iso.hom_inv_id_app_assoc CategoryTheory.ShiftedHom.mk₀_comp CategoryTheory.Functor.commShiftIso_hom_naturality CategoryTheory.Functor.map_comp_assoc CategoryTheory.Iso.hom_inv_id_app CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.NatIso.naturality_2
smallShiftedHomMap_mk₀ 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	smallShiftedHomMap CategoryTheory.Localization.SmallShiftedHom.mk₀ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.Iso.inv CategoryTheory.Functor.map CategoryTheory.Iso.hom	—	add_zero zero_add CategoryTheory.ShiftedHom.comp.congr_simp CategoryTheory.ShiftedHom.map_mk₀ CategoryTheory.ShiftedHom.mk₀_comp_mk₀

---

← Back to Index