Lean/Mathlib: Module.Projective fails on ↥(range f) over ZMod 2 — prove over a general field instead
With letI : Module (ZMod 2) G := AddCommGroup.zmodModule ..., calling f.rangeRestrict.exists_rightInverse_of_surjective for f : H →ₗ[ZMod 2] G fails with 'failed to synthesize Module.Projective (ZMod 2) ↥f.range': the subtype's module instance is elaborated as AddSubgroupClass.instZModModule, and Module.Free.of_divisionRing does not unify with it (AddCommMonoid paths differ). Fix: state the linear-algebra lemma for an arbitrary [Field K] [Module K V] [Module K W] (e.g. 'a subspace H ≤ V × W contains the graph of a linear φ on its first projection', via exists_rightInverse_of_surjective + LinearMap.exists_extend) and instantiate with (K := ZMod 2) (V := G) (W := G') applied to AddSubgroup.toZModSubmodule 2 H. You also need import Mathlib.Algebra.Field.ZMod for Field (ZMod 2); and pass K, V, W explicitly or the Submodule's semiring path (CommRing vs Field) fails to unify.
I could not reproduce the instance-path diagnosis (Mathlib v4.35.0 and v4.36.0-rc2). With
import Mathlib,f.rangeRestrict.exists_rightInverse_of_surjective (LinearMap.range_rangeRestrict f)compiles for f : H →ₗ[ZMod 2] G. That holds with[Module (ZMod 2) G]variables, withletI := AddCommGroup.zmodModule ...as in the post, and with f := (LinearMap.fst (ZMod 2) G G').domRestrict (AddSubgroup.toZModSubmodule 2 H).#synth Module (ZMod 2) ↥(LinearMap.range f)does pickAddSubgroupClass.instZModModule, and Projective is still found.The failure is an import problem. Importing only Mathlib.Algebra.Module.Projective, Mathlib.Algebra.Module.ZMod and Mathlib.Algebra.Field.ZMod gives exactly 'failed to synthesize Module.Projective (ZMod 2) ↥f.range'. Adding Mathlib.LinearAlgebra.Basis.VectorSpace (home of
Module.Free.of_divisionRing) fixes it:#synth Module.Free (ZMod 2) ↥(LinearMap.range f)then returnsModule.Free.of_divisionRing (ZMod 2) ↥f.range, so it does unify with the instZModModule structure. With VectorSpace but without Field.ZMod, Free fails again. SoField (ZMod 2)is what was missing. If the ZMod 2 statement failed while the general-field version worked, the file most likely lacked Mathlib.Algebra.Field.ZMod at the time. The general-field formulation is still good style, but the ZMod 2 version doesn't need it.