Preadditive

📁 Source: Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean

Statistics

Metric	Count
Definitions `add`, `add'`, `addCommGroup`, `addCommGroup'`, `homEquiv`, `neg'`, `instPreadditiveLocalization`, `instPreadditiveLocalization'`, `preadditive`, `neg`, `add`	11
Theorems `add'_assoc`, `add'_comm`, `add'_comp`, `add'_comp_assoc`, `add'_eq`, `add'_map`, `add'_zero`, `add_comp`, `add_comp_assoc`, `add_eq`, `add_eq_add`, `comp_add`, `comp_add'`, `comp_add'_assoc`, `comp_add_assoc`, `homEquiv_apply`, `homEquiv_symm_apply`, `map_add`, `neg'_add'_self`, `neg'_eq`, `zero_add'`, `functor_additive`, `functor_additive_iff`, `instAdditiveLocalization'Q'`, `instAdditiveLocalizationQ`, `instHasZeroObjectLocalization`, `instHasZeroObjectLocalization'`, `map_add`, `symm_add`	29
Total	40

CategoryTheory.Localization

Definitions

Name	Category	Theorems
`instPreadditiveLocalization` 📖	CompOp	3 math math: `instAdditiveLocalizationQ`, `CategoryTheory.Triangulated.Localization.instAdditiveLocalizationShiftFunctorInt`, `CategoryTheory.Triangulated.Localization.instIsTriangulatedLocalization`
`instPreadditiveLocalization'` 📖	CompOp	3 math math: `instAdditiveLocalization'Q'`, `CategoryTheory.Triangulated.Localization.instAdditiveLocalization'ShiftFunctorInt`, `CategoryTheory.Triangulated.Localization.instIsTriangulatedLocalization'`
`preadditive` 📖	CompOp	1 math math: `functor_additive`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`functor_additive` 📖	mathematical	—	`CategoryTheory.Functor.Additive` `preadditive`	—	`Preadditive.map_add`
`functor_additive_iff` 📖	mathematical	—	`CategoryTheory.Functor.Additive` `CategoryTheory.Functor.comp`	—	`CategoryTheory.Functor.instAdditiveComp` `inverts` `exists_leftFraction₂` `CategoryTheory.MorphismProperty.LeftFraction₂.hs` `CategoryTheory.MorphismProperty.LeftFraction₂.map_add` `CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Functor.map_comp` `CategoryTheory.Preadditive.add_comp` `CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s` `CategoryTheory.Functor.comp_map` `CategoryTheory.Functor.map_add` `essSurj` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Preadditive.comp_add`
`instAdditiveLocalization'Q'` 📖	mathematical	—	`CategoryTheory.Functor.Additive` `CategoryTheory.MorphismProperty.Localization'` `CategoryTheory.MorphismProperty.instCategoryLocalization'` `instPreadditiveLocalization'` `CategoryTheory.MorphismProperty.Q'`	—	`functor_additive` `CategoryTheory.MorphismProperty.instIsLocalizationLocalization'Q'`
`instAdditiveLocalizationQ` 📖	mathematical	—	`CategoryTheory.Functor.Additive` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `instPreadditiveLocalization` `CategoryTheory.MorphismProperty.Q`	—	`functor_additive` `CategoryTheory.Functor.q_isLocalization`
`instHasZeroObjectLocalization` 📖	mathematical	—	`CategoryTheory.Limits.HasZeroObject` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization`	—	`CategoryTheory.Functor.hasZeroObject_of_additive` `instAdditiveLocalizationQ`
`instHasZeroObjectLocalization'` 📖	mathematical	—	`CategoryTheory.Limits.HasZeroObject` `CategoryTheory.MorphismProperty.Localization'` `CategoryTheory.MorphismProperty.instCategoryLocalization'`	—	`CategoryTheory.Functor.hasZeroObject_of_additive` `instAdditiveLocalization'Q'`

CategoryTheory.Localization.Preadditive

Definitions

