Documentation Verification Report

ExteriorPower

📁 Source: Mathlib/Algebra/Category/ModuleCat/ExteriorPower.lean

Statistics

Metric	Count
Definitions `AlternatingMap`, `postcomp`, `exteriorPower`, `desc`, `functor`, `iso₀`, `iso₁`, `map`, `mk`, `natIso₀`, `natIso₁`, `instFunLikeAlternatingMapForallFinCarrier`	12
Theorems `ext`, `ext_iff`, `postcomp_apply`, `desc_mk`, `functor_map`, `functor_obj`, `hom_ext`, `hom_ext_iff`, `iso₀_hom_apply`, `iso₀_hom_naturality`, `iso₀_hom_naturality_assoc`, `iso₁_hom_apply`, `iso₁_hom_naturality`, `iso₁_hom_naturality_assoc`, `map_mk`	15
Total	27

ModuleCat

Definitions

Name	Category	Theorems
`AlternatingMap` 📖	CompOp	6 math math: `AlternatingMap.postcomp_apply`, `exteriorPower.desc_mk`, `exteriorPower.map_mk`, `exteriorPower.iso₀_hom_apply`, `exteriorPower.iso₁_hom_apply`, `AlternatingMap.ext_iff`
`exteriorPower` 📖	CompOp	10 math math: `exteriorPower.iso₀_hom_naturality`, `exteriorPower.desc_mk`, `exteriorPower.map_mk`, `exteriorPower.iso₁_hom_naturality`, `exteriorPower.iso₀_hom_apply`, `exteriorPower.hom_ext_iff`, `exteriorPower.iso₀_hom_naturality_assoc`, `exteriorPower.iso₁_hom_apply`, `exteriorPower.iso₁_hom_naturality_assoc`, `exteriorPower.functor_obj`
`instFunLikeAlternatingMapForallFinCarrier` 📖	CompOp	6 math math: `AlternatingMap.postcomp_apply`, `exteriorPower.desc_mk`, `exteriorPower.map_mk`, `exteriorPower.iso₀_hom_apply`, `exteriorPower.iso₁_hom_apply`, `AlternatingMap.ext_iff`

ModuleCat.AlternatingMap

Definitions

Name	Category	Theorems
`postcomp` 📖	CompOp	2 math math: `postcomp_apply`, `ModuleCat.exteriorPower.hom_ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`DFunLike.coe` `ModuleCat.AlternatingMap` `ModuleCat.carrier` `CommRing.toRing` `ModuleCat.instFunLikeAlternatingMapForallFinCarrier`	—	—	`AlternatingMap.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `ModuleCat.AlternatingMap` `ModuleCat.carrier` `CommRing.toRing` `ModuleCat.instFunLikeAlternatingMapForallFinCarrier`	—	`ext`
`postcomp_apply` 📖	mathematical	—	`DFunLike.coe` `ModuleCat.AlternatingMap` `ModuleCat.carrier` `CommRing.toRing` `ModuleCat.instFunLikeAlternatingMapForallFinCarrier` `postcomp` `CategoryTheory.ConcreteCategory.hom` `ModuleCat` `ModuleCat.moduleCategory` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier`	—	—

ModuleCat.exteriorPower

Definitions

Name	Category	Theorems
`desc` 📖	CompOp	1 math math: `desc_mk`
`functor` 📖	CompOp	2 math math: `functor_obj`, `functor_map`
`iso₀` 📖	CompOp	3 math math: `iso₀_hom_naturality`, `iso₀_hom_apply`, `iso₀_hom_naturality_assoc`
`iso₁` 📖	CompOp	3 math math: `iso₁_hom_naturality`, `iso₁_hom_apply`, `iso₁_hom_naturality_assoc`
`map` 📖	CompOp	6 math math: `iso₀_hom_naturality`, `map_mk`, `iso₁_hom_naturality`, `iso₀_hom_naturality_assoc`, `iso₁_hom_naturality_assoc`, `functor_map`
`mk` 📖	CompOp	—
`natIso₀` 📖	CompOp	—
`natIso₁` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`desc_mk` 📖	mathematical	—	`DFunLike.coe` `ModuleCat.exteriorPower` `ModuleCat.carrier` `CommRing.toRing` `CategoryTheory.ConcreteCategory.hom` `ModuleCat` `ModuleCat.moduleCategory` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `desc` `ModuleCat.AlternatingMap` `ModuleCat.instFunLikeAlternatingMapForallFinCarrier`	—	`exteriorPower.alternatingMapLinearEquiv_apply_ιMulti`
`functor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `functor` `map`	—	—
`functor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `functor` `ModuleCat.exteriorPower`	—	—
`hom_ext` 📖	—	`ModuleCat.AlternatingMap.postcomp` `ModuleCat.exteriorPower`	—	—	`ModuleCat.hom_ext` `exteriorPower.linearMap_ext`
`hom_ext_iff` 📖	mathematical	—	`ModuleCat.AlternatingMap.postcomp` `ModuleCat.exteriorPower`	—	`hom_ext`
`iso₀_hom_apply` 📖	mathematical	—	`DFunLike.coe` `ModuleCat.exteriorPower` `ModuleCat.of` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `ModuleCat` `ModuleCat.moduleCategory` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Iso.hom` `iso₀` `ModuleCat.AlternatingMap` `ModuleCat.instFunLikeAlternatingMapForallFinCarrier` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`exteriorPower.zeroEquiv_ιMulti`
`iso₀_hom_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ModuleCat` `CommRing.toRing` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `ModuleCat.exteriorPower` `ModuleCat.of` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `map` `CategoryTheory.Iso.hom` `iso₀`	—	`ModuleCat.hom_ext` `exteriorPower.zeroEquiv_naturality`
`iso₀_hom_naturality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ModuleCat` `CommRing.toRing` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `ModuleCat.exteriorPower` `map` `ModuleCat.of` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `CategoryTheory.Iso.hom` `iso₀`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `iso₀_hom_naturality`
`iso₁_hom_apply` 📖	mathematical	—	`DFunLike.coe` `ModuleCat.exteriorPower` `ModuleCat.carrier` `CommRing.toRing` `CategoryTheory.ConcreteCategory.hom` `ModuleCat` `ModuleCat.moduleCategory` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Iso.hom` `iso₁` `ModuleCat.AlternatingMap` `ModuleCat.instFunLikeAlternatingMapForallFinCarrier`	—	`exteriorPower.oneEquiv_ιMulti`
`iso₁_hom_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ModuleCat` `CommRing.toRing` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `ModuleCat.exteriorPower` `map` `CategoryTheory.Iso.hom` `iso₁`	—	`ModuleCat.hom_ext` `exteriorPower.oneEquiv_naturality`
`iso₁_hom_naturality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ModuleCat` `CommRing.toRing` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `ModuleCat.exteriorPower` `map` `CategoryTheory.Iso.hom` `iso₁`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `iso₁_hom_naturality`
`map_mk` 📖	mathematical	—	`DFunLike.coe` `ModuleCat.exteriorPower` `ModuleCat.carrier` `CommRing.toRing` `CategoryTheory.ConcreteCategory.hom` `ModuleCat` `ModuleCat.moduleCategory` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `map` `ModuleCat.AlternatingMap` `ModuleCat.instFunLikeAlternatingMapForallFinCarrier`	—	`exteriorPower.map_apply_ιMulti`

---

← Back to Index