English
The biproduct from subtype is equal to a biproduct lift of a piecewise projection: if p j then π(g) else 0.
Русский
Из биопродукта через подтип равен lift-образу проекции: если p j, то проекция, иначе ноль.
LaTeX
$$$\\text{biproduct.fromSubtype } f p = \\text{biproduct.lift }(\\lambda j. \\; \\pi f j \\text{ если } p j, \\text{ иначе } 0).$$$
Lean4
instance {ι} (f : ι → Type*) (g : (i : ι) → (f i) → C) [∀ i, HasBiproduct (g i)] [HasBiproduct fun i => ⨁ g i] :
HasBiproduct fun p : Σ i, f i => g p.1 p.2 where
exists_biproduct :=
Nonempty.intro
{ bicone :=
{ pt := ⨁ fun i => ⨁ g i
ι := fun X => biproduct.ι (g X.1) X.2 ≫ biproduct.ι (fun i => ⨁ g i) X.1
π := fun X => biproduct.π (fun i => ⨁ g i) X.1 ≫ biproduct.π (g X.1) X.2
ι_π := fun ⟨j, x⟩ ⟨j', y⟩ => by
split_ifs with h
· obtain ⟨rfl, rfl⟩ := h
simp
· simp only [Sigma.mk.inj_iff, not_and] at h
by_cases w : j = j'
· cases w
simp only [heq_eq_eq, forall_true_left] at h
simp [biproduct.ι_π_ne _ h]
· simp [biproduct.ι_π_ne_assoc _ w] }
isBilimit :=
{ isLimit := mkFanLimit _ (fun s => biproduct.lift fun b => biproduct.lift fun c => s.proj ⟨b, c⟩)
isColimit := mkCofanColimit _ (fun s => biproduct.desc fun b => biproduct.desc fun c => s.inj ⟨b, c⟩) } }
