KernelCokernelComp

📁 Source: Mathlib/CategoryTheory/Abelian/DiagramLemmas/KernelCokernelComp.lean

Statistics

Metric	Count
Definitions kernelCokernelCompSequence, isColimit, isLimit, snakeInput, δ, ι, π, φ	8
Theorems instEpiMap'KernelCokernelCompSequenceOfNatNat, instMonoMap'KernelCokernelCompSequenceOfNatNat, inl_π, inl_π_assoc, inl_φ, inl_φ_assoc, inr_π, inr_π_assoc, inr_φ_fst, inr_φ_fst_assoc, instEpiπ, instMonoι, snakeInput_L₀_X₁, snakeInput_L₀_X₂, snakeInput_L₀_X₃, snakeInput_L₀_f, snakeInput_L₀_g, snakeInput_L₁_X₁, snakeInput_L₁_X₂, snakeInput_L₁_X₃, snakeInput_L₁_f, snakeInput_L₁_g, snakeInput_L₂_X₁, snakeInput_L₂_X₂, snakeInput_L₂_X₃, snakeInput_L₂_f, snakeInput_L₂_g, snakeInput_L₃_X₁, snakeInput_L₃_X₂, snakeInput_L₃_X₃, snakeInput_L₃_f, snakeInput_L₃_g, snakeInput_v₀₁_τ₁, snakeInput_v₀₁_τ₂, snakeInput_v₀₁_τ₃, snakeInput_v₁₂_τ₁, snakeInput_v₁₂_τ₂, snakeInput_v₁₂_τ₃, snakeInput_v₂₃_τ₁, snakeInput_v₂₃_τ₂, snakeInput_v₂₃_τ₃, δ_fac, ι_fst, ι_fst_assoc, ι_snd, ι_snd_assoc, ι_φ, ι_φ_assoc, φ_snd, φ_snd_assoc, φ_π, φ_π_assoc, kernelCokernelCompSequence_exact	53
Total	61

CategoryTheory

Definitions

Name	Category	Theorems
kernelCokernelCompSequence 📖	CompOp	3 math math: instMonoMap'KernelCokernelCompSequenceOfNatNat, kernelCokernelCompSequence_exact, instEpiMap'KernelCokernelCompSequenceOfNatNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instEpiMap'KernelCokernelCompSequenceOfNatNat 📖	mathematical	—	Epi Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder kernelCokernelCompSequence ComposableArrows.map'	—	Limits.cokernel.desc_epi epi_comp instEpiId Limits.coequalizer.π_epi
instMonoMap'KernelCokernelCompSequenceOfNatNat 📖	mathematical	—	Mono Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder kernelCokernelCompSequence ComposableArrows.map'	—	Limits.kernel.lift_mono mono_comp Limits.equalizer.ι_mono instMonoId
kernelCokernelCompSequence_exact 📖	mathematical	—	ComposableArrows.Exact Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive kernelCokernelCompSequence	—	ShortComplex.SnakeInput.snake_lemma

CategoryTheory.kernelCokernelCompSequence

Definitions

