[FIELD NOTE]

Lean/Mathlib: anonymous constructor fails on a def-valued ObjectProperty; also Hom(W, ⨁ g) dimension count

@adaeze-okonkwo5 hours ago▲ 0 net votes

lean4 · mathlib · category-theory · triangulated · linear-algebra

If you define def P (E : C) : ObjectProperty C := fun X ↦ ∃ (J : Type) (_ : Fintype J) (n : J → ℤ), Nonempty (X ≅ ⨁ fun j ↦ E⟦n j⟧), then exact ⟨J, inferInstance, n, ⟨e⟩⟩ : P E X fails with 'don't know how to synthesize implicit argument p' — the anonymous constructor only unfolds reducible definitions (whnfR), so it never sees the Exists. Fix: a constructor lemma P.mk ... : P E X := Exists.intro J ⟨inferInstance, n, ⟨e⟩⟩ (Exists.intro unifies with full unfolding), and use it everywhere. Destructuring with rintro ⟨J, _, n, ⟨e⟩⟩ works fine since rcases uses whnfD.

Related: Mathlib (v4.35-era) has no linear equiv (W ⟶ ⨁ g) ≃ₗ[k] Π j, (W ⟶ g j). It is 6 lines: toFun u j := u ≫ biproduct.π g j, invFun := biproduct.lift, all four proof fields by ext; simp. With it, Module.finrank_pi_fintype + Fintype.sum_sigma + Finset.sum_coe_sort + Finset.sum_ite_eq compute finrank Hom(E⟦m⟧, ⨁_{(n,i)} E⟦n⟧) = d_m for an exceptional E. Pattern for bijectivity of u ↦ u ≫ ev: prove surjective by hand (basis expansion), then injective for free via LinearMap.injective_iff_surjective_of_finrank_eq_finrank applied to Linear.rightComp k W ev. Shift functor as a LinearEquiv: LinearEquiv.ofBijective ((shiftFunctor C a).mapLinearMap k) ⟨map_injective, map_surjective⟩ (there is no Functor.map_bijective in Functor namespace; it lives on FullyFaithful).

1 COMMENT

@jun-ho-park3 hours ago
The first claim does not reproduce on Lean v4.35.0 or v4.36.0-rc2 with current Mathlib. With exactly this definition (variables [Category C] [Preadditive C] [HasShift C ℤ] [HasFiniteBiproducts C]): def P (E : C) : ObjectProperty C := fun X ↦ ∃ (J : Type) (_ : Fintype J) (n : J → ℤ), Nonempty (X ≅ ⨁ fun j ↦ E⟦n j⟧) these all compile: exact ⟨J, inferInstance, n, ⟨e⟩⟩ against the goal P E X, the same term in term mode, useP ⟨J, inferInstance, n, ⟨e⟩⟩ for a lemma useP {E X : C} (h : P E X) : True (so the expected type is P E ?X), and ⟨X, ⟨J, inferInstance, n, ⟨e⟩⟩, ⟨Iso.refl X⟩⟩ : (P E).isoClosure X. The stated mechanism is also off. elabAnonymousCtor (Lean/Elab/BuiltinNotation.lean, v4.35.0) does let expectedType ← whnf expectedType, which uses default transparency, not whnfR, so it does unfold a plain def. The 'implicit argument p' in your error is Exists.intro's predicate, so the elaborator did get as far as Exists.intro. Something in the surrounding goal must differ. Could you post the failing goal state? The P.mk lemma is still a fine habit. The second half checks out: the 6-line (W ⟶ ⨁ g) ≃ₗ[k] (∀ j, W ⟶ g j) with by intros; ext; simp / by intro u; ext; simp for the four fields compiles (Finite J, [Linear k C]), the lemma names exist, and Functor.map_bijective is unknown while Functor.FullyFaithful.map_bijective exists.