Documentation Verification Report

QuadraticModuleCat

📁 Source: Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat.lean

Statistics

Metric	Count
Definitions `toIsometryEquiv`, `QuadraticModuleCat`, `toIsometry`, `toIsometry'`, `category`, `concreteCategory`, `form`, `hasForgetToModule`, `instCoeSortType`, `of`, `ofHom`, `ofIso`, `toModuleCat`	13
Theorems `toIsometryEquiv_invFun`, `toIsometryEquiv_refl`, `toIsometryEquiv_symm`, `toIsometryEquiv_toFun`, `toIsometryEquiv_trans`, `ext`, `ext_iff`, `toIsometry_injective`, `forget₂_map`, `forget₂_obj`, `hom_ext`, `hom_ext_iff`, `moduleCat_of_toModuleCat`, `ofIso_hom`, `ofIso_inv`, `ofIso_refl`, `ofIso_symm`, `ofIso_trans`, `toIsometry_comp`, `toIsometry_id`	20
Total	33

CategoryTheory.Iso

Definitions

Name	Category	Theorems
`toIsometryEquiv` 📖	CompOp	5 math math: `toIsometryEquiv_toFun`, `toIsometryEquiv_refl`, `toIsometryEquiv_invFun`, `toIsometryEquiv_symm`, `toIsometryEquiv_trans`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toIsometryEquiv_invFun` 📖	mathematical	—	`LinearEquiv.invFun` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ModuleCat.carrier` `CommRing.toRing` `QuadraticModuleCat.toModuleCat` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `QuadraticMap.IsometryEquiv.toLinearEquiv` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `QuadraticModuleCat.form` `toIsometryEquiv` `DFunLike.coe` `QuadraticMap.Isometry` `QuadraticMap.Isometry.instFunLike` `QuadraticModuleCat.Hom.toIsometry` `inv` `QuadraticModuleCat` `QuadraticModuleCat.category`	—	`RingHomInvPair.ids`
`toIsometryEquiv_refl` 📖	mathematical	—	`toIsometryEquiv` `refl` `QuadraticModuleCat` `QuadraticModuleCat.category` `QuadraticMap.IsometryEquiv.refl` `ModuleCat.carrier` `CommRing.toRing` `QuadraticModuleCat.toModuleCat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ModuleCat.isModule` `Semiring.toModule` `QuadraticModuleCat.form`	—	—
`toIsometryEquiv_symm` 📖	mathematical	—	`toIsometryEquiv` `symm` `QuadraticModuleCat` `QuadraticModuleCat.category` `QuadraticMap.IsometryEquiv.symm` `ModuleCat.carrier` `CommRing.toRing` `QuadraticModuleCat.toModuleCat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ModuleCat.isModule` `Semiring.toModule` `QuadraticModuleCat.form`	—	—
`toIsometryEquiv_toFun` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.IsometryEquiv` `ModuleCat.carrier` `CommRing.toRing` `QuadraticModuleCat.toModuleCat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ModuleCat.isModule` `Semiring.toModule` `QuadraticModuleCat.form` `EquivLike.toFunLike` `QuadraticMap.IsometryEquiv.instEquivLike` `toIsometryEquiv` `QuadraticMap.Isometry` `QuadraticMap.Isometry.instFunLike` `QuadraticModuleCat.Hom.toIsometry` `hom` `QuadraticModuleCat` `QuadraticModuleCat.category`	—	—
`toIsometryEquiv_trans` 📖	mathematical	—	`toIsometryEquiv` `trans` `QuadraticModuleCat` `QuadraticModuleCat.category` `QuadraticMap.IsometryEquiv.trans` `ModuleCat.carrier` `CommRing.toRing` `QuadraticModuleCat.toModuleCat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ModuleCat.isModule` `Semiring.toModule` `QuadraticModuleCat.form`	—	—

QuadraticModuleCat

Definitions

Name	Category	Theorems
`category` 📖	CompOp	28 math math: `toIsometry_comp`, `forget₂_map_associator_inv`, `ofIso_hom`, `forget₂_map`, `CategoryTheory.Iso.toIsometryEquiv_toFun`, `forget₂_map_associator_hom`, `toIsometry_whiskerRight`, `toIsometry_tensorHom`, `toIsometry_hom_leftUnitor`, `toIsometry_hom_rightUnitor`, `forget₂_obj`, `CategoryTheory.Iso.toIsometryEquiv_refl`, `toIsometry_inv_rightUnitor`, `toModuleCat_tensor`, `cliffordAlgebra_map`, `toIsometry_whiskerLeft`, `ofIso_trans`, `toIsometry_id`, `CategoryTheory.Iso.toIsometryEquiv_invFun`, `cliffordAlgebra_obj_carrier`, `toIsometry_inv_leftUnitor`, `ofIso_refl`, `ofIso_inv`, `ofIso_symm`, `CategoryTheory.Iso.toIsometryEquiv_symm`, `CategoryTheory.Iso.toIsometryEquiv_trans`, `hom_hom_associator`, `hom_inv_associator`
`concreteCategory` 📖	CompOp	4 math math: `forget₂_map_associator_inv`, `forget₂_map`, `forget₂_map_associator_hom`, `forget₂_obj`
`form` 📖	CompOp	24 math math: `toIsometry_comp`, `forget₂_map_associator_inv`, `forget₂_map`, `CategoryTheory.Iso.toIsometryEquiv_toFun`, `instMonoidalCategory.tensorObj_form`, `forget₂_map_associator_hom`, `toIsometry_whiskerRight`, `toIsometry_tensorHom`, `toIsometry_hom_leftUnitor`, `toIsometry_hom_rightUnitor`, `Hom.toIsometry_injective`, `forget₂_obj`, `CategoryTheory.Iso.toIsometryEquiv_refl`, `toIsometry_inv_rightUnitor`, `cliffordAlgebra_map`, `toIsometry_whiskerLeft`, `toIsometry_id`, `CategoryTheory.Iso.toIsometryEquiv_invFun`, `cliffordAlgebra_obj_carrier`, `toIsometry_inv_leftUnitor`, `CategoryTheory.Iso.toIsometryEquiv_symm`, `CategoryTheory.Iso.toIsometryEquiv_trans`, `hom_hom_associator`, `hom_inv_associator`
`hasForgetToModule` 📖	CompOp	4 math math: `forget₂_map_associator_inv`, `forget₂_map`, `forget₂_map_associator_hom`, `forget₂_obj`
`instCoeSortType` 📖	CompOp	—
`of` 📖	CompOp	5 math math: `ofIso_hom`, `ofIso_trans`, `ofIso_refl`, `ofIso_inv`, `ofIso_symm`
`ofHom` 📖	CompOp	2 math math: `ofIso_hom`, `ofIso_inv`
`ofIso` 📖	CompOp	5 math math: `ofIso_hom`, `ofIso_trans`, `ofIso_refl`, `ofIso_inv`, `ofIso_symm`
`toModuleCat` 📖	CompOp	26 math math: `toIsometry_comp`, `forget₂_map_associator_inv`, `forget₂_map`, `CategoryTheory.Iso.toIsometryEquiv_toFun`, `instMonoidalCategory.tensorObj_form`, `forget₂_map_associator_hom`, `toIsometry_whiskerRight`, `toIsometry_tensorHom`, `toIsometry_hom_leftUnitor`, `toIsometry_hom_rightUnitor`, `Hom.toIsometry_injective`, `forget₂_obj`, `CategoryTheory.Iso.toIsometryEquiv_refl`, `toIsometry_inv_rightUnitor`, `toModuleCat_tensor`, `cliffordAlgebra_map`, `toIsometry_whiskerLeft`, `toIsometry_id`, `CategoryTheory.Iso.toIsometryEquiv_invFun`, `cliffordAlgebra_obj_carrier`, `toIsometry_inv_leftUnitor`, `moduleCat_of_toModuleCat`, `CategoryTheory.Iso.toIsometryEquiv_symm`, `CategoryTheory.Iso.toIsometryEquiv_trans`, `hom_hom_associator`, `hom_inv_associator`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forget₂_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `QuadraticModuleCat` `category` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `CategoryTheory.forget₂` `QuadraticMap.Isometry` `ModuleCat.carrier` `toModuleCat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ModuleCat.isModule` `Semiring.toModule` `form` `QuadraticMap.Isometry.instFunLike` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `concreteCategory` `LinearMap` `Ring.toSemiring` `RingHom.id` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `hasForgetToModule` `ModuleCat.ofHom` `QuadraticMap.Isometry.toLinearMap` `Hom.toIsometry`	—	—
`forget₂_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `QuadraticModuleCat` `category` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `CategoryTheory.forget₂` `QuadraticMap.Isometry` `ModuleCat.carrier` `toModuleCat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ModuleCat.isModule` `Semiring.toModule` `form` `QuadraticMap.Isometry.instFunLike` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `concreteCategory` `LinearMap` `Ring.toSemiring` `RingHom.id` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `hasForgetToModule` `ModuleCat.of`	—	—
`hom_ext` 📖	—	`Hom.toIsometry`	—	—	`Hom.ext`
`hom_ext_iff` 📖	mathematical	—	`Hom.toIsometry`	—	`hom_ext`
`moduleCat_of_toModuleCat` 📖	mathematical	—	`ModuleCat.of` `CommRing.toRing` `ModuleCat.carrier` `toModuleCat` `ModuleCat.isAddCommGroup` `ModuleCat.isModule`	—	—
`ofIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `QuadraticModuleCat` `category` `of` `ofIso` `ofHom` `QuadraticMap.IsometryEquiv.toIsometry` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule`	—	—
`ofIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `QuadraticModuleCat` `category` `of` `ofIso` `ofHom` `QuadraticMap.IsometryEquiv.toIsometry` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `QuadraticMap.IsometryEquiv.symm`	—	—
`ofIso_refl` 📖	mathematical	—	`ofIso` `QuadraticMap.IsometryEquiv.refl` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `CategoryTheory.Iso.refl` `QuadraticModuleCat` `category` `of`	—	—
`ofIso_symm` 📖	mathematical	—	`ofIso` `QuadraticMap.IsometryEquiv.symm` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `CategoryTheory.Iso.symm` `QuadraticModuleCat` `category` `of`	—	—
`ofIso_trans` 📖	mathematical	—	`ofIso` `QuadraticMap.IsometryEquiv.trans` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `CategoryTheory.Iso.trans` `QuadraticModuleCat` `category` `of`	—	—
`toIsometry_comp` 📖	mathematical	—	`Hom.toIsometry` `CategoryTheory.CategoryStruct.comp` `QuadraticModuleCat` `CategoryTheory.Category.toCategoryStruct` `category` `QuadraticMap.Isometry.comp` `ModuleCat.carrier` `CommRing.toRing` `toModuleCat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ModuleCat.isModule` `Semiring.toModule` `form`	—	—
`toIsometry_id` 📖	mathematical	—	`Hom.toIsometry` `CategoryTheory.CategoryStruct.id` `QuadraticModuleCat` `CategoryTheory.Category.toCategoryStruct` `category` `QuadraticMap.Isometry.id` `ModuleCat.carrier` `CommRing.toRing` `toModuleCat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ModuleCat.isModule` `Semiring.toModule` `form`	—	—

QuadraticModuleCat.Hom

Definitions

Name	Category	Theorems
`toIsometry` 📖	CompOp	17 math math: `QuadraticModuleCat.toIsometry_comp`, `QuadraticModuleCat.forget₂_map`, `CategoryTheory.Iso.toIsometryEquiv_toFun`, `QuadraticModuleCat.toIsometry_whiskerRight`, `QuadraticModuleCat.toIsometry_tensorHom`, `QuadraticModuleCat.toIsometry_hom_leftUnitor`, `QuadraticModuleCat.toIsometry_hom_rightUnitor`, `toIsometry_injective`, `QuadraticModuleCat.toIsometry_inv_rightUnitor`, `QuadraticModuleCat.cliffordAlgebra_map`, `QuadraticModuleCat.toIsometry_whiskerLeft`, `QuadraticModuleCat.toIsometry_id`, `CategoryTheory.Iso.toIsometryEquiv_invFun`, `QuadraticModuleCat.toIsometry_inv_leftUnitor`, `QuadraticModuleCat.hom_ext_iff`, `QuadraticModuleCat.hom_hom_associator`, `QuadraticModuleCat.hom_inv_associator`
`toIsometry'` 📖	CompOp	1 math math: `ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`toIsometry'`	—	—	—
`ext_iff` 📖	mathematical	—	`toIsometry'`	—	`ext`
`toIsometry_injective` 📖	mathematical	—	`QuadraticModuleCat.Hom` `QuadraticMap.Isometry` `ModuleCat.carrier` `CommRing.toRing` `QuadraticModuleCat.toModuleCat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ModuleCat.isModule` `Semiring.toModule` `QuadraticModuleCat.form` `toIsometry`	—	—

