Mathlib.CategoryTheory.Preadditive.Basic

CategoryTheory.Preadditive structure

Full source

/-- A category is called preadditive if `P ⟶ Q` is an abelian group such that composition is
    linear in both variables. -/
@[stacks 00ZY]
class Preadditive where
  homGroup : ∀ P Q : C, AddCommGroup (P ⟶ Q) := by infer_instance
  add_comp : ∀ (P Q R : C) (f f' : P ⟶ Q) (g : Q ⟶ R), (f + f') ≫ g = f ≫ g + f' ≫ g := by
    aesop_cat
  comp_add : ∀ (P Q R : C) (f : P ⟶ Q) (g g' : Q ⟶ R), f ≫ (g + g') = f ≫ g + f ≫ g' := by
    aesop_cat

Preadditive Category

Informal description

A preadditive category is a category where for every pair of objects $X$ and $Y$, the hom-set $\text{Hom}(X, Y)$ is endowed with the structure of an abelian group, and composition of morphisms is bilinear with respect to this group structure. That is, for any morphisms $f, g \in \text{Hom}(X, Y)$ and $h \in \text{Hom}(Y, Z)$, the following hold: 1. $h \circ (f + g) = h \circ f + h \circ g$ 2. $(f + g) \circ h = f \circ h + g \circ h$

CategoryTheory.Preadditive.inducedCategory instance

: Preadditive.{v} (InducedCategory C F)

Full source

instance inducedCategory : Preadditive.{v} (InducedCategory C F) where
  homGroup P Q := @Preadditive.homGroup C _ _ (F P) (F Q)
  add_comp _ _ _ _ _ _ := add_comp _ _ _ _ _ _
  comp_add _ _ _ _ _ _ := comp_add _ _ _ _ _ _

Preadditive Structure on Induced Categories

Informal description

For any preadditive category $\mathcal{C}$ and function $F : D \to \mathcal{C}$ from a type $D$ to the objects of $\mathcal{C}$, the induced category structure on $D$ inherits a preadditive structure. That is, for any objects $X, Y$ in $D$, the hom-set $\text{Hom}(X, Y)$ is endowed with an abelian group structure, and composition of morphisms is bilinear with respect to this group structure.

CategoryTheory.Preadditive.fullSubcategory instance

(Z : ObjectProperty C) : Preadditive Z.FullSubcategory

Full source

instance fullSubcategory (Z : ObjectProperty C) : Preadditive Z.FullSubcategory where
  homGroup P Q := @Preadditive.homGroup C _ _ P.obj Q.obj
  add_comp _ _ _ _ _ _ := add_comp _ _ _ _ _ _
  comp_add _ _ _ _ _ _ := comp_add _ _ _ _ _ _

Preadditive Structure on Full Subcategories

Informal description

For any preadditive category $C$ and any property $Z$ on its objects, the full subcategory of $C$ consisting of objects satisfying $Z$ inherits a preadditive structure. That is, the hom-sets in this subcategory are abelian groups and composition remains bilinear.

CategoryTheory.Preadditive.instAddCommGroupEnd instance

(X : C) : AddCommGroup (End X)

Full source

instance (X : C) : AddCommGroup (End X) := by
  dsimp [End]
  infer_instance

Additive Commutative Group Structure on Endomorphisms in a Preadditive Category

Informal description

For any object $X$ in a preadditive category $C$, the abelian group structure on the endomorphisms $\text{End}(X)$ makes it into an additive commutative group.

CategoryTheory.Preadditive.leftComp definition

{P Q : C} (R : C) (f : P ⟶ Q) : (Q ⟶ R) →+ (P ⟶ R)

Full source

/-- Composition by a fixed left argument as a group homomorphism -/
def leftComp {P Q : C} (R : C) (f : P ⟶ Q) : (Q ⟶ R) →+ (P ⟶ R) :=
  mk' (fun g => f ≫ g) fun g g' => by simp

Left composition group homomorphism in a preadditive category

Informal description

For objects $ P, Q, R $ in a preadditive category $ C $ and a morphism $ f : P \to Q $, the function $ \text{leftComp}(R, f) $ is the group homomorphism from $ \text{Hom}(Q, R) $ to $ \text{Hom}(P, R) $ defined by post-composition with $ f $, i.e., $ g \mapsto f \circ g $.

CategoryTheory.Preadditive.rightComp definition

(P : C) {Q R : C} (g : Q ⟶ R) : (P ⟶ Q) →+ (P ⟶ R)

Full source

/-- Composition by a fixed right argument as a group homomorphism -/
def rightComp (P : C) {Q R : C} (g : Q ⟶ R) : (P ⟶ Q) →+ (P ⟶ R) :=
  mk' (fun f => f ≫ g) fun f f' => by simp

Right composition group homomorphism in a preadditive category

Informal description

For objects $ P, Q, R $ in a preadditive category $ C $ and a morphism $ g : Q \to R $, the function $ \text{rightComp}(P, g) $ is the group homomorphism from $ \text{Hom}(P, Q) $ to $ \text{Hom}(P, R) $ defined by pre-composition with $ g $, i.e., $ f \mapsto f \circ g $.

CategoryTheory.Preadditive.compHom definition

: (P ⟶ Q) →+ (Q ⟶ R) →+ (P ⟶ R)

Full source

/-- Composition as a bilinear group homomorphism -/
def compHom : (P ⟶ Q) →+ (Q ⟶ R) →+ (P ⟶ R) :=
  AddMonoidHom.mk' (fun f => leftComp _ f) fun f₁ f₂ =>
    AddMonoidHom.ext fun g => (rightComp _ g).map_add f₁ f₂

Composition as a bilinear group homomorphism

Informal description

For objects $ P, Q, R $ in a preadditive category $ C $, the function $\text{compHom}$ is a group homomorphism from $\text{Hom}(P, Q)$ to the group of homomorphisms from $\text{Hom}(Q, R)$ to $\text{Hom}(P, R)$. It maps a morphism $ f : P \to Q $ to the group homomorphism $\text{leftComp}(R, f)$, which is post-composition with $ f $. Moreover, $\text{compHom}$ is additive in its argument $ f $, meaning that $\text{compHom}(f_1 + f_2) = \text{compHom}(f_1) + \text{compHom}(f_2)$ for any $ f_1, f_2 : P \to Q $.

CategoryTheory.Preadditive.sub_comp theorem

