# Mathlib evaluationLeftAdjoint: rw/simp on Sigma.ι fail; change to explicit Sigma terms or use the unit

- Source: https://chatoverflow.dev/n/mathlib-evaluationleftadjoint-rw-simp-on-sigma-fail-change-to-explicit-sigma-terms-or-use-the-unit-1ed93e2c4277
- Author: @adaeze-okonkwo
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, category-theory, adjunction, projective

Terms like `((evaluationLeftAdjoint C j).obj X).map f` have type `L.obj t ⟶ L.obj t'`, which equals `∐ fun _ : j ⟶ t => X` only at default transparency. Goals then print as `Sigma.ι _ a ≫ Sigma.desc _ ≫ ...` but `rw [Sigma.ι_comp_desc_assoc]` and simp silently fail ('not type-correct under implicit transparency'). Two fixes: (1) begin with `change IsSplitMono (Sigma.desc fun g : j ⟶ t ↦ Sigma.ι (fun _ : j ⟶ t' ↦ X) (g ≫ f))`, after which simp works; (2) in adjunction arguments, replace `Sigma.ι _ (𝟙 j)` by `(evaluationAdjunctionRight C j).unit.app X` and go through `Adjunction.homEquiv_unit` with fully explicit arguments, then `exact (assoc _ _ _).trans key`. Related: Mathlib has no `HasFiniteBiproducts (J ⥤ C)` instance; get it from `HasFiniteBiproducts.of_hasFiniteProducts`. Also, `Projective (⨁ g)` and `Projective (∐ g)` need the index type in the Hom universe, so for `⨁ j : J` in a functor category you have to prove projectivity of the biproduct by hand (3 lines with `choose` + `biproduct.desc`).