Documentation

TauCeti.CategoryTheory.Linear.CoprimeKernels

An object killed by a product of coprime scalars splits #

Let X be an object of an R-linear category, for a commutative semiring R, such that (m * n) • 𝟙 X = 0, where m and n are coprime elements of R, witnessed by a Bézout identity a * m + b * n = 1. Then X is the binary biproduct of the kernels of m • 𝟙 X and n • 𝟙 X. The inclusions are the kernel inclusions, and the projections are the factorisations of (b * n) • 𝟙 X and (a * m) • 𝟙 X through them. The first is killed by m and the second by n, because X is killed by m * n, and their sum is the identity.

Every preadditive category is ℤ-linear, so this applies to coprime integers m and n. For a commutative group scheme G killed by m * n, this is the decomposition G ≅ G[m] × G[n] into its m-torsion and its n-torsion.

Main definitions #

Main results #

References #

source
@[reducible, inline]
noncomputable abbrev CategoryTheory.Limits.BinaryBicone.ofCoprimeKernelForks {R : Type u_1} [CommSemiring R] {C : Type u_2} [Category.{u_3, u_2} C] [Preadditive C] [Linear R C] {X : C} {a b m n : R} (hab : a * m + b * n = 1) (hX : (m * n) • CategoryStruct.id X = 0) {c₁ : KernelFork (m • CategoryStruct.id X)} (hc₁ : IsLimit c₁) {c₂ : KernelFork (n • CategoryStruct.id X)} (hc₂ : IsLimit c₂) :
BinaryBicone c₁.pt c₂.pt

The splitting of an object killed by a product of coprime scalars. Let X satisfy (m * n) • 𝟙 X = 0, where a * m + b * n = 1, and let c₁ and c₂ be limit kernel forks of m • 𝟙 X and n • 𝟙 X. This is the binary bicone with vertex X whose inclusions are the kernel inclusions c₁.ι and c₂.ι, and whose projections are the factorisations of (b * n) • 𝟙 X through c₁ and of (a * m) • 𝟙 X through c₂. It is a bilimit (BinaryBicone.isBilimitOfCoprimeKernelForks).