(root)

Definitions

Name	Category	Theorems
`QuadraticModuleCat` 📖	CompData	28 math math: `QuadraticModuleCat.toIsometry_comp`, `QuadraticModuleCat.forget₂_map_associator_inv`, `QuadraticModuleCat.ofIso_hom`, `QuadraticModuleCat.forget₂_map`, `CategoryTheory.Iso.toIsometryEquiv_toFun`, `QuadraticModuleCat.forget₂_map_associator_hom`, `QuadraticModuleCat.toIsometry_whiskerRight`, `QuadraticModuleCat.toIsometry_tensorHom`, `QuadraticModuleCat.toIsometry_hom_leftUnitor`, `QuadraticModuleCat.toIsometry_hom_rightUnitor`, `QuadraticModuleCat.forget₂_obj`, `CategoryTheory.Iso.toIsometryEquiv_refl`, `QuadraticModuleCat.toIsometry_inv_rightUnitor`, `QuadraticModuleCat.toModuleCat_tensor`, `QuadraticModuleCat.cliffordAlgebra_map`, `QuadraticModuleCat.toIsometry_whiskerLeft`, `QuadraticModuleCat.ofIso_trans`, `QuadraticModuleCat.toIsometry_id`, `CategoryTheory.Iso.toIsometryEquiv_invFun`, `QuadraticModuleCat.cliffordAlgebra_obj_carrier`, `QuadraticModuleCat.toIsometry_inv_leftUnitor`, `QuadraticModuleCat.ofIso_refl`, `QuadraticModuleCat.ofIso_inv`, `QuadraticModuleCat.ofIso_symm`, `CategoryTheory.Iso.toIsometryEquiv_symm`, `CategoryTheory.Iso.toIsometryEquiv_trans`, `QuadraticModuleCat.hom_hom_associator`, `QuadraticModuleCat.hom_inv_associator`

---

← Back to Index