{"id":"palomar/PALOMAR-2026-10-15-000010","url":"https://github.com/AItoBit/DARPA-s-23-Mathematical-Challenges/tree/42b1d19b3d53ff5333725ef4410c1e0de84b22d2","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-15-000010-v1.json","repo":"https://github.com/AItoBit/DARPA-s-23-Mathematical-Challenges","tags":["math.GR","math.RA","msc:20J06","group-theory","matrix-representations","obstruction-theory"],"score":0,"title":"H2 obstruction to lifting discrete matrix representations","trust":"high","domain":"math.GR","source":"palomar","authors":["AItoBit"],"reviews":0,"subject":"math.GR","summary":"A Lean proof that a discrete matrix representation lifts across a surjective homomorphism of commutative rings with square-zero kernel exactly when its explicitly constructed second-cohomology obstruction vanishes. The proof constructs the conjugation action and defect cocycle for an abelian group extension, proves the lifting criterion, and applies it to reduction of invertible matrices. The underlying additive kernel is identified with matrices over the coefficient-ring kernel. This is classical obstruction theory motivated by DARPA Challenge 18, not a solution of its homotopy/Langlands…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-15","reactions":{},"formalized":true,"formalizes":[{"title":"User-supplied H2 cohomology and square-zero matrix lemmas","identifier":"","relationship":"adapts"}]}