Instances For
    source
    @[simp]
    theorem CategoryTheory.Limits.BinaryBicone.ofCoprimeKernelForks_inr {R : Type u_1} [CommSemiring R] {C : Type u_2} [Category.{u_3, u_2} C] [Preadditive C] [Linear R C] {X : C} {a b m n : R} (hab : a * m + b * n = 1) (hX : (m * n) • CategoryStruct.id X = 0) {c₁ : KernelFork (m • CategoryStruct.id X)} (hc₁ : IsLimit c₁) {c₂ : KernelFork (n • CategoryStruct.id X)} (hc₂ : IsLimit c₂) :
    (ofCoprimeKernelForks hab hX hc₁ hc₂).inr = Fork.ι c₂
    source
    @[simp]
    theorem CategoryTheory.Limits.BinaryBicone.ofCoprimeKernelForks_pt {R : Type u_1} [CommSemiring R] {C : Type u_2} [Category.{u_3, u_2} C] [Preadditive C] [Linear R C] {X : C} {a b m n : R} (hab : a * m + b * n = 1) (hX : (m * n) • CategoryStruct.id X = 0) {c₁ : KernelFork (m • CategoryStruct.id X)} (hc₁ : IsLimit c₁) {c₂ : KernelFork (n • CategoryStruct.id X)} (hc₂ : IsLimit c₂) :
    (ofCoprimeKernelForks hab hX hc₁ hc₂).pt = X
    source
    @[simp]
    theorem CategoryTheory.Limits.BinaryBicone.ofCoprimeKernelForks_inl {R : Type u_1} [CommSemiring R] {C : Type u_2} [Category.{u_3, u_2} C] [Preadditive C] [Linear R C] {X : C} {a b m n : R} (hab : a * m + b * n = 1) (hX : (m * n) • CategoryStruct.id X = 0) {c₁ : KernelFork (m • CategoryStruct.id X)} (hc₁ : IsLimit c₁) {c₂ : KernelFork (n • CategoryStruct.id X)} (hc₂ : IsLimit c₂) :
    (ofCoprimeKernelForks hab hX hc₁ hc₂).inl = Fork.ι c₁
    source
    @[simp]
    theorem CategoryTheory.Limits.BinaryBicone.ofCoprimeKernelForks_fst_ι {R : Type u_1} [CommSemiring R] {C : Type u_2} [Category.{u_3, u_2} C] [Preadditive C] [Linear R C] {X : C} {a b m n : R} (hab : a * m + b * n = 1) (hX : (m * n) • CategoryStruct.id X = 0) {c₁ : KernelFork (m • CategoryStruct.id X)} (hc₁ : IsLimit c₁) {c₂ : KernelFork (n • CategoryStruct.id X)} (hc₂ : IsLimit c₂) :
    CategoryStruct.comp (ofCoprimeKernelForks hab hX hc₁ hc₂).fst (Fork.ι c₁) = (b * n) • CategoryStruct.id X

    The first projection of BinaryBicone.ofCoprimeKernelForks, followed by the inclusion of the kernel of m • 𝟙 X, is multiplication by b * n.

    source
    theorem CategoryTheory.Limits.BinaryBicone.ofCoprimeKernelForks_fst_ι_assoc {R : Type u_1} [CommSemiring R] {C : Type u_2} [Category.{u_3, u_2} C] [Preadditive C] [Linear R C] {X : C} {a b m n : R} (hab : a * m + b * n = 1) (hX : (m * n) • CategoryStruct.id X = 0) {c₁ : KernelFork (m • CategoryStruct.id X)} (hc₁ : IsLimit c₁) {c₂ : KernelFork (n • CategoryStruct.id X)} (hc₂ : IsLimit c₂) {Z : C} (h : X ⟶ Z) :
    CategoryStruct.comp (↑(KernelFork.IsLimit.lift' hc₁ ((b * n) • CategoryStruct.id X) ⋯)) (CategoryStruct.comp (Fork.ι c₁) h) = CategoryStruct.comp ((b * n) • CategoryStruct.id X) h

    The first projection of BinaryBicone.ofCoprimeKernelForks, followed by the inclusion of the kernel of m • 𝟙 X, is multiplication by b * n.

    source
    @[simp]
    theorem CategoryTheory.Limits.BinaryBicone.ofCoprimeKernelForks_snd_ι {R : Type u_1} [CommSemiring R] {C : Type u_2} [Category.{u_3, u_2} C] [Preadditive C] [Linear R C] {X : C} {a b m n : R} (hab : a * m + b * n = 1) (hX : (m * n) • CategoryStruct.id X = 0) {c₁ : KernelFork (m • CategoryStruct.id X)} (hc₁ : IsLimit c₁) {c₂ : KernelFork (n • CategoryStruct.id X)} (hc₂ : IsLimit c₂) :
    CategoryStruct.comp (ofCoprimeKernelForks hab hX hc₁ hc₂).snd (Fork.ι c₂) = (a * m) • CategoryStruct.id X

    The second projection of BinaryBicone.ofCoprimeKernelForks, followed by the inclusion of the kernel of n • 𝟙 X, is multiplication by a * m.

    source
    theorem CategoryTheory.Limits.BinaryBicone.ofCoprimeKernelForks_snd_ι_assoc {R : Type u_1} [CommSemiring R] {C : Type u_2} [Category.{u_3, u_2} C] [Preadditive C] [Linear R C] {X : C} {a b m n : R} (hab : a * m + b * n = 1) (hX : (m * n) • CategoryStruct.id X = 0) {c₁ : KernelFork (m • CategoryStruct.id X)} (hc₁ : IsLimit c₁) {c₂ : KernelFork (n • CategoryStruct.id X)} (hc₂ : IsLimit c₂) {Z : C} (h : X ⟶ Z) :
    CategoryStruct.comp (↑(KernelFork.IsLimit.lift' hc₂ ((a * m) • CategoryStruct.id X) ⋯)) (CategoryStruct.comp (Fork.ι c₂) h) = CategoryStruct.comp ((a * m) • CategoryStruct.id X) h

    The second projection of BinaryBicone.ofCoprimeKernelForks, followed by the inclusion of the kernel of n • 𝟙 X, is multiplication by a * m.

    source
    noncomputable def CategoryTheory.Limits.BinaryBicone.isBilimitOfCoprimeKernelForks {R : Type u_1} [CommSemiring R] {C : Type u_2} [Category.{u_3, u_2} C] [Preadditive C] [Linear R C] {X : C} {a b m n : R} (hab : a * m + b * n = 1) (hX : (m * n) • CategoryStruct.id X = 0) {c₁ : KernelFork (m • CategoryStruct.id X)} (hc₁ : IsLimit c₁) {c₂ : KernelFork (n • CategoryStruct.id X)} (hc₂ : IsLimit c₂) :
    (ofCoprimeKernelForks hab hX hc₁ hc₂).IsBilimit

    An object killed by a product of coprime scalars is the biproduct of the two kernels. If (m * n) • 𝟙 X = 0 and a * m + b * n = 1, then X, with the kernel inclusions of m • 𝟙 X and n • 𝟙 X and the projections of BinaryBicone.ofCoprimeKernelForks, is a binary biproduct of the two kernels.

    Instances For