The Problem With Grothendieck’s Use Of Equality

The article examines how Grothendieck’s casual identification of canonically isomorphic objects with true equalities—especially in EGA and later texts like Milne’s—creates a silent gap between classical algebraic geometry and modern formal proof systems such as Lean. By unpacking examples involving localisations and pullbacks of sheaves, it argues that the community’s habitual abuse of “=” hides missing arguments and forces a rethink of how universal properties and “canonical” constructions should be defined when mathematics is formalised.