Stricklandization of biproduct

Stream: general

[Kenny Lau]

import linear_algebra.basic

universes u v w u₁ v₁

variables (R : Type u) [ring R]

class biproduct (M : Type v) [add_comm_group M] [module R M]
  (N : Type w) [add_comm_group N] [module R N]
  (P : Type u₁) [add_comm_group P] [module R P] :=
(inl : M →ₗ[R] P)
(inr : N →ₗ[R] P)
(fst : P →ₗ[R] M)
(snd : P →ₗ[R] N)
(fst_inl : fst.comp inl = 1)
(snd_inr : snd.comp inr = 1)
(fst_inl_fst : fst.comp (inl.comp fst) = fst)
(snd_inr_snd : snd.comp (inr.comp snd) = snd)
(inl_fst_add_inr_snd : inl.comp fst + inr.comp snd = 1)

variables (M : Type v) [add_comm_group M] [module R M]
variables (N : Type w) [add_comm_group N] [module R N]

instance biproduct_prod : biproduct R M N (M × N) :=
{ inl := linear_map.inl R M N,
  inr := linear_map.inr R M N,
  fst := linear_map.fst R M N,
  snd := linear_map.snd R M N,
  fst_inl := linear_map.ext $ λ x, rfl,
  snd_inr := linear_map.ext $ λ x, rfl,
  fst_inl_fst := linear_map.ext $ λ x, rfl,
  snd_inr_snd := linear_map.ext $ λ x, rfl,
  inl_fst_add_inr_snd := linear_map.ext $ λ ⟨m, n⟩, prod.ext (add_zero m) (zero_add n) }

instance biproduct_prod_swap : biproduct R M N (N × M) :=
{ inl := linear_map.inr R N M,
  inr := linear_map.inl R N M,
  fst := linear_map.snd R N M,
  snd := linear_map.fst R N M,
  fst_inl := linear_map.ext $ λ x, rfl,
  snd_inr := linear_map.ext $ λ x, rfl,
  fst_inl_fst := linear_map.ext $ λ x, rfl,
  snd_inr_snd := linear_map.ext $ λ x, rfl,
  inl_fst_add_inr_snd := linear_map.ext $ λ ⟨m, n⟩, prod.ext (zero_add m) (add_zero n) }

variables {P : Type u₁} [add_comm_group P] [module R P] [biproduct R M N P]
variables {Q : Type v₁} [add_comm_group Q] [module R Q]

def biproduct.rec' (f : M →ₗ[R] Q) (g : N →ₗ[R] Q) : P →ₗ[R] Q :=
f.comp (biproduct.fst R M N P) + g.comp (biproduct.snd R M N P)

def biproduct.corec' (f : Q →ₗ[R] M) (g : Q →ₗ[R] N) : Q →ₗ[R] P :=
(biproduct.inl R M N P).comp f + (biproduct.inr R M N P).comp g

theorem biproduct.eq_rec (f : P →ₗ[R] Q) : f = biproduct.rec' R M N (f.comp (biproduct.inl R M N P)) (f.comp (biproduct.inr R M N P)) :=
by rw [biproduct.rec', linear_map.comp_assoc, linear_map.comp_assoc]; sorry -- missing comp_add

theorem biproduct.eq_corec (f : Q →ₗ[R] P) : f = biproduct.corec' R M N ((biproduct.fst R M N P).comp f) ((biproduct.snd R M N P).comp f) :=
by rw [biproduct.corec', ← linear_map.comp_assoc, ← linear_map.comp_assoc]; sorry -- missing add_comp

def biproduct.equiv_prod : P ≃ₗ[R] M × N :=
linear_equiv.of_linear
  (biproduct.rec' R M N (biproduct.inl R M N _) (biproduct.inr R M N _))
  (biproduct.corec' R M N (biproduct.fst R M N _) (biproduct.snd R M N _))
  sorry
  sorry

[Kenny Lau]

anyone wanna continue?

[Kenny Lau]

goal: a functor F:R-Mod=>S-Mod is additive iff it preserves biproduct

[Kevin Buzzard]

There's some cool endomorphism of A + B that you get from a map from A to B, presumably.

[Kenny Lau]

the "cone", i.e. the matrix $\begin{bmatrix}1&0\\f&1\end{bmatrix}$ right

[Kenny Lau]

Weibel was all for it

[Kenny Lau]

def biproduct.mk_end (a : M →ₗ[R] M) (b : N →ₗ[R] M) (c : M →ₗ[R] N) (d : N →ₗ[R] N) : P →ₗ[R] P :=
biproduct.corec' R M N (biproduct.rec' R M N a b) (biproduct.rec' R M N c d)

[Mario Carneiro]

(fst_inl : fst.comp inl = 1)
(snd_inr : snd.comp inr = 1)
(fst_inl_fst : fst.comp (inl.comp fst) = fst)
(snd_inr_snd : snd.comp (inr.comp snd) = snd)

Don't the last two follow from the first two? I guess 1 is id

[Kenny Lau]

there is something wrong with me

[Kenny Lau]

you're right