Kernels

📁 Source: Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean

Statistics

Metric	Count
Definitions `cokernelCocone`, `cokernelLift`, `explicitCokernel`, `map`, `explicitCokernelDesc`, `explicitCokernelIso`, `explicitCokernelπ`, `fork`, `instNNNormHom`, `instNormHom`, `isColimitCokernelCocone`, `cokernelCocone`, `cokernelLift`	13
Theorems `map_desc`, `comp_explicitCokernelπ`, `comp_explicitCokernelπ_assoc`, `explicitCokernelDesc_comp_eq_desc`, `explicitCokernelDesc_comp_eq_zero`, `explicitCokernelDesc_normNoninc`, `explicitCokernelDesc_norm_le`, `explicitCokernelDesc_norm_le_of_norm_le`, `explicitCokernelDesc_unique`, `explicitCokernelDesc_zero`, `explicitCokernelIso_hom_desc`, `explicitCokernelIso_hom_π`, `explicitCokernelIso_inv_π`, `explicitCokernel_hom_ext`, `explicitCokernel_hom_ext_iff`, `epi`, `explicitCokernelπ_apply_dom_eq_zero`, `explicitCokernelπ_desc`, `explicitCokernelπ_desc_apply`, `explicitCokernelπ_desc_assoc`, `explicitCokernelπ_surjective`, `hasLimit_parallelPair`, `instHasCokernels`, `instHasEqualizers`, `isQuotient_explicitCokernelπ`, `normNoninc_explicitCokernelπ`, `instHasCokernels`	27
Total	40

SemiNormedGrp

Definitions

