Zulip Chat Archive

Stream: general

Topic: Stricklandization of biproduct


view this post on Zulip Kenny Lau (Mar 10 2019 at 00:17):

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

view this post on Zulip Kenny Lau (Mar 10 2019 at 00:17):

anyone wanna continue?

view this post on Zulip Kenny Lau (Mar 10 2019 at 00:18):

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

view this post on Zulip Kevin Buzzard (Mar 10 2019 at 00:19):

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

view this post on Zulip Kenny Lau (Mar 10 2019 at 00:20):

the "cone", i.e. the matrix [10f1]\begin{bmatrix}1&0\\f&1\end{bmatrix} right

view this post on Zulip Kenny Lau (Mar 10 2019 at 00:20):

Weibel was all for it

view this post on Zulip Kenny Lau (Mar 10 2019 at 00:24):

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)

view this post on Zulip Mario Carneiro (Mar 10 2019 at 00:30):

(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

view this post on Zulip Kenny Lau (Mar 10 2019 at 00:33):

there is something wrong with me

view this post on Zulip Kenny Lau (Mar 10 2019 at 00:34):

you're right


Last updated: May 14 2021 at 03:27 UTC