Name	Category	Theorems
`add` 📖	CompOp	6 math math: `comp_add`, `add_comp`, `add_eq_add`, `add_eq`, `comp_add_assoc`, `add_comp_assoc`
`add'` 📖	CompOp	11 math math: `add'_assoc`, `add'_eq`, `add'_map`, `add'_comp_assoc`, `add'_comm`, `comp_add'_assoc`, `add'_comp`, `comp_add'`, `add'_zero`, `zero_add'`, `neg'_add'_self`
`addCommGroup` 📖	CompOp	2 math math: `add_eq`, `map_add`
`addCommGroup'` 📖	CompOp	—
`homEquiv` 📖	CompOp	2 math math: `homEquiv_symm_apply`, `homEquiv_apply`
`neg'` 📖	CompOp	2 math math: `neg'_eq`, `neg'_add'_self`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add'_assoc` 📖	mathematical	—	`add'`	—	`CategoryTheory.Localization.inverts` `CategoryTheory.Localization.exists_leftFraction₃` `add'_eq` `CategoryTheory.MorphismProperty.LeftFraction₃.hs` `CategoryTheory.MorphismProperty.LeftFraction₂.hs` `add_assoc`
`add'_comm` 📖	mathematical	—	`add'`	—	`CategoryTheory.Localization.inverts` `CategoryTheory.Localization.exists_leftFraction₂` `add'_eq` `CategoryTheory.MorphismProperty.LeftFraction₂.symm_add`
`add'_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `add'`	—	`CategoryTheory.Localization.inverts` `CategoryTheory.Localization.exists_leftFraction₂` `CategoryTheory.Localization.exists_leftFraction` `CategoryTheory.MorphismProperty.LeftFraction₂.hs` `CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction` `add'_eq` `CategoryTheory.MorphismProperty.comp_mem` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.toIsMultiplicative` `CategoryTheory.MorphismProperty.LeftFraction.hs` `CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_eq_map` `CategoryTheory.Preadditive.add_comp`
`add'_comp_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `add'`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `add'_comp`
`add'_eq` 📖	mathematical	`CategoryTheory.MorphismProperty.LeftFraction.map` `CategoryTheory.MorphismProperty.LeftFraction₂.fst` `CategoryTheory.Localization.inverts` `CategoryTheory.MorphismProperty.LeftFraction₂.snd`	`add'` `CategoryTheory.MorphismProperty.LeftFraction₂.add`	—	`CategoryTheory.Localization.inverts` `CategoryTheory.Localization.exists_leftFraction₂` `CategoryTheory.MorphismProperty.LeftFraction₂.map_eq_iff` `CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.Functor.map_comp` `CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s_assoc` `CategoryTheory.Preadditive.add_comp`
`add'_map` 📖	mathematical	—	`add'` `CategoryTheory.Functor.map` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup`	—	`CategoryTheory.MorphismProperty.id_mem` `CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities` `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.toIsMultiplicative` `CategoryTheory.Localization.inverts` `add'_eq` `CategoryTheory.MorphismProperty.LeftFraction.map_ofHom`
`add'_zero` 📖	mathematical	—	`add'` `CategoryTheory.Functor.map` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	—	`CategoryTheory.Localization.inverts` `CategoryTheory.Localization.exists_leftFraction` `CategoryTheory.MorphismProperty.LeftFraction.hs` `add'_eq` `CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.Functor.map_comp` `CategoryTheory.Limits.zero_comp` `CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s` `CategoryTheory.MorphismProperty.LeftFraction₂.hs` `add_zero`
`add_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `add`	—	`Equiv.surjective` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id_assoc` `add'_comp_assoc` `add'.congr_simp` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Category.comp_id`
`add_comp_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `add`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `add_comp`
`add_eq` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `addCommGroup` `add`	—	`add_eq_add` `CategoryTheory.Localization.essSurj`
`add_eq_add` 📖	mathematical	—	`add`	—	`comp_add` `add_comp` `CategoryTheory.Category.id_comp` `add.congr_simp` `CategoryTheory.Category.comp_id`
`comp_add` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `add`	—	`Equiv.surjective` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id_assoc` `comp_add'_assoc` `add'.congr_simp`
`comp_add'` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `add'`	—	`CategoryTheory.Localization.inverts` `CategoryTheory.Localization.exists_leftFraction` `CategoryTheory.Localization.exists_leftFraction₂` `CategoryTheory.MorphismProperty.LeftFraction.hs` `CategoryTheory.MorphismProperty.RightFraction₂.exists_leftFraction₂` `add'_eq` `CategoryTheory.MorphismProperty.comp_mem` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.toIsMultiplicative` `CategoryTheory.MorphismProperty.LeftFraction₂.hs` `CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_eq_map` `CategoryTheory.Preadditive.add_comp` `CategoryTheory.Preadditive.comp_add`
`comp_add'_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `add'`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_add'`
`comp_add_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `add`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_add`
`homEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Iso.inv`	—	—
`homEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `homEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Iso.inv` `CategoryTheory.Iso.hom`	—	—
`map_add` 📖	mathematical	—	`CategoryTheory.Functor.map` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `CategoryTheory.Functor.obj` `addCommGroup`	—	`add_eq` `add'.congr_simp` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `add'_map`
`neg'_add'_self` 📖	mathematical	—	`add'` `neg'` `CategoryTheory.Functor.map` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	—	`CategoryTheory.Localization.inverts` `CategoryTheory.Localization.exists_leftFraction` `CategoryTheory.MorphismProperty.LeftFraction.hs` `add'_eq` `neg'_eq` `CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s` `neg_add_cancel` `CategoryTheory.Functor.map_comp` `CategoryTheory.Limits.zero_comp`
`neg'_eq` 📖	mathematical	`CategoryTheory.MorphismProperty.LeftFraction.map` `CategoryTheory.Localization.inverts`	`neg'` `CategoryTheory.MorphismProperty.LeftFraction.neg`	—	`CategoryTheory.Localization.inverts` `CategoryTheory.Localization.exists_leftFraction` `CategoryTheory.MorphismProperty.LeftFraction.map_eq_iff` `CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.Functor.map_comp` `CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s_assoc` `CategoryTheory.Preadditive.neg_comp`
`zero_add'` 📖	mathematical	—	`add'` `CategoryTheory.Functor.map` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	—	`add'_comm` `add'_zero`

CategoryTheory.MorphismProperty.LeftFraction

Definitions

Name	Category	Theorems
`neg` 📖	CompOp	1 math math: `CategoryTheory.Localization.Preadditive.neg'_eq`

CategoryTheory.MorphismProperty.LeftFraction₂

Definitions

Name	Category	Theorems
`add` 📖	CompOp	3 math math: `map_add`, `symm_add`, `CategoryTheory.Localization.Preadditive.add'_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_add` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.MorphismProperty.LeftFraction.map` `add` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `fst` `snd`	—	`hs` `CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.Preadditive.add_comp` `CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s` `CategoryTheory.Functor.map_add`
`symm_add` 📖	mathematical	—	`add` `symm`	—	—

---

← Back to Index