Name	Category	Theorems
`cokernelCocone` 📖	CompOp	—
`cokernelLift` 📖	CompOp	—
`explicitCokernel` 📖	CompOp	21 math math: `explicitCokernelDesc_norm_le`, `explicitCokernelπ_desc_apply`, `explicitCokernelDesc_comp_eq_desc`, `explicitCokernelπ.epi`, `isQuotient_explicitCokernelπ`, `explicitCokernel_hom_ext_iff`, `explicitCokernelDesc_normNoninc`, `explicitCokernelπ_desc`, `explicitCokernelπ_apply_dom_eq_zero`, `explicitCokernelπ_surjective`, `explicitCokernelIso_hom_π`, `explicitCokernelDesc_zero`, `comp_explicitCokernelπ`, `normNoninc_explicitCokernelπ`, `explicitCokernelDesc_comp_eq_zero`, `comp_explicitCokernelπ_assoc`, `explicitCokernelIso_hom_desc`, `explicitCokernelDesc_norm_le_of_norm_le`, `explicitCokernelIso_inv_π`, `ExplicitCoker.map_desc`, `explicitCokernelπ_desc_assoc`
`explicitCokernelDesc` 📖	CompOp	12 math math: `explicitCokernelDesc_norm_le`, `explicitCokernelπ_desc_apply`, `explicitCokernelDesc_comp_eq_desc`, `explicitCokernelDesc_unique`, `explicitCokernelDesc_normNoninc`, `explicitCokernelπ_desc`, `explicitCokernelDesc_zero`, `explicitCokernelDesc_comp_eq_zero`, `explicitCokernelIso_hom_desc`, `explicitCokernelDesc_norm_le_of_norm_le`, `ExplicitCoker.map_desc`, `explicitCokernelπ_desc_assoc`
`explicitCokernelIso` 📖	CompOp	3 math math: `explicitCokernelIso_hom_π`, `explicitCokernelIso_hom_desc`, `explicitCokernelIso_inv_π`
`explicitCokernelπ` 📖	CompOp	13 math math: `explicitCokernelπ_desc_apply`, `explicitCokernelπ.epi`, `isQuotient_explicitCokernelπ`, `explicitCokernel_hom_ext_iff`, `explicitCokernelπ_desc`, `explicitCokernelπ_apply_dom_eq_zero`, `explicitCokernelπ_surjective`, `explicitCokernelIso_hom_π`, `comp_explicitCokernelπ`, `normNoninc_explicitCokernelπ`, `comp_explicitCokernelπ_assoc`, `explicitCokernelIso_inv_π`, `explicitCokernelπ_desc_assoc`
`fork` 📖	CompOp	—
`instNNNormHom` 📖	CompOp	—
`instNormHom` 📖	CompOp	1 math math: `explicitCokernelDesc_norm_le`
`isColimitCokernelCocone` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_explicitCokernelπ` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SemiNormedGrp` `CategoryTheory.Category.toCategoryStruct` `instLargeCategory` `explicitCokernel` `explicitCokernelπ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `instZeroHom`	—	`CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_left` `CategoryTheory.Limits.CokernelCofork.condition` `CategoryTheory.Limits.Cocone.w`
`comp_explicitCokernelπ_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SemiNormedGrp` `CategoryTheory.Category.toCategoryStruct` `instLargeCategory` `explicitCokernel` `explicitCokernelπ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `instZeroHom`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_explicitCokernelπ`
`explicitCokernelDesc_comp_eq_desc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SemiNormedGrp` `CategoryTheory.Category.toCategoryStruct` `instLargeCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `instZeroHom`	`explicitCokernel` `explicitCokernelDesc`	—	`explicitCokernelDesc_unique` `CategoryTheory.Category.assoc` `explicitCokernelπ_desc`
`explicitCokernelDesc_comp_eq_zero` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SemiNormedGrp` `CategoryTheory.Category.toCategoryStruct` `instLargeCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `instZeroHom`	`explicitCokernel` `explicitCokernelDesc`	—	`CategoryTheory.cancel_epi` `explicitCokernelπ.epi` `CategoryTheory.Category.assoc` `explicitCokernelπ_desc` `CategoryTheory.Limits.comp_zero`
`explicitCokernelDesc_normNoninc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SemiNormedGrp` `CategoryTheory.Category.toCategoryStruct` `instLargeCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `instZeroHom` `NormedAddGroupHom.NormNoninc` `carrier` `str` `Hom.hom`	`explicitCokernel` `explicitCokernelDesc`	—	`NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one` `NNReal.coe_one` `explicitCokernelDesc_norm_le_of_norm_le`
`explicitCokernelDesc_norm_le` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SemiNormedGrp` `CategoryTheory.Category.toCategoryStruct` `instLargeCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `instZeroHom`	`Real` `Real.instLE` `Norm.norm` `explicitCokernel` `instNormHom` `explicitCokernelDesc`	—	`explicitCokernelDesc_norm_le_of_norm_le` `le_rfl`
`explicitCokernelDesc_norm_le_of_norm_le` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SemiNormedGrp` `CategoryTheory.Category.toCategoryStruct` `instLargeCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `instZeroHom` `Real` `Real.instLE` `Norm.norm` `instNormHom` `NNReal.toReal`	`explicitCokernel` `explicitCokernelDesc`	—	`NormedAddGroupHom.lift_norm_le`
`explicitCokernelDesc_unique` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SemiNormedGrp` `CategoryTheory.Category.toCategoryStruct` `instLargeCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `instZeroHom` `explicitCokernel` `explicitCokernelπ`	`explicitCokernelDesc`	—	`CategoryTheory.Limits.IsColimit.uniq` `CategoryTheory.Limits.zero_comp` `CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_left` `CategoryTheory.Limits.CokernelCofork.condition`
`explicitCokernelDesc_zero` 📖	mathematical	—	`explicitCokernelDesc` `Quiver.Hom` `SemiNormedGrp` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instLargeCategory` `instZeroHom` `explicitCokernel`	—	`CategoryTheory.Limits.comp_zero` `explicitCokernelDesc_unique`
`explicitCokernelIso_hom_desc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SemiNormedGrp` `CategoryTheory.Category.toCategoryStruct` `instLargeCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `instZeroHom`	`explicitCokernel` `CategoryTheory.Limits.cokernel` `instHasZeroMorphisms` `CategoryTheory.Limits.HasCokernels.has_colimit` `instHasCokernels` `CategoryTheory.Iso.hom` `explicitCokernelIso` `CategoryTheory.Limits.cokernel.desc` `explicitCokernelDesc`	—	`explicitCokernel_hom_ext` `CategoryTheory.Limits.HasCokernels.has_colimit` `instHasCokernels` `CategoryTheory.Limits.Cofork.IsColimit.π_desc_assoc` `CategoryTheory.Limits.cokernel.π_desc` `CategoryTheory.Limits.Cofork.IsColimit.π_desc`
`explicitCokernelIso_hom_π` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SemiNormedGrp` `CategoryTheory.Category.toCategoryStruct` `instLargeCategory` `explicitCokernel` `CategoryTheory.Limits.cokernel` `instHasZeroMorphisms` `CategoryTheory.Limits.HasCokernels.has_colimit` `instHasCokernels` `explicitCokernelπ` `CategoryTheory.Iso.hom` `explicitCokernelIso` `CategoryTheory.Limits.cokernel.π`	—	`CategoryTheory.Limits.HasCokernels.has_colimit` `instHasCokernels` `CategoryTheory.Limits.Cofork.IsColimit.π_desc`
`explicitCokernelIso_inv_π` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SemiNormedGrp` `CategoryTheory.Category.toCategoryStruct` `instLargeCategory` `CategoryTheory.Limits.cokernel` `instHasZeroMorphisms` `CategoryTheory.Limits.HasCokernels.has_colimit` `instHasCokernels` `explicitCokernel` `CategoryTheory.Limits.cokernel.π` `CategoryTheory.Iso.inv` `explicitCokernelIso` `explicitCokernelπ`	—	`CategoryTheory.Limits.HasCokernels.has_colimit` `instHasCokernels` `CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv`
`explicitCokernel_hom_ext` 📖	—	`CategoryTheory.CategoryStruct.comp` `SemiNormedGrp` `CategoryTheory.Category.toCategoryStruct` `instLargeCategory` `explicitCokernel` `explicitCokernelπ`	—	—	`comp_explicitCokernelπ_assoc` `CategoryTheory.Limits.zero_comp` `explicitCokernelDesc_unique`
`explicitCokernel_hom_ext_iff` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SemiNormedGrp` `CategoryTheory.Category.toCategoryStruct` `instLargeCategory` `explicitCokernel` `explicitCokernelπ`	—	`explicitCokernel_hom_ext`
`explicitCokernelπ_apply_dom_eq_zero` 📖	mathematical	—	`DFunLike.coe` `explicitCokernel` `carrier` `CategoryTheory.ConcreteCategory.hom` `SemiNormedGrp` `instLargeCategory` `NormedAddGroupHom` `str` `NormedAddGroupHom.funLike` `instConcreteCategoryNormedAddGroupHomCarrier` `explicitCokernelπ` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`comp_explicitCokernelπ`
`explicitCokernelπ_desc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SemiNormedGrp` `CategoryTheory.Category.toCategoryStruct` `instLargeCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `instZeroHom`	`explicitCokernel` `explicitCokernelπ` `explicitCokernelDesc`	—	`CategoryTheory.Limits.IsColimit.fac`
`explicitCokernelπ_desc_apply` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SemiNormedGrp` `CategoryTheory.Category.toCategoryStruct` `instLargeCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `instZeroHom`	`DFunLike.coe` `explicitCokernel` `carrier` `CategoryTheory.ConcreteCategory.hom` `NormedAddGroupHom` `str` `NormedAddGroupHom.funLike` `instConcreteCategoryNormedAddGroupHomCarrier` `explicitCokernelDesc` `explicitCokernelπ`	—	`explicitCokernelπ_desc`
`explicitCokernelπ_desc_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SemiNormedGrp` `CategoryTheory.Category.toCategoryStruct` `instLargeCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `instZeroHom`	`explicitCokernel` `explicitCokernelπ` `explicitCokernelDesc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `explicitCokernelπ_desc`
`explicitCokernelπ_surjective` 📖	mathematical	—	`carrier` `explicitCokernel` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `SemiNormedGrp` `instLargeCategory` `NormedAddGroupHom` `str` `NormedAddGroupHom.funLike` `instConcreteCategoryNormedAddGroupHomCarrier` `explicitCokernelπ`	—	`Quot.mk_surjective`
`hasLimit_parallelPair` 📖	mathematical	—	`CategoryTheory.Limits.HasLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `SemiNormedGrp` `instLargeCategory` `CategoryTheory.Limits.parallelPair`	—	`hom_sub` `map_sub` `AddMonoidHom.instAddMonoidHomClass` `AddMonoidHom.sub_apply` `sub_eq_zero` `CategoryTheory.Limits.Fork.condition` `hom_ext` `NormedAddGroupHom.ker.incl_comp_lift` `NormedAddGroupHom.ext` `NormedAddGroupHom.ker.lift.congr_simp`
`instHasCokernels` 📖	mathematical	—	`CategoryTheory.Limits.HasCokernels` `SemiNormedGrp` `instLargeCategory` `instHasZeroMorphisms`	—	—
`instHasEqualizers` 📖	mathematical	—	`CategoryTheory.Limits.HasEqualizers` `SemiNormedGrp` `instLargeCategory`	—	`CategoryTheory.Limits.hasEqualizers_of_hasLimit_parallelPair` `hasLimit_parallelPair`
`isQuotient_explicitCokernelπ` 📖	mathematical	—	`NormedAddGroupHom.IsQuotient` `carrier` `explicitCokernel` `str` `Hom.hom` `explicitCokernelπ`	—	`NormedAddGroupHom.isQuotientQuotient`
`normNoninc_explicitCokernelπ` 📖	mathematical	—	`NormedAddGroupHom.NormNoninc` `carrier` `explicitCokernel` `str` `Hom.hom` `explicitCokernelπ`	—	`NormedAddGroupHom.IsQuotient.norm_le` `isQuotient_explicitCokernelπ`