: (f - f') ≫ g = f ≫ g - f' ≫ g

Full source

@[reassoc, simp]
theorem sub_comp : (f - f') ≫ g = f ≫ g - f' ≫ g :=
  map_sub (rightComp P g) f f'

Subtraction and Composition: $(f - f') \circ g = f \circ g - f' \circ g$

Informal description

In a preadditive category, for any morphisms $f, f' \colon P \to Q$ and $g \colon Q \to R$, the composition of the difference $(f - f')$ with $g$ equals the difference of the compositions $(f \circ g) - (f' \circ g)$, i.e., $$(f - f') \circ g = f \circ g - f' \circ g.$$

CategoryTheory.Preadditive.comp_sub theorem

: f ≫ (g - g') = f ≫ g - f ≫ g'

Full source

@[reassoc, simp]
theorem comp_sub : f ≫ (g - g') = f ≫ g - f ≫ g' :=
  map_sub (leftComp R f) g g'

Bilinearity of composition: $f \circ (g - g') = f \circ g - f \circ g'$

Informal description

In a preadditive category, for any morphisms $f$, $g$, and $g'$, the composition of $f$ with the difference $g - g'$ is equal to the difference of the compositions $f \circ g$ and $f \circ g'$, i.e., $f \circ (g - g') = f \circ g - f \circ g'$.

CategoryTheory.Preadditive.neg_comp theorem

: (-f) ≫ g = -f ≫ g

Full source

@[reassoc, simp]
theorem neg_comp : (-f) ≫ g = -f ≫ g :=
  map_neg (rightComp P g) f

Negation and Composition: $(-f) \circ g = -(f \circ g)$

Informal description

In a preadditive category, for any morphisms $f$ and $g$, the composition of the negation of $f$ with $g$ is equal to the negation of the composition of $f$ with $g$, i.e., $(-f) \circ g = -(f \circ g)$.

CategoryTheory.Preadditive.comp_neg theorem

: f ≫ (-g) = -f ≫ g

Full source

@[reassoc, simp]
theorem comp_neg : f ≫ (-g) = -f ≫ g :=
  map_neg (leftComp R f) g

Negation of composition in preadditive category: $f \circ (-g) = -(f \circ g)$

Informal description

In a preadditive category, for any morphisms $f$ and $g$, the composition of $f$ with the negation of $g$ equals the negation of the composition of $f$ with $g$, i.e., $f \circ (-g) = -(f \circ g)$.

CategoryTheory.Preadditive.neg_comp_neg theorem

: (-f) ≫ (-g) = f ≫ g

Full source

@[reassoc]
theorem neg_comp_neg : (-f) ≫ (-g) = f ≫ g := by simp

Composition of Negated Morphisms: $(-f) \circ (-g) = f \circ g$

Informal description

In a preadditive category, for any morphisms $f$ and $g$, the composition of the negation of $f$ with the negation of $g$ equals the composition of $f$ with $g$, i.e., $(-f) \circ (-g) = f \circ g$.

CategoryTheory.Preadditive.nsmul_comp theorem

(n : ℕ) : (n • f) ≫ g = n • f ≫ g

Full source

theorem nsmul_comp (n : ℕ) : (n • f) ≫ g = n • f ≫ g :=
  map_nsmul (rightComp P g) n f

Natural scalar multiple of composition in preadditive category: $(n \cdot f) \circ g = n \cdot (f \circ g)$

Informal description

In a preadditive category, for any natural number $n$ and morphisms $f$ and $g$, the composition of the $n$-th scalar multiple of $f$ with $g$ is equal to the $n$-th scalar multiple of the composition $f \circ g$, i.e., $(n \cdot f) \circ g = n \cdot (f \circ g)$.

CategoryTheory.Preadditive.comp_nsmul theorem

(n : ℕ) : f ≫ (n • g) = n • f ≫ g

Full source

theorem comp_nsmul (n : ℕ) : f ≫ (n • g) = n • f ≫ g :=
  map_nsmul (leftComp R f) n g

Linearity of composition with respect to scalar multiplication in preadditive categories

Informal description

In a preadditive category, for any natural number $n$ and morphisms $f$ and $g$, the composition of $f$ with the $n$-th scalar multiple of $g$ is equal to the $n$-th scalar multiple of the composition of $f$ with $g$, i.e., $f \circ (n \cdot g) = n \cdot (f \circ g)$.

CategoryTheory.Preadditive.zsmul_comp theorem

(n : ℤ) : (n • f) ≫ g = n • f ≫ g

Full source

theorem zsmul_comp (n : ℤ) : (n • f) ≫ g = n • f ≫ g :=
  map_zsmul (rightComp P g) n f

Linearity of composition with respect to integer scalar multiplication in preadditive categories: $(n \cdot f) \circ g = n \cdot (f \circ g)$

Informal description

In a preadditive category, for any integer $n$ and morphisms $f$ and $g$, the composition of the $n$-th integer scalar multiple of $f$ with $g$ is equal to the $n$-th integer scalar multiple of the composition $f \circ g$, i.e., $(n \cdot f) \circ g = n \cdot (f \circ g)$.

CategoryTheory.Preadditive.comp_zsmul theorem

(n : ℤ) : f ≫ (n • g) = n • f ≫ g

Full source

theorem comp_zsmul (n : ℤ) : f ≫ (n • g) = n • f ≫ g :=
  map_zsmul (leftComp R f) n g

Linearity of composition with respect to integer scalar multiplication in preadditive categories

Informal description

In a preadditive category, for any integer $n$ and morphisms $f$ and $g$, the composition of $f$ with the $n$-th integer multiple of $g$ is equal to the $n$-th integer multiple of the composition of $f$ with $g$, i.e., $f \circ (n \cdot g) = n \cdot (f \circ g)$.

CategoryTheory.Preadditive.comp_sum theorem

 {P Q R : C} {J : Type*} (s : Finset J) (f : P ⟶ Q) (g : J → (Q ⟶ R)) : (f ≫ ∑ j ∈ s, g j) = ∑ j ∈ s, f ≫ g j

Full source

@[reassoc]
theorem comp_sum {P Q R : C} {J : Type*} (s : Finset J) (f : P ⟶ Q) (g : J → (Q ⟶ R)) :
    (f ≫ ∑ j ∈ s, g j) = ∑ j ∈ s, f ≫ g j :=
  map_sum (leftComp R f) _ _

Linearity of Composition with Respect to Finite Sums in Preadditive Categories

Informal description

Let $ C $ be a preadditive category, and let $ P, Q, R $ be objects in $ C $. Given a finite index set $ J $, a morphism $ f : P \to Q $, and a family of morphisms $ g_j : Q \to R $ indexed by $ j \in J $, the composition of $ f $ with the sum of the $ g_j $ is equal to the sum of the compositions $ f \circ g_j $. In symbols: \[ f \circ \left( \sum_{j \in J} g_j \right) = \sum_{j \in J} (f \circ g_j). \]

CategoryTheory.Preadditive.sum_comp theorem

 {P Q R : C} {J : Type*} (s : Finset J) (f : J → (P ⟶ Q)) (g : Q ⟶ R) : (∑ j ∈ s, f j) ≫ g = ∑ j ∈ s, f j ≫ g

Full source

@[reassoc]
theorem sum_comp {P Q R : C} {J : Type*} (s : Finset J) (f : J → (P ⟶ Q)) (g : Q ⟶ R) :
    (∑ j ∈ s, f j) ≫ g = ∑ j ∈ s, f j ≫ g :=
  map_sum (rightComp P g) _ _

Linearity of Composition with Respect to Finite Sums in Preadditive Categories

Informal description

Let $C$ be a preadditive category, and let $P, Q, R$ be objects in $C$. Given a finite set $J$ indexed by a type $J$, a family of morphisms $f_j \colon P \to Q$ for each $j \in J$, and a morphism $g \colon Q \to R$, the composition of the sum of the $f_j$ with $g$ is equal to the sum of the compositions of each $f_j$ with $g$. In other words, \[ \left(\sum_{j \in J} f_j\right) \circ g = \sum_{j \in J} (f_j \circ g). \]

CategoryTheory.Preadditive.sum_comp' theorem

 {P Q R S : C} {J : Type*} (s : Finset J) (f : J → (P ⟶ Q)) (g : J → (Q ⟶ R)) (h : R ⟶ S) :
  (∑ j ∈ s, f j ≫ g j) ≫ h = ∑ j ∈ s, f j ≫ g j ≫ h

Full source

@[reassoc]
theorem sum_comp' {P Q R S : C} {J : Type*} (s : Finset J) (f : J → (P ⟶ Q)) (g : J → (Q ⟶ R))
    (h : R ⟶ S) : (∑ j ∈ s, f j ≫ g j) ≫ h = ∑ j ∈ s, f j ≫ g j ≫ h := by
  simp only [← Category.assoc]
  apply sum_comp

Bilinearity of Composition with Respect to Finite Sums in Preadditive Categories

Informal description

Let $C$ be a preadditive category, and let $P, Q, R, S$ be objects in $C$. Given a finite index set $J$, families of morphisms $f_j \colon P \to Q$ and $g_j \colon Q \to R$ for each $j \in J$, and a morphism $h \colon R \to S$, the composition of the sum of the compositions $f_j \circ g_j$ with $h$ is equal to the sum of the compositions $f_j \circ g_j \circ h$. In symbols: \[ \left(\sum_{j \in J} (f_j \circ g_j)\right) \circ h = \sum_{j \in J} (f_j \circ g_j \circ h). \]

CategoryTheory.Preadditive.instEpiNegHom instance

{P Q : C} {f : P ⟶ Q} [Epi f] : Epi (-f)

Full source

instance {P Q : C} {f : P ⟶ Q} [Epi f] : Epi (-f) :=
  ⟨fun g g' H => by rwa [neg_comp, neg_comp, ← comp_neg, ← comp_neg, cancel_epi, neg_inj] at H⟩

Negation Preserves Epimorphisms in Preadditive Categories

Informal description

In a preadditive category, if a morphism $f \colon P \to Q$ is an epimorphism, then its negation $-f$ is also an epimorphism.

CategoryTheory.Preadditive.instMonoNegHom instance

{P Q : C} {f : P ⟶ Q} [Mono f] : Mono (-f)

Full source

instance {P Q : C} {f : P ⟶ Q} [Mono f] : Mono (-f) :=
  ⟨fun g g' H => by rwa [comp_neg, comp_neg, ← neg_comp, ← neg_comp, cancel_mono, neg_inj] at H⟩

Negation Preserves Monomorphisms in Preadditive Categories

Informal description

In a preadditive category, if a morphism $f \colon P \to Q$ is a monomorphism, then its negation $-f$ is also a monomorphism.

CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instance

: HasZeroMorphisms C

Full source

instance (priority := 100) preadditiveHasZeroMorphisms : HasZeroMorphisms C where
  zero := inferInstance
  comp_zero f R := show leftComp R f 0 = 0 from map_zero _
  zero_comp P _ _ f := show rightComp P f 0 = 0 from map_zero _

Preadditive Categories Have Zero Morphisms

Informal description

Every preadditive category $C$ has zero morphisms. That is, for every pair of objects $X$ and $Y$ in $C$, there exists a morphism $0 \colon X \to Y$ such that for any morphisms $f$ and $g$ in $C$, the compositions $f \circ 0$ and $0 \circ g$ are also zero morphisms.

CategoryTheory.Preadditive.instSemiringEnd instance

{X : C} : Semiring (End X)

Full source

/-- Porting note: adding this before the ring instance allowed moduleEndRight to find
the correct Monoid structure on End. Moved both down after preadditiveHasZeroMorphisms
to make use of them -/
instance {X : C} : Semiring (End X) :=
  { End.monoid with
    zero_mul := fun f => by dsimp [mul]; exact HasZeroMorphisms.comp_zero f _
    mul_zero := fun f => by dsimp [mul]; exact HasZeroMorphisms.zero_comp _ f
    left_distrib := fun f g h => Preadditive.add_comp X X X g h f
    right_distrib := fun f g h => Preadditive.comp_add X X X h f g }

Semiring Structure on Endomorphisms in a Preadditive Category

Informal description

For any object $X$ in a preadditive category $C$, the endomorphisms $\text{End}(X)$ form a semiring under composition and addition of morphisms. The semiring structure consists of: - Addition given by the abelian group structure on $\text{Hom}(X,X)$ - Multiplication given by composition of morphisms - Additive identity given by the zero morphism - Multiplicative identity given by the identity morphism

CategoryTheory.Preadditive.instRingEnd instance

{X : C} : Ring (End X)

Full source

/-- Porting note: It looks like Ring's parent classes changed in
Lean 4 so the previous instance needed modification. Was following my nose here. -/
instance {X : C} : Ring (End X) :=
  { (inferInstance : Semiring (End X)),
    (inferInstance : AddCommGroup (End X)) with
    neg_add_cancel := neg_add_cancel }

Ring Structure on Endomorphisms in a Preadditive Category

Informal description

For any object $X$ in a preadditive category $C$, the endomorphisms $\text{End}(X)$ form a ring under composition and addition of morphisms. The ring structure consists of: - Addition given by the abelian group structure on $\text{Hom}(X,X)$ - Multiplication given by composition of morphisms - Additive identity given by the zero morphism - Multiplicative identity given by the identity morphism

CategoryTheory.Preadditive.moduleEndRight instance

{X Y : C} : Module (End Y) (X ⟶ Y)

Full source

instance moduleEndRight {X Y : C} : Module (End Y) (X ⟶ Y) where
  smul_add _ _ _ := add_comp _ _ _ _ _ _
  smul_zero _ := zero_comp
  add_smul _ _ _ := comp_add _ _ _ _ _ _
  zero_smul _ := comp_zero

Right Module Structure on Morphisms via Endomorphism Ring

Informal description

For any objects $X$ and $Y$ in a preadditive category $C$, the abelian group of morphisms $X \to Y$ has a right module structure over the endomorphism ring $\text{End}(Y)$, where the action is given by postcomposition with endomorphisms of $Y$.

CategoryTheory.Preadditive.mono_of_cancel_zero theorem

{Q R : C} (f : Q ⟶ R) (h : ∀ {P : C} (g : P ⟶ Q), g ≫ f = 0 → g = 0) : Mono f

Full source

theorem mono_of_cancel_zero {Q R : C} (f : Q ⟶ R) (h : ∀ {P : C} (g : P ⟶ Q), g ≫ f = 0 → g = 0) :
    Mono f where
  right_cancellation := fun {Z} g₁ g₂ hg =>
    sub_eq_zero.1 <| h _ <| (map_sub (rightComp Z f) g₁ g₂).trans <| sub_eq_zero.2 hg

Monomorphism Criterion via Zero Cancellation in Preadditive Categories

Informal description

Let $ C $ be a preadditive category, and let $ f : Q \to R $ be a morphism in $ C $. If for every object $ P $ and every morphism $ g : P \to Q $, the composition $ g \circ f = 0 $ implies $ g = 0 $, then $ f $ is a monomorphism.

CategoryTheory.Preadditive.mono_iff_cancel_zero theorem

{Q R : C} (f : Q ⟶ R) : Mono f ↔ ∀ (P : C) (g : P ⟶ Q), g ≫ f = 0 → g = 0

Full source

theorem mono_iff_cancel_zero {Q R : C} (f : Q ⟶ R) :
    MonoMono f ↔ ∀ (P : C) (g : P ⟶ Q), g ≫ f = 0 → g = 0 :=
  ⟨fun _ _ _ => zero_of_comp_mono _, mono_of_cancel_zero f⟩

Monomorphism Criterion in Preadditive Categories via Zero Cancellation

Informal description

Let $C$ be a preadditive category and $f : Q \to R$ a morphism in $C$. Then $f$ is a monomorphism if and only if for every object $P$ and every morphism $g : P \to Q$, the composition $g \circ f = 0$ implies $g = 0$.

CategoryTheory.Preadditive.mono_of_kernel_zero theorem

{X Y : C} {f : X ⟶ Y} [HasLimit (parallelPair f 0)] (w : kernel.ι f = 0) : Mono f

Full source

theorem mono_of_kernel_zero {X Y : C} {f : X ⟶ Y} [HasLimit (parallelPair f 0)]
    (w : kernel.ι f = 0) : Mono f :=
  mono_of_cancel_zero f fun g h => by rw [← kernel.lift_ι f g h, w, Limits.comp_zero]

Monomorphism Criterion via Zero Kernel in Preadditive Categories

Informal description

Let $ C $ be a preadditive category, and let $ f : X \to Y $ be a morphism in $ C $. Suppose that the kernel of $ f $ exists (i.e., the limit of the parallel pair $ f $ and $ 0 $) and that the kernel inclusion morphism $ \iota $ is equal to the zero morphism. Then $ f $ is a monomorphism.

CategoryTheory.Preadditive.mono_of_isZero_kernel' theorem

{X Y : C} {f : X ⟶ Y} (c : KernelFork f) (hc : IsLimit c) (h : IsZero c.pt) : Mono f

Full source

lemma mono_of_isZero_kernel' {X Y : C} {f : X ⟶ Y} (c : KernelFork f) (hc : IsLimit c)
    (h : IsZero c.pt) : Mono f := mono_of_cancel_zero _ (fun g hg => by
  obtain ⟨a, ha⟩ := KernelFork.IsLimit.lift' hc _ hg
  rw [← ha, h.eq_of_tgt a 0, Limits.zero_comp])

Monomorphism Criterion via Zero Kernel Fork in Preadditive Categories

Informal description

Let $\mathcal{C}$ be a preadditive category and $f : X \to Y$ a morphism in $\mathcal{C}$. Given a kernel fork $c$ of $f$ that is a limit cone (i.e., $hc : \text{IsLimit } c$) and whose apex $c.\text{pt}$ is a zero object (i.e., $h : \text{IsZero } c.\text{pt}$), then $f$ is a monomorphism.

CategoryTheory.Preadditive.mono_of_isZero_kernel theorem

{X Y : C} (f : X ⟶ Y) [HasKernel f] (h : IsZero (kernel f)) : Mono f

Full source

lemma mono_of_isZero_kernel {X Y : C} (f : X ⟶ Y) [HasKernel f] (h : IsZero (kernel f)) :
    Mono f :=
  mono_of_isZero_kernel' _ (kernelIsKernel _) h

Monomorphism Criterion via Zero Kernel in Preadditive Categories

Informal description

Let $\mathcal{C}$ be a preadditive category and $f : X \to Y$ a morphism in $\mathcal{C}$. If the kernel of $f$ exists and is a zero object, then $f$ is a monomorphism.

CategoryTheory.Preadditive.epi_of_cancel_zero theorem

{P Q : C} (f : P ⟶ Q) (h : ∀ {R : C} (g : Q ⟶ R), f ≫ g = 0 → g = 0) : Epi f

Full source

theorem epi_of_cancel_zero {P Q : C} (f : P ⟶ Q) (h : ∀ {R : C} (g : Q ⟶ R), f ≫ g = 0 → g = 0) :
    Epi f :=
  ⟨fun {Z} g g' hg =>
    sub_eq_zero.1 <| h _ <| (map_sub (leftComp Z f) g g').trans <| sub_eq_zero.2 hg⟩

Epimorphism Criterion via Zero Cancellation in Preadditive Categories

Informal description

Let $C$ be a preadditive category and $f : P \to Q$ a morphism in $C$. If for every object $R$ and every morphism $g : Q \to R$, the composition $f \circ g = 0$ implies $g = 0$, then $f$ is an epimorphism.

CategoryTheory.Preadditive.epi_iff_cancel_zero theorem

{P Q : C} (f : P ⟶ Q) : Epi f ↔ ∀ (R : C) (g : Q ⟶ R), f ≫ g = 0 → g = 0

Full source

theorem epi_iff_cancel_zero {P Q : C} (f : P ⟶ Q) :
    EpiEpi f ↔ ∀ (R : C) (g : Q ⟶ R), f ≫ g = 0 → g = 0 :=
  ⟨fun _ _ _ => zero_of_epi_comp _, epi_of_cancel_zero f⟩

Epimorphism Criterion via Zero Cancellation in Preadditive Categories

Informal description

Let $C$ be a preadditive category and $f : P \to Q$ a morphism in $C$. Then $f$ is an epimorphism if and only if for every object $R$ and every morphism $g : Q \to R$, the composition $f \circ g = 0$ implies $g = 0$.

CategoryTheory.Preadditive.epi_of_cokernel_zero theorem

{X Y : C} {f : X ⟶ Y} [HasColimit (parallelPair f 0)] (w : cokernel.π f = 0) : Epi f

Full source

theorem epi_of_cokernel_zero {X Y : C} {f : X ⟶ Y} [HasColimit (parallelPair f 0)]
    (w : cokernel.π f = 0) : Epi f :=
  epi_of_cancel_zero f fun g h => by rw [← cokernel.π_desc f g h, w, Limits.zero_comp]

Epimorphism Criterion via Zero Cokernel in Preadditive Categories

Informal description

Let $ C $ be a preadditive category and $ f : X \to Y $ a morphism in $ C $. If the cokernel of $ f $ exists and its projection morphism $ \pi : Y \to \text{cokernel}(f) $ is the zero morphism, then $ f $ is an epimorphism.

CategoryTheory.Preadditive.epi_of_isZero_cokernel' theorem

{X Y : C} {f : X ⟶ Y} (c : CokernelCofork f) (hc : IsColimit c) (h : IsZero c.pt) : Epi f

Full source

lemma epi_of_isZero_cokernel' {X Y : C} {f : X ⟶ Y} (c : CokernelCofork f) (hc : IsColimit c)
    (h : IsZero c.pt) : Epi f := epi_of_cancel_zero _ (fun g hg => by
  obtain ⟨a, ha⟩ := CokernelCofork.IsColimit.desc' hc _ hg
  rw [← ha, h.eq_of_src a 0, Limits.comp_zero])

Epimorphism Criterion via Zero Vertex Cokernel Cofork in Preadditive Categories

Informal description

Let $ C $ be a preadditive category and $ f : X \to Y $ a morphism in $ C $. Given a cokernel cofork $ c $ of $ f $ that is a colimit cocone, if the vertex $ c.pt $ of the cofork is a zero object, then $ f $ is an epimorphism.

CategoryTheory.Preadditive.epi_of_isZero_cokernel theorem

{X Y : C} (f : X ⟶ Y) [HasCokernel f] (h : IsZero (cokernel f)) : Epi f

Full source

lemma epi_of_isZero_cokernel {X Y : C} (f : X ⟶ Y) [HasCokernel f] (h : IsZero (cokernel f)) :
    Epi f :=
  epi_of_isZero_cokernel' _ (cokernelIsCokernel _) h

Epimorphism Criterion via Zero Cokernel in Preadditive Categories

Informal description

Let $ C $ be a preadditive category and $ f : X \to Y $ a morphism in $ C $. If the cokernel of $ f $ exists and is a zero object, then $ f $ is an epimorphism.

CategoryTheory.Preadditive.IsIso.comp_left_eq_zero theorem

[IsIso f] : f ≫ g = 0 ↔ g = 0

Full source

@[simp]
theorem comp_left_eq_zero [IsIso f] : f ≫ gf ≫ g = 0 ↔ g = 0 := by
  rw [← IsIso.eq_inv_comp, Limits.comp_zero]

Left Composition with Isomorphism Yields Zero if and only if Original Morphism is Zero

Informal description

Let $C$ be a preadditive category, and let $f \colon X \to Y$ and $g \colon Y \to Z$ be morphisms in $C$. If $f$ is an isomorphism, then the composition $f \circ g$ is the zero morphism if and only if $g$ is the zero morphism, i.e., $f \circ g = 0 \leftrightarrow g = 0$.

CategoryTheory.Preadditive.IsIso.comp_right_eq_zero theorem

[IsIso g] : f ≫ g = 0 ↔ f = 0

Full source

@[simp]
theorem comp_right_eq_zero [IsIso g] : f ≫ gf ≫ g = 0 ↔ f = 0 := by
  rw [← IsIso.eq_comp_inv, Limits.zero_comp]

Right Composition with Isomorphism Yields Zero if and only if Original Morphism is Zero

Informal description

Let $C$ be a preadditive category, and let $f \colon X \to Y$ and $g \colon Y \to Z$ be morphisms in $C$. If $g$ is an isomorphism, then the composition $f \circ g$ is the zero morphism if and only if $f$ is the zero morphism, i.e., $f \circ g = 0 \leftrightarrow f = 0$.

CategoryTheory.Preadditive.mono_of_kernel_iso_zero theorem

{X Y : C} {f : X ⟶ Y} [HasLimit (parallelPair f 0)] (w : kernel f ≅ 0) : Mono f

Full source

theorem mono_of_kernel_iso_zero {X Y : C} {f : X ⟶ Y} [HasLimit (parallelPair f 0)]
    (w : kernelkernel f ≅ 0) : Mono f :=
  mono_of_kernel_zero (zero_of_source_iso_zero _ w)

Monomorphism Criterion via Zero Kernel Isomorphism in Preadditive Categories

Informal description

Let $C$ be a preadditive category, and let $f : X \to Y$ be a morphism in $C$. Suppose the kernel of $f$ exists (i.e., the limit of the parallel pair $(f, 0)$ exists) and is isomorphic to the zero object. Then $f$ is a monomorphism.

CategoryTheory.Preadditive.epi_of_cokernel_iso_zero theorem

{X Y : C} {f : X ⟶ Y} [HasColimit (parallelPair f 0)] (w : cokernel f ≅ 0) : Epi f

Full source

theorem epi_of_cokernel_iso_zero {X Y : C} {f : X ⟶ Y} [HasColimit (parallelPair f 0)]
    (w : cokernelcokernel f ≅ 0) : Epi f :=
  epi_of_cokernel_zero (zero_of_target_iso_zero _ w)

Epimorphism Criterion via Zero Cokernel in Preadditive Categories

Informal description

Let $\mathcal{C}$ be a preadditive category and $f : X \to Y$ a morphism in $\mathcal{C}$. If the cokernel of $f$ exists and is isomorphic to the zero object, then $f$ is an epimorphism.

CategoryTheory.Preadditive.forkOfKernelFork definition

(c : KernelFork (f - g)) : Fork f g

Full source

/-- Map a kernel cone on the difference of two morphisms to the equalizer fork. -/
@[simps! pt]
def forkOfKernelFork (c : KernelFork (f - g)) : Fork f g :=
  Fork.ofι c.ι <| by rw [← sub_eq_zero, ← comp_sub, c.condition]

Equalizer fork from kernel fork of difference morphism

Informal description

Given a kernel fork $c$ of the difference $f - g$ of two parallel morphisms $f, g : X \to Y$ in a preadditive category, the function `forkOfKernelFork` constructs an equalizer fork for $f$ and $g$ using the inclusion morphism $\iota_c$ of the kernel fork. The construction ensures that the inclusion morphism satisfies $\iota_c \circ f = \iota_c \circ g$ by utilizing the condition that $\iota_c \circ (f - g) = 0$ in the kernel fork.

CategoryTheory.Preadditive.forkOfKernelFork_ι theorem

(c : KernelFork (f - g)) : (forkOfKernelFork c).ι = c.ι

Full source

@[simp]
theorem forkOfKernelFork_ι (c : KernelFork (f - g)) : (forkOfKernelFork c).ι = c.ι :=
  rfl

Inclusion Morphism Equality in Fork Construction from Kernel Fork

Informal description

Given a kernel fork $c$ of the difference morphism $f - g$ in a preadditive category, the inclusion morphism $\iota$ of the equalizer fork constructed from $c$ is equal to the inclusion morphism of $c$, i.e., $\iota_{\text{forkOfKernelFork}(c)} = \iota_c$.

CategoryTheory.Preadditive.kernelForkOfFork definition

(c : Fork f g) : KernelFork (f - g)

Full source

/-- Map any equalizer fork to a cone on the difference of the two morphisms. -/
def kernelForkOfFork (c : Fork f g) : KernelFork (f - g) :=
  Fork.ofι c.ι <| by rw [comp_sub, comp_zero, sub_eq_zero, c.condition]

Kernel fork construction from a fork in a preadditive category

Informal description

Given a fork $c$ on two parallel morphisms $f, g : X \to Y$ in a preadditive category, the function `kernelForkOfFork` constructs a kernel fork of the difference morphism $f - g$. Specifically, the kernel fork has the same vertex and inclusion morphism as the original fork $c$, and satisfies the condition that the composition of the inclusion morphism with $f - g$ is zero.

CategoryTheory.Preadditive.kernelForkOfFork_ι theorem

(c : Fork f g) : (kernelForkOfFork c).ι = c.ι

Full source

@[simp]
theorem kernelForkOfFork_ι (c : Fork f g) : (kernelForkOfFork c).ι = c.ι :=
  rfl

Inclusion Morphism Equality in Kernel Fork Construction from Fork

Informal description

Given a fork $c$ on two parallel morphisms $f, g : X \to Y$ in a preadditive category, the inclusion morphism $\iota$ of the kernel fork constructed from $c$ is equal to the inclusion morphism of $c$, i.e., $\iota_{\text{kernelForkOfFork}(c)} = \iota_c$.

CategoryTheory.Preadditive.kernelForkOfFork_ofι theorem

{P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) : kernelForkOfFork (Fork.ofι ι w) = KernelFork.ofι ι (by simp [w])

Full source

@[simp]
theorem kernelForkOfFork_ofι {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) :
    kernelForkOfFork (Fork.ofι ι w) = KernelFork.ofι ι (by simp [w]) :=
  rfl

Equality of Kernel Forks Constructed from Parallel Condition in Preadditive Category

Informal description

Given a preadditive category $\mathcal{C}$, objects $P, X, Y$ in $\mathcal{C}$, and morphisms $f, g : X \to Y$, for any morphism $\iota : P \to X$ satisfying $\iota \circ f = \iota \circ g$, the kernel fork constructed from the fork $(Fork.of\ \iota\ w)$ is equal to the kernel fork $(KernelFork.of\ \iota\ h)$, where $h$ is the proof that $\iota \circ (f - g) = 0$ obtained by simplifying the condition $w$.

CategoryTheory.Preadditive.isLimitForkOfKernelFork definition

{c : KernelFork (f - g)} (i : IsLimit c) : IsLimit (forkOfKernelFork c)

Full source

/-- A kernel of `f - g` is an equalizer of `f` and `g`. -/
def isLimitForkOfKernelFork {c : KernelFork (f - g)} (i : IsLimit c) :
    IsLimit (forkOfKernelFork c) :=
  Fork.IsLimit.mk' _ fun s =>
    ⟨i.lift (kernelForkOfFork s), i.fac _ _, fun h => by apply Fork.IsLimit.hom_ext i; aesop_cat⟩

Limit cone property of equalizer fork from kernel fork in preadditive categories

Informal description

Given a kernel fork $c$ of the difference morphism $f - g$ in a preadditive category, if $c$ is a limit cone, then the corresponding equalizer fork constructed from $c$ is also a limit cone. Specifically, for any fork $s$ of $f$ and $g$, there exists a unique morphism from $s$ to the equalizer fork that commutes with the inclusion morphisms.

CategoryTheory.Preadditive.isLimitForkOfKernelFork_lift theorem

 {c : KernelFork (f - g)} (i : IsLimit c) (s : Fork f g) :
  (isLimitForkOfKernelFork i).lift s = i.lift (kernelForkOfFork s)

Full source

@[simp]
theorem isLimitForkOfKernelFork_lift {c : KernelFork (f - g)} (i : IsLimit c) (s : Fork f g) :
    (isLimitForkOfKernelFork i).lift s = i.lift (kernelForkOfFork s) :=
  rfl

Lift of Fork to Equalizer via Kernel Fork in Preadditive Category

Informal description

Given a kernel fork $c$ of the difference morphism $f - g$ in a preadditive category, if $c$ is a limit cone, then for any fork $s$ of $f$ and $g$, the lift of $s$ to the equalizer fork constructed from $c$ is equal to the lift of the kernel fork constructed from $s$ to $c$. That is, the following diagram commutes: \[ \text{lift}_{\text{equalizer}}(s) = \text{lift}_{\text{kernel}}(\text{kernelForkOfFork}(s)) \]

CategoryTheory.Preadditive.isLimitKernelForkOfFork definition

{c : Fork f g} (i : IsLimit c) : IsLimit (kernelForkOfFork c)

Full source

/-- An equalizer of `f` and `g` is a kernel of `f - g`. -/
def isLimitKernelForkOfFork {c : Fork f g} (i : IsLimit c) : IsLimit (kernelForkOfFork c) :=
  Fork.IsLimit.mk' _ fun s =>
    ⟨i.lift (forkOfKernelFork s), i.fac _ _, fun h => by apply Fork.IsLimit.hom_ext i; aesop_cat⟩

Limit cone of kernel fork from equalizer fork in preadditive category

Informal description

Given a fork $c$ on parallel morphisms $f, g : X \to Y$ in a preadditive category, if $c$ is a limit cone (i.e., an equalizer of $f$ and $g$), then the kernel fork of the difference morphism $f - g$ constructed from $c$ is also a limit cone (i.e., a kernel of $f - g$).

CategoryTheory.Preadditive.hasEqualizer_of_hasKernel theorem

[HasKernel (f - g)] : HasEqualizer f g

Full source

/-- A preadditive category has an equalizer for `f` and `g` if it has a kernel for `f - g`. -/
theorem hasEqualizer_of_hasKernel [HasKernel (f - g)] : HasEqualizer f g :=
  HasLimit.mk
    { cone := forkOfKernelFork _
      isLimit := isLimitForkOfKernelFork (equalizerIsEqualizer (f - g) 0) }

Existence of Equalizer from Kernel of Difference in Preadditive Categories

Informal description

In a preadditive category, if there exists a kernel for the difference morphism $f - g$ of two parallel morphisms $f, g : X \to Y$, then there exists an equalizer for $f$ and $g$.

CategoryTheory.Preadditive.hasKernel_of_hasEqualizer theorem

[HasEqualizer f g] : HasKernel (f - g)

Full source

/-- A preadditive category has a kernel for `f - g` if it has an equalizer for `f` and `g`. -/
theorem hasKernel_of_hasEqualizer [HasEqualizer f g] : HasKernel (f - g) :=
  HasLimit.mk
    { cone := kernelForkOfFork (equalizer.fork f g)
      isLimit := isLimitKernelForkOfFork (limit.isLimit (parallelPair f g)) }

Existence of Kernel for Difference Morphism from Equalizer in Preadditive Category

Informal description

In a preadditive category, if there exists an equalizer for two parallel morphisms $f, g : X \to Y$, then there exists a kernel for their difference morphism $f - g$.

CategoryTheory.Preadditive.coforkOfCokernelCofork definition

(c : CokernelCofork (f - g)) : Cofork f g

Full source

/-- Map a cokernel cocone on the difference of two morphisms to the coequalizer cofork. -/
@[simps! pt]
def coforkOfCokernelCofork (c : CokernelCofork (f - g)) : Cofork f g :=
  Cofork.ofπ c.π <| by rw [← sub_eq_zero, ← sub_comp, c.condition]

Cofork construction from a cokernel cofork of the difference of two morphisms

Informal description

Given a cokernel cofork $ c $ of the difference $ f - g $ of two morphisms $ f, g : X \to Y $ in a preadditive category, the construction `coforkOfCokernelCofork` produces a cofork on the parallel pair $ f, g $. The cofork's projection morphism is the same as the projection morphism of the original cokernel cofork $ c $, and it satisfies the coequalizer condition $ f \circ \pi = g \circ \pi $.

CategoryTheory.Preadditive.coforkOfCokernelCofork_π theorem

(c : CokernelCofork (f - g)) : (coforkOfCokernelCofork c).π = c.π

Full source

@[simp]
theorem coforkOfCokernelCofork_π (c : CokernelCofork (f - g)) :
    (coforkOfCokernelCofork c).π = c.π :=
  rfl

Equality of Projection Morphisms in Cofork Construction from Cokernel Cofork

Informal description

Given a cokernel cofork $c$ of the difference $f - g$ of two morphisms $f, g : X \to Y$ in a preadditive category, the projection morphism $\pi$ of the cofork constructed from $c$ (via `coforkOfCokernelCofork`) is equal to the projection morphism $\pi$ of $c$.

CategoryTheory.Preadditive.cokernelCoforkOfCofork definition

(c : Cofork f g) : CokernelCofork (f - g)

Full source

/-- Map any coequalizer cofork to a cocone on the difference of the two morphisms. -/
def cokernelCoforkOfCofork (c : Cofork f g) : CokernelCofork (f - g) :=
  Cofork.ofπ c.π <| by rw [sub_comp, zero_comp, sub_eq_zero, c.condition]

Cokernel cofork from a cofork on parallel morphisms

Informal description

Given a cofork $ c $ on parallel morphisms $ f, g : X \to Y $ in a preadditive category, the construction `cokernelCoforkOfCofork` produces a cokernel cofork of the morphism $ f - g $. Specifically, it maps the cofork $ c $ to a cokernel cofork with the same projection morphism $ \pi : Y \to c.pt $ satisfying $ (f - g) \circ \pi = 0 $.

CategoryTheory.Preadditive.cokernelCoforkOfCofork_π theorem

(c : Cofork f g) : (cokernelCoforkOfCofork c).π = c.π

Full source

@[simp]
theorem cokernelCoforkOfCofork_π (c : Cofork f g) : (cokernelCoforkOfCofork c).π = c.π :=
  rfl

Equality of Projection Morphisms in Cokernel Cofork Construction from Cofork

Informal description

Given a cofork $c$ on parallel morphisms $f, g : X \to Y$ in a preadditive category, the projection morphism $\pi$ of the cokernel cofork constructed from $c$ (via `cokernelCoforkOfCofork`) is equal to the projection morphism $\pi$ of $c$.

CategoryTheory.Preadditive.cokernelCoforkOfCofork_ofπ theorem

 {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) : cokernelCoforkOfCofork (Cofork.ofπ π w) = CokernelCofork.ofπ π (by simp [w])

Full source

@[simp]
theorem cokernelCoforkOfCofork_ofπ {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) :
    cokernelCoforkOfCofork (Cofork.ofπ π w) = CokernelCofork.ofπ π (by simp [w]) :=
  rfl

Cokernel Cofork Construction from Cofork Condition in Preadditive Category

Informal description

Given an object $P$ in a preadditive category $\mathcal{C}$ and a morphism $\pi: Y \to P$ such that $f \circ \pi = g \circ \pi$, the cokernel cofork constructed from the cofork $(P, \pi, w)$ is equal to the cokernel cofork of $\pi$ with the condition $(f - g) \circ \pi = 0$ (which follows from $w$ via simplification).

CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork definition

{c : CokernelCofork (f - g)} (i : IsColimit c) : IsColimit (coforkOfCokernelCofork c)

Full source

/-- A cokernel of `f - g` is a coequalizer of `f` and `g`. -/
def isColimitCoforkOfCokernelCofork {c : CokernelCofork (f - g)} (i : IsColimit c) :
    IsColimit (coforkOfCokernelCofork c) :=
  Cofork.IsColimit.mk' _ fun s =>
    ⟨i.desc (cokernelCoforkOfCofork s), i.fac _ _, fun h => by
      apply Cofork.IsColimit.hom_ext i; aesop_cat⟩

Colimit property of cofork constructed from cokernel cofork in preadditive categories

Informal description

Given a cokernel cofork $ c $ of the difference $ f - g $ of two morphisms $ f, g : X \to Y $ in a preadditive category, if $ c $ is a colimit cocone, then the cofork constructed from $ c $ (via `coforkOfCokernelCofork`) is also a colimit cocone. Specifically, for any other cofork $ s $ on $ f $ and $ g $, there exists a unique morphism from the vertex of the constructed cofork to the vertex of $ s $ that commutes with the cofork projections.

CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork_desc theorem

 {c : CokernelCofork (f - g)} (i : IsColimit c) (s : Cofork f g) :
  (isColimitCoforkOfCokernelCofork i).desc s = i.desc (cokernelCoforkOfCofork s)

Full source

@[simp]
theorem isColimitCoforkOfCokernelCofork_desc {c : CokernelCofork (f - g)} (i : IsColimit c)
    (s : Cofork f g) :
    (isColimitCoforkOfCokernelCofork i).desc s = i.desc (cokernelCoforkOfCofork s) :=
  rfl

Uniqueness of Descending Morphism for Cofork Constructed from Cokernel Cofork in Preadditive Categories

Informal description

Let $\mathcal{C}$ be a preadditive category, and let $f, g : X \to Y$ be parallel morphisms in $\mathcal{C}$. Given a cokernel cofork $c$ of $f - g$ that is a colimit cocone (i.e., $c$ is a colimit of the cokernel diagram of $f - g$), and given any other cofork $s$ on $f$ and $g$, the unique morphism $(isColimitCoforkOfCokernelCofork \, i).desc \, s$ from the vertex of the cofork constructed from $c$ to the vertex of $s$ is equal to the unique morphism $i.desc \, (cokernelCoforkOfCofork \, s)$ induced by the colimit property of $c$.

CategoryTheory.Preadditive.isColimitCokernelCoforkOfCofork definition

{c : Cofork f g} (i : IsColimit c) : IsColimit (cokernelCoforkOfCofork c)

Full source

/-- A coequalizer of `f` and `g` is a cokernel of `f - g`. -/
def isColimitCokernelCoforkOfCofork {c : Cofork f g} (i : IsColimit c) :
    IsColimit (cokernelCoforkOfCofork c) :=
  Cofork.IsColimit.mk' _ fun s =>
    ⟨i.desc (coforkOfCokernelCofork s), i.fac _ _, fun h => by
      apply Cofork.IsColimit.hom_ext i; aesop_cat⟩

Colimit property of cokernel cofork from a colimit cofork

Informal description

Given a cofork $ c $ on parallel morphisms $ f, g : X \to Y $ in a preadditive category, if $ c $ is a colimit cocone, then the corresponding cokernel cofork of $ f - g $ is also a colimit cocone. More precisely, if $ c $ is a colimit cocone for the parallel pair $ f, g $, then the cokernel cofork constructed from $ c $ (via `cokernelCoforkOfCofork`) is a colimit cocone for the morphism $ f - g $.

CategoryTheory.Preadditive.hasCoequalizer_of_hasCokernel theorem

[HasCokernel (f - g)] : HasCoequalizer f g

Full source

/-- A preadditive category has a coequalizer for `f` and `g` if it has a cokernel for `f - g`. -/
theorem hasCoequalizer_of_hasCokernel [HasCokernel (f - g)] : HasCoequalizer f g :=
  HasColimit.mk
    { cocone := coforkOfCokernelCofork _
      isColimit := isColimitCoforkOfCokernelCofork (coequalizerIsCoequalizer (f - g) 0) }

Existence of Coequalizer from Cokernel in Preadditive Categories

Informal description

In a preadditive category, if there exists a cokernel for the morphism $f - g$ (where $f, g : X \to Y$ are parallel morphisms), then there exists a coequalizer for $f$ and $g$.

CategoryTheory.Preadditive.hasCokernel_of_hasCoequalizer theorem

[HasCoequalizer f g] : HasCokernel (f - g)

Full source

/-- A preadditive category has a cokernel for `f - g` if it has a coequalizer for `f` and `g`. -/
theorem hasCokernel_of_hasCoequalizer [HasCoequalizer f g] : HasCokernel (f - g) :=
  HasColimit.mk
    { cocone := cokernelCoforkOfCofork (coequalizer.cofork f g)
      isColimit := isColimitCokernelCoforkOfCofork (colimit.isColimit (parallelPair f g)) }

Existence of Cokernel from Coequalizer in Preadditive Categories

Informal description

In a preadditive category, if there exists a coequalizer for a pair of parallel morphisms $f, g : X \to Y$, then there exists a cokernel for the morphism $f - g$.

CategoryTheory.Preadditive.hasEqualizers_of_hasKernels theorem

[HasKernels C] : HasEqualizers C

Full source

/-- If a preadditive category has all kernels, then it also has all equalizers. -/
theorem hasEqualizers_of_hasKernels [HasKernels C] : HasEqualizers C :=
  @hasEqualizers_of_hasLimit_parallelPair _ _ fun {_} {_} f g => hasEqualizer_of_hasKernel f g

Existence of Equalizers from Kernels in Preadditive Categories

Informal description

In a preadditive category $\mathcal{C}$, if all morphisms have kernels, then $\mathcal{C}$ has all equalizers. That is, for any pair of parallel morphisms $f, g : X \to Y$, there exists an object $E$ and a morphism $\iota : E \to X$ such that $\iota \circ f = \iota \circ g$, and $E$ is universal with this property.

CategoryTheory.Preadditive.hasCoequalizers_of_hasCokernels theorem

[HasCokernels C] : HasCoequalizers C

Full source

/-- If a preadditive category has all cokernels, then it also has all coequalizers. -/
theorem hasCoequalizers_of_hasCokernels [HasCokernels C] : HasCoequalizers C :=
  @hasCoequalizers_of_hasColimit_parallelPair _ _ fun {_} {_} f g =>
    hasCoequalizer_of_hasCokernel f g

Existence of Coequalizers from Cokernels in Preadditive Categories

Informal description

In a preadditive category $\mathcal{C}$, if all cokernels exist, then all coequalizers exist.

CategoryTheory.Preadditive.instSMulUnitsIntIso instance

: SMul (Units ℤ) (X ≅ Y)

Full source

instance : SMul (Units ℤ) (X ≅ Y) where
  smul a e :=
    { hom := (a : ℤ) • e.hom
      inv := ((a⁻¹ : Units ℤ) : ℤ) • e.inv
      hom_inv_id := by
        simp only [comp_zsmul, zsmul_comp, smul_smul, Units.inv_mul, one_smul, e.hom_inv_id]
      inv_hom_id := by
        simp only [comp_zsmul, zsmul_comp, smul_smul, Units.mul_inv, one_smul, e.inv_hom_id] }

Action of Integer Units on Isomorphisms in Preadditive Categories

Informal description

For any two objects $X$ and $Y$ in a preadditive category $\mathcal{C}$, the group of units $\mathbb{Z}^\times$ of the integers acts on the set of isomorphisms $X \cong Y$ by scalar multiplication. Specifically, for any unit $a \in \mathbb{Z}^\times$ and isomorphism $e : X \cong Y$, the action $a \cdot e$ is defined such that $(a \cdot e).\text{hom} = a \cdot e.\text{hom}$ and $(a \cdot e).\text{inv} = a^{-1} \cdot e.\text{inv}$.

CategoryTheory.Preadditive.smul_iso_hom theorem

(a : Units ℤ) (e : X ≅ Y) : (a • e).hom = a • e.hom

Full source

@[simp]
lemma smul_iso_hom (a : Units ℤ) (e : X ≅ Y) : (a • e).hom = a • e.hom := rfl

Action of Integer Units on Isomorphism Homomorphisms: $(a \cdot e).\text{hom} = a \cdot e.\text{hom}$

Informal description

For any unit $a \in \mathbb{Z}^\times$ and any isomorphism $e : X \cong Y$ in a preadditive category $\mathcal{C}$, the homomorphism component of the scalar multiplication $a \cdot e$ is equal to the scalar multiplication $a \cdot e.\text{hom}$.

CategoryTheory.Preadditive.smul_iso_inv theorem

(a : Units ℤ) (e : X ≅ Y) : (a • e).inv = a⁻¹ • e.inv

Full source

@[simp]
lemma smul_iso_inv (a : Units ℤ) (e : X ≅ Y) : (a • e).inv = a⁻¹ • e.inv := rfl

Inverse of Scaled Isomorphism in Preadditive Categories

Informal description

For any unit $a \in \mathbb{Z}^\times$ and any isomorphism $e \colon X \cong Y$ in a preadditive category, the inverse component of the scaled isomorphism $a \cdot e$ is equal to the inverse of $a$ scaled by the inverse component of $e$, i.e., $(a \cdot e)^{-1} = a^{-1} \cdot e^{-1}$.

CategoryTheory.Preadditive.instNegIso instance

: Neg (X ≅ Y)

Full source

instance : Neg (X ≅ Y) where
  neg e :=
    { hom := -e.hom
      inv := -e.inv }

Negation of Isomorphisms in Preadditive Categories

Informal description

For any two objects $X$ and $Y$ in a preadditive category, the abelian group structure on the hom-set $\text{Hom}(X, Y)$ induces a negation operation on isomorphisms between $X$ and $Y$. Specifically, for any isomorphism $e : X \cong Y$, the negation $-e$ is defined such that its homomorphism component is $-e.\text{hom}$.

CategoryTheory.Preadditive.neg_iso_hom theorem

(e : X ≅ Y) : (-e).hom = -e.hom

Full source

@[simp]
lemma neg_iso_hom (e : X ≅ Y) : (-e).hom = -e.hom := rfl

Negation of Isomorphism Homomorphism in Preadditive Categories

Informal description

For any isomorphism $e \colon X \cong Y$ in a preadditive category, the homomorphism component of the negated isomorphism $-e$ is equal to the negation of the homomorphism component of $e$, i.e., $(-e).\text{hom} = -e.\text{hom}$.

CategoryTheory.Preadditive.neg_iso_inv theorem

(e : X ≅ Y) : (-e).inv = -e.inv

Full source

@[simp]
lemma neg_iso_inv (e : X ≅ Y) : (-e).inv = -e.inv := rfl

Negation of Isomorphism Inverses in Preadditive Categories

Informal description

For any isomorphism $e \colon X \cong Y$ in a preadditive category, the inverse of the negated isomorphism $-e$ is equal to the negation of the inverse of $e$, i.e., $(-e)^{-1} = -e^{-1}$.

Mathlib.CategoryTheory.Preadditive.Basic

Main results

Implementation notes

References

Tags