CommSq

📁 Source: Mathlib/CategoryTheory/Abelian/CommSq.lean

Statistics

Metric	Count
Definitions	0
Theorems epi_kernel_map_of_isPushout, instIsStableUnderBaseChangeEpimorphisms, instIsStableUnderCobaseChangeMonomorphisms, mono_cokernel_map_of_isPullback, exact_shortComplex', exact_shortComplex, hom_eq_add_up_to_refinements, mono_of_isPullback_of_mono	8
Total	8

CategoryTheory.Abelian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_kernel_map_of_isPushout 📖	mathematical	CategoryTheory.IsPushout	CategoryTheory.Epi CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.kernel.map CategoryTheory.CommSq.w CategoryTheory.IsPushout.toCommSq	—	CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.CommSq.w CategoryTheory.IsPushout.toCommSq CategoryTheory.epi_iff_surjective_up_to_refinements CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct hasBinaryBiproducts CategoryTheory.Limits.CokernelCofork.condition CategoryTheory.ShortComplex.Exact.exact_up_to_refinements CategoryTheory.ShortComplex.exact_of_g_is_cokernel CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc CategoryTheory.Limits.biprod.inr_desc CategoryTheory.Limits.kernel.condition CategoryTheory.Limits.comp_zero CategoryTheory.Limits.biprod.lift_fst CategoryTheory.Limits.BinaryBicone.inr_fst CategoryTheory.eq_whisker CategoryTheory.Limits.equalizer.hom_ext CategoryTheory.Preadditive.neg_comp CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Limits.kernel.lift_ι_assoc CategoryTheory.Limits.BinaryBicone.inr_snd CategoryTheory.Category.comp_id CategoryTheory.Limits.biprod.lift_snd CategoryTheory.Preadditive.comp_neg
instIsStableUnderBaseChangeEpimorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange CategoryTheory.MorphismProperty.epimorphisms	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange.mk' CategoryTheory.MorphismProperty.RespectsIso.epimorphisms epi_pullback_of_epi_g CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits hasFiniteLimits
instIsStableUnderCobaseChangeMonomorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderCobaseChange CategoryTheory.MorphismProperty.monomorphisms	—	CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.mk' CategoryTheory.MorphismProperty.RespectsIso.monomorphisms mono_pushout_of_mono_f CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits hasFiniteColimits
mono_cokernel_map_of_isPullback 📖	mathematical	CategoryTheory.IsPullback	CategoryTheory.Mono CategoryTheory.Limits.cokernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Limits.cokernel.map CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq	—	CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq CategoryTheory.Preadditive.mono_iff_cancel_zero CategoryTheory.surjective_up_to_refinements_of_epi CategoryTheory.Limits.coequalizer.π_epi CategoryTheory.Limits.cokernel.condition CategoryTheory.ShortComplex.exact_of_g_is_cokernel CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.Exact.exact_up_to_refinements CategoryTheory.Category.assoc CategoryTheory.Limits.cokernel.π_desc CategoryTheory.Limits.comp_zero CategoryTheory.eq_whisker CategoryTheory.IsPullback.exists_lift CategoryTheory.cancel_epi Mathlib.Tactic.Reassoc.eq_whisker'

CategoryTheory.IsPullback

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exact_shortComplex' 📖	mathematical	CategoryTheory.IsPullback	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.CommSq.shortComplex' CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts toCommSq	—	CategoryTheory.ShortComplex.exact_of_f_is_kernel CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts toCommSq CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian

CategoryTheory.IsPushout

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exact_shortComplex 📖	mathematical	CategoryTheory.IsPushout	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.CommSq.shortComplex CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts toCommSq	—	CategoryTheory.ShortComplex.exact_of_g_is_cokernel CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts toCommSq CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian
hom_eq_add_up_to_refinements 📖	mathematical	CategoryTheory.IsPushout	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts toCommSq epi_shortComplex_g CategoryTheory.surjective_up_to_refinements_of_epi CategoryTheory.Category.assoc CategoryTheory.Limits.biprod.hom_ext' CategoryTheory.Limits.biprod.inl_desc CategoryTheory.Preadditive.comp_add CategoryTheory.Limits.BinaryBicone.inl_fst_assoc CategoryTheory.Limits.BinaryBicone.inl_snd_assoc CategoryTheory.Limits.zero_comp add_zero CategoryTheory.Limits.biprod.inr_desc CategoryTheory.Limits.BinaryBicone.inr_fst_assoc CategoryTheory.Limits.BinaryBicone.inr_snd_assoc zero_add
mono_of_isPullback_of_mono 📖	mathematical	CategoryTheory.IsPushout CategoryTheory.IsPullback CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Mono	—	CategoryTheory.Preadditive.mono_of_cancel_zero hom_eq_add_up_to_refinements CategoryTheory.Preadditive.neg_comp neg_eq_iff_add_eq_zero CategoryTheory.Category.assoc CategoryTheory.Preadditive.add_comp CategoryTheory.Limits.comp_zero CategoryTheory.CommSq.w toCommSq CategoryTheory.IsPullback.lift_snd_assoc add_comm CategoryTheory.cancel_epi CategoryTheory.Limits.zero_comp CategoryTheory.Limits.zero_of_comp_mono Mathlib.Tactic.Reassoc.eq_whisker'

---

← Back to Index