SemiNormedGrp.ExplicitCoker

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_desc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SemiNormedGrp` `CategoryTheory.Category.toCategoryStruct` `SemiNormedGrp.instLargeCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `SemiNormedGrp.instZeroHom`	`SemiNormedGrp.explicitCokernel` `SemiNormedGrp.explicitCokernelDesc` `SemiNormedGrp.explicitCokernel.map`	—	`CategoryTheory.cancel_epi` `SemiNormedGrp.explicitCokernelπ.epi` `SemiNormedGrp.explicitCokernelπ_desc` `CategoryTheory.Category.assoc`

SemiNormedGrp.explicitCokernel

Definitions

Name	Category	Theorems
`map` 📖	CompOp	1 math math: `SemiNormedGrp.ExplicitCoker.map_desc`

SemiNormedGrp.explicitCokernelπ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi` 📖	mathematical	—	`CategoryTheory.Epi` `SemiNormedGrp` `SemiNormedGrp.instLargeCategory` `SemiNormedGrp.explicitCokernel` `SemiNormedGrp.explicitCokernelπ`	—	`SemiNormedGrp.explicitCokernel_hom_ext` `SemiNormedGrp.hom_ext` `NormedAddGroupHom.ext`

SemiNormedGrp₁

Definitions

Name	Category	Theorems
`cokernelCocone` 📖	CompOp	—
`cokernelLift` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasCokernels` 📖	mathematical	—	`CategoryTheory.Limits.HasCokernels` `SemiNormedGrp₁` `instLargeCategory` `instHasZeroMorphisms`	—	`hom_ext` `NormedAddGroupHom.ext` `CategoryTheory.Limits.CokernelCofork.condition` `NormedAddGroupHom.lift_unique`

---

← Back to Index