Commit 2023-09-18 15:32 4b30681e

View on Github →

feat: the category of quadratic modules, QuadraticModuleCat (#6987) The motivations here are:

QuadraticModuleCat.cliffordAlgebra : QuadraticModuleCat.{u} R ⥤ AlgebraCat.{u} R (in this PR)
The project to formalize the Witt ring of quadratic forms ended up needing QuadraticModuleCat, which came up at LFTCM2023

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/CliffordAlgebra/CategoryTheory.lean

added def QuadraticModuleCat.cliffordAlgebra

Created Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat.lean

added def CategoryTheory.Iso.toIsometryEquiv

added theorem CategoryTheory.Iso.toIsometryEquiv_refl

added theorem CategoryTheory.Iso.toIsometryEquiv_symm

added theorem CategoryTheory.Iso.toIsometryEquiv_trans

added theorem QuadraticModuleCat.Hom.toIsometry_injective

added structure QuadraticModuleCat.Hom

added theorem QuadraticModuleCat.forget₂_map

added theorem QuadraticModuleCat.forget₂_obj

added theorem QuadraticModuleCat.hom_ext

added def QuadraticModuleCat.of

added def QuadraticModuleCat.ofIso

added theorem QuadraticModuleCat.ofIso_refl

added theorem QuadraticModuleCat.ofIso_symm

added theorem QuadraticModuleCat.ofIso_trans

added theorem QuadraticModuleCat.toIsometry_comp

added theorem QuadraticModuleCat.toIsometry_id

added structure QuadraticModuleCat