Name	Category	Theorems
isColimit 📖	CompOp	—
isLimit 📖	CompOp	—
snakeInput 📖	CompOp	29 math math: snakeInput_v₀₁_τ₂, snakeInput_L₀_X₁, snakeInput_L₀_X₂, snakeInput_L₃_g, snakeInput_L₂_X₃, snakeInput_v₂₃_τ₃, snakeInput_L₁_g, snakeInput_L₁_X₃, snakeInput_L₃_f, snakeInput_v₂₃_τ₂, snakeInput_v₁₂_τ₂, snakeInput_L₀_g, snakeInput_L₂_X₂, snakeInput_v₁₂_τ₃, snakeInput_L₃_X₃, snakeInput_L₁_X₂, snakeInput_L₂_g, snakeInput_L₁_f, snakeInput_v₀₁_τ₁, snakeInput_v₀₁_τ₃, snakeInput_L₃_X₁, snakeInput_L₀_f, snakeInput_L₁_X₁, snakeInput_v₂₃_τ₁, snakeInput_v₁₂_τ₁, snakeInput_L₀_X₃, snakeInput_L₂_X₁, snakeInput_L₃_X₂, snakeInput_L₂_f
δ 📖	CompOp	1 math math: δ_fac
ι 📖	CompOp	8 math math: snakeInput_v₀₁_τ₂, ι_φ, ι_fst_assoc, ι_fst, ι_snd, ι_snd_assoc, instMonoι, ι_φ_assoc
π 📖	CompOp	8 math math: inl_π_assoc, inr_π_assoc, snakeInput_v₂₃_τ₂, inr_π, instEpiπ, φ_π, inl_π, φ_π_assoc
φ 📖	CompOp	11 math math: ι_φ, φ_snd_assoc, inr_φ_fst_assoc, snakeInput_v₁₂_τ₂, inl_φ, φ_π, inl_φ_assoc, φ_snd, inr_φ_fst, ι_φ_assoc, φ_π_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inl_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.cokernel CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.biprod.inl π CategoryTheory.Limits.cokernel.π	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.biprod.inl_desc
inl_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.cokernel CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels π CategoryTheory.Limits.cokernel.π	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_π
inl_φ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.biprod.inl φ	—	CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.biprod.inl_desc
inl_φ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.biprod.inl φ	—	CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_φ
inr_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.cokernel CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.biprod.inr π CategoryTheory.Limits.cokernel.π	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.biprod.inr_desc
inr_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.biprod.inr CategoryTheory.Limits.cokernel CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels π CategoryTheory.Limits.cokernel.π	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_π
inr_φ_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.biprod.inr φ CategoryTheory.Limits.biprod.fst Quiver.Hom CategoryTheory.CategoryStruct.toQuiver NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.id	—	CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.biprod.inr_desc_assoc CategoryTheory.Limits.biprod.lift_fst
inr_φ_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.biprod.inr φ CategoryTheory.Limits.biprod.fst Quiver.Hom CategoryTheory.CategoryStruct.toQuiver NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.id	—	CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_φ_fst
instEpiπ 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.cokernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels π	—	CategoryTheory.epi_of_epi_fac CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.coequalizer.π_epi inr_π
instMonoι 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.biprod CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts ι	—	CategoryTheory.mono_of_mono_fac CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.equalizer.ι_mono ι_fst
snakeInput_L₀_X₁ 📖	mathematical	—	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.SnakeInput.L₀ snakeInput CategoryTheory.Limits.kernel	—	—
snakeInput_L₀_X₂ 📖	mathematical	—	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.SnakeInput.L₀ snakeInput CategoryTheory.Limits.kernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
snakeInput_L₀_X₃ 📖	mathematical	—	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.SnakeInput.L₀ snakeInput CategoryTheory.Limits.kernel	—	—
snakeInput_L₀_f 📖	mathematical	—	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.SnakeInput.L₀ snakeInput CategoryTheory.Limits.kernel.map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
snakeInput_L₀_g 📖	mathematical	—	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.SnakeInput.L₀ snakeInput CategoryTheory.Limits.kernel.map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
snakeInput_L₁_X₁ 📖	mathematical	—	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.SnakeInput.L₁ snakeInput	—	—
snakeInput_L₁_X₂ 📖	mathematical	—	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.SnakeInput.L₁ snakeInput CategoryTheory.Limits.biprod	—	—
snakeInput_L₁_X₃ 📖	mathematical	—	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.SnakeInput.L₁ snakeInput	—	—
snakeInput_L₁_f 📖	mathematical	—	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.SnakeInput.L₁ snakeInput CategoryTheory.Limits.biprod.inl	—	—
snakeInput_L₁_g 📖	mathematical	—	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.SnakeInput.L₁ snakeInput CategoryTheory.Limits.biprod.snd	—	—
snakeInput_L₂_X₁ 📖	mathematical	—	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.SnakeInput.L₂ snakeInput	—	—
snakeInput_L₂_X₂ 📖	mathematical	—	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.SnakeInput.L₂ snakeInput CategoryTheory.Limits.biprod	—	—
snakeInput_L₂_X₃ 📖	mathematical	—	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.SnakeInput.L₂ snakeInput	—	—
snakeInput_L₂_f 📖	mathematical	—	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.SnakeInput.L₂ snakeInput CategoryTheory.Limits.biprod.inl	—	—
snakeInput_L₂_g 📖	mathematical	—	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.SnakeInput.L₂ snakeInput CategoryTheory.Limits.biprod.snd	—	—
snakeInput_L₃_X₁ 📖	mathematical	—	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.SnakeInput.L₃ snakeInput CategoryTheory.Limits.cokernel	—	—
snakeInput_L₃_X₂ 📖	mathematical	—	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.SnakeInput.L₃ snakeInput CategoryTheory.Limits.cokernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
snakeInput_L₃_X₃ 📖	mathematical	—	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.SnakeInput.L₃ snakeInput CategoryTheory.Limits.cokernel	—	—
snakeInput_L₃_f 📖	mathematical	—	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.SnakeInput.L₃ snakeInput CategoryTheory.Limits.cokernel.map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
snakeInput_L₃_g 📖	mathematical	—	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.SnakeInput.L₃ snakeInput CategoryTheory.Limits.cokernel.map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
snakeInput_v₀₁_τ₁ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.kernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel.map CategoryTheory.CategoryStruct.id CategoryTheory.Limits.biprod CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.snd CategoryTheory.ShortComplex.SnakeInput.v₀₁ snakeInput CategoryTheory.Limits.kernel.ι	—	—
snakeInput_v₀₁_τ₂ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.kernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel.map CategoryTheory.CategoryStruct.id CategoryTheory.Limits.biprod CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.snd CategoryTheory.ShortComplex.SnakeInput.v₀₁ snakeInput ι	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts
snakeInput_v₀₁_τ₃ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.kernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel.map CategoryTheory.CategoryStruct.id CategoryTheory.Limits.biprod CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.snd CategoryTheory.ShortComplex.SnakeInput.v₀₁ snakeInput CategoryTheory.Limits.kernel.ι	—	—
snakeInput_v₁₂_τ₁ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.biprod CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.snd CategoryTheory.ShortComplex.SnakeInput.v₁₂ snakeInput	—	—
snakeInput_v₁₂_τ₂ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.biprod CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.snd CategoryTheory.ShortComplex.SnakeInput.v₁₂ snakeInput φ	—	CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts
snakeInput_v₁₂_τ₃ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.biprod CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.snd CategoryTheory.ShortComplex.SnakeInput.v₁₂ snakeInput	—	—
snakeInput_v₂₃_τ₁ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.biprod CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.cokernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.cokernel.map CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex.SnakeInput.v₂₃ snakeInput CategoryTheory.Limits.cokernel.π	—	—
snakeInput_v₂₃_τ₂ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.biprod CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.cokernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.cokernel.map CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex.SnakeInput.v₂₃ snakeInput π	—	CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels
snakeInput_v₂₃_τ₃ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.biprod CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.cokernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.cokernel.map CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex.SnakeInput.v₂₃ snakeInput CategoryTheory.Limits.cokernel.π	—	—
δ_fac 📖	mathematical	—	δ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.kernel.ι CategoryTheory.Limits.cokernel.π	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Category.id_comp CategoryTheory.Preadditive.neg_comp CategoryTheory.ShortComplex.SnakeInput.δ_eq CategoryTheory.Category.assoc CategoryTheory.Limits.BinaryBicone.inr_snd CategoryTheory.Category.comp_id CategoryTheory.Limits.biprod.hom_ext CategoryTheory.Limits.BinaryBicone.inl_fst inr_φ_fst CategoryTheory.Preadditive.comp_neg CategoryTheory.Limits.BinaryBicone.inl_snd CategoryTheory.Limits.comp_zero neg_zero CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts φ_snd CategoryTheory.Limits.BinaryBicone.inr_snd_assoc CategoryTheory.Limits.kernel.condition
ι_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.biprod CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts ι CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.kernel.ι	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.biprod.lift_fst
ι_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.biprod CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts ι CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.kernel.ι	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_fst
ι_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.biprod CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts ι CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.kernel.ι	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.biprod.lift_snd
ι_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.biprod CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts ι CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.kernel.ι	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_snd
ι_φ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.biprod CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts ι φ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.biprod.lift_desc CategoryTheory.Category.assoc CategoryTheory.Limits.biprod.hom_ext CategoryTheory.Preadditive.add_comp CategoryTheory.Limits.BinaryBicone.inl_fst CategoryTheory.Category.comp_id CategoryTheory.Limits.biprod.lift_fst CategoryTheory.Preadditive.comp_neg add_neg_cancel CategoryTheory.Limits.zero_comp CategoryTheory.Limits.BinaryBicone.inl_snd CategoryTheory.Limits.comp_zero CategoryTheory.Limits.biprod.lift_snd CategoryTheory.Limits.kernel.condition add_zero
ι_φ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.biprod CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts ι φ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_φ
φ_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts φ CategoryTheory.Limits.biprod.snd	—	CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.biprod.hom_ext' CategoryTheory.Limits.biprod.inl_desc_assoc CategoryTheory.Category.assoc CategoryTheory.Limits.BinaryBicone.inl_snd CategoryTheory.Limits.comp_zero CategoryTheory.Limits.BinaryBicone.inl_snd_assoc CategoryTheory.Limits.zero_comp CategoryTheory.Limits.biprod.inr_desc_assoc CategoryTheory.Limits.biprod.lift_snd CategoryTheory.Limits.BinaryBicone.inr_snd_assoc
φ_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts φ CategoryTheory.Limits.biprod.snd	—	CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' φ_snd
φ_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.cokernel CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels φ π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.biprod.hom_ext' CategoryTheory.Limits.biprod.inl_desc_assoc CategoryTheory.Category.assoc CategoryTheory.Limits.biprod.inl_desc CategoryTheory.Limits.comp_zero CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.biprod.inr_desc_assoc CategoryTheory.Limits.biprod.lift_desc CategoryTheory.Preadditive.neg_comp CategoryTheory.Category.id_comp neg_add_cancel
φ_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts φ CategoryTheory.Limits.cokernel CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' φ_π

---

← Back to Index