Documentation Verification Report

Iso

📁 Source: Mathlib/RepresentationTheory/Rep/Iso.lean

Statistics

Metric	Count
Definitions `Iso`, `counitIso`, `counitIsoAddEquiv`, `diagonalHomEquiv`, `diagonalSuccIsoFree`, `diagonalSuccIsoTensorTrivial`, `equivalenceModuleMonoidAlgebra`, `instAbelian`, `ofModuleMonoidAlgebra`, `toModuleMonoidAlgebra`, `toModuleMonoidAlgebraMap`, `unitIso`, `unitIsoAddEquiv`, `Iso`	14
Theorems `diagonal_succ_projective`, `free_projective`, `instEnoughProjectives`, `instHasBinaryBiproducts`, `instHasFiniteProducts`, `instHasZeroObject`, `instIsEquivalenceModuleCatMonoidAlgebraOfModuleMonoidAlgebra`, `instIsEquivalenceModuleCatMonoidAlgebraToModuleMonoidAlgebra`, `leftRegular_projective`, `ofModuleMonoidAlgebra_obj_coe`, `ofModuleMonoidAlgebra_obj_ρ`, `to_Module_monoidAlgebra_map_aux`, `trivial_projective_of_subsingleton`, `unit_iso_comm`	14
Total	28

JordanHolderLattice

Definitions

Name	Category	Theorems
`Iso` 📖	MathDef	5 math math: `second_iso`, `second_iso_of_eq`, `iso_trans`, `iso_symm`, `IsMaximal.iso_refl`

Rep

Definitions

Name	Category	Theorems
`counitIso` 📖	CompOp	—
`counitIsoAddEquiv` 📖	CompOp	—
`diagonalHomEquiv` 📖	CompOp	—
`diagonalSuccIsoFree` 📖	CompOp	1 math math: `barComplex.d_comp_diagonalSuccIsoFree_inv_eq`
`diagonalSuccIsoTensorTrivial` 📖	CompOp	—
`equivalenceModuleMonoidAlgebra` 📖	CompOp	—
`instAbelian` 📖	CompOp	7 math math: `Tor_map`, `FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun`, `inhomogeneousCochains.d_eq`, `standardComplex.instQuasiIsoNatεToSingle₀`, `FiniteCyclicGroup.resolution_quasiIso`, `FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply`, `Tor_obj`
`ofModuleMonoidAlgebra` 📖	CompOp	4 math math: `instIsEquivalenceModuleCatMonoidAlgebraOfModuleMonoidAlgebra`, `ofModuleMonoidAlgebra_obj_coe`, `ofModuleMonoidAlgebra_obj_ρ`, `unit_iso_comm`
`toModuleMonoidAlgebra` 📖	CompOp	2 math math: `instIsEquivalenceModuleCatMonoidAlgebraToModuleMonoidAlgebra`, `unit_iso_comm`
`toModuleMonoidAlgebraMap` 📖	CompOp	—
`unitIso` 📖	CompOp	—
`unitIsoAddEquiv` 📖	CompOp	1 math math: `unit_iso_comm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diagonal_succ_projective` 📖	mathematical	—	`CategoryTheory.Projective` `Rep` `Ring.toSemiring` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instCategory` `diagonal`	—	`CategoryTheory.Projective.of_iso` `free_projective`
`free_projective` 📖	mathematical	—	`CategoryTheory.Projective` `Rep` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCategory` `free`	—	`CategoryTheory.Adjunction.projective_of_map_projective` `CategoryTheory.Equivalence.full_functor` `CategoryTheory.Equivalence.faithful_functor` `ModuleCat.projective_of_free`
`instEnoughProjectives` 📖	mathematical	—	`CategoryTheory.EnoughProjectives` `Rep` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCategory`	—	`CategoryTheory.Equivalence.enoughProjectives_iff` `ModuleCat.enoughProjectives` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`instHasBinaryBiproducts` 📖	mathematical	—	`CategoryTheory.Limits.HasBinaryBiproducts` `Rep` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive`	—	`CategoryTheory.Limits.hasBinaryBiproduct_of_total` `RingHomCompTriple.ids` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `hom_ext` `Representation.IntertwiningMap.ext` `add_zero` `zero_add`
`instHasFiniteProducts` 📖	mathematical	—	`CategoryTheory.Limits.HasFiniteProducts` `Rep` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCategory`	—	`CategoryTheory.hasFiniteProducts_of_has_binary_and_terminal` `CategoryTheory.Limits.hasBinaryProducts_of_hasBinaryBiproducts` `instHasBinaryBiproducts` `CategoryTheory.Limits.HasZeroObject.hasTerminal` `instHasZeroObject`
`instHasZeroObject` 📖	mathematical	—	`CategoryTheory.Limits.HasZeroObject` `Rep` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCategory`	—	`hom_ext` `Representation.IntertwiningMap.ext` `LinearMap.ext` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `Representation.IntertwiningMap.instLinearMapClass`
`instIsEquivalenceModuleCatMonoidAlgebraOfModuleMonoidAlgebra` 📖	mathematical	—	`CategoryTheory.Functor.IsEquivalence` `ModuleCat` `MonoidAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidAlgebra.ring` `CommRing.toRing` `ModuleCat.moduleCategory` `Rep` `instCategory` `ofModuleMonoidAlgebra`	—	`CategoryTheory.Equivalence.isEquivalence_inverse`
`instIsEquivalenceModuleCatMonoidAlgebraToModuleMonoidAlgebra` 📖	mathematical	—	`CategoryTheory.Functor.IsEquivalence` `Rep` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCategory` `ModuleCat` `MonoidAlgebra` `MonoidAlgebra.ring` `CommRing.toRing` `ModuleCat.moduleCategory` `toModuleMonoidAlgebra`	—	`CategoryTheory.Equivalence.isEquivalence_functor`
`leftRegular_projective` 📖	mathematical	—	`CategoryTheory.Projective` `Rep` `Ring.toSemiring` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instCategory` `leftRegular`	—	`CategoryTheory.Projective.of_iso` `diagonal_succ_projective`
`ofModuleMonoidAlgebra_obj_coe` 📖	mathematical	—	`V` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CategoryTheory.Functor.obj` `ModuleCat` `MonoidAlgebra` `MonoidAlgebra.ring` `CommRing.toRing` `ModuleCat.moduleCategory` `Rep` `instCategory` `ofModuleMonoidAlgebra` `RestrictScalars` `ModuleCat.carrier`	—	—
`ofModuleMonoidAlgebra_obj_ρ` 📖	mathematical	—	`ρ` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CategoryTheory.Functor.obj` `ModuleCat` `MonoidAlgebra` `MonoidAlgebra.ring` `CommRing.toRing` `ModuleCat.moduleCategory` `Rep` `instCategory` `ofModuleMonoidAlgebra` `Representation.ofModule` `ModuleCat.carrier` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule`	—	—
`to_Module_monoidAlgebra_map_aux` 📖	mathematical	`LinearMap.comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `DFunLike.coe` `MonoidHom` `LinearMap` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring` `MonoidHom.instFunLike`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `AlgHom` `MonoidAlgebra` `MonoidAlgebra.semiring` `Module.End.instSemiring` `MonoidAlgebra.algebra` `Algebra.id` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `MonoidAlgebra.lift`	—	`RingHomCompTriple.ids` `MonoidAlgebra.induction_on` `smulCommClass_self` `IsScalarTower.left` `MonoidAlgebra.lift_single` `one_smul` `LinearMap.congr_fun` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `LinearMap.semilinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass`
`trivial_projective_of_subsingleton` 📖	mathematical	—	`CategoryTheory.Projective` `Rep` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instCategory` `trivial` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule`	—	`CategoryTheory.Projective.of_iso` `diagonal_succ_projective`
`unit_iso_comm` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `V` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CategoryTheory.Functor.obj` `Rep` `instCategory` `CategoryTheory.Functor.comp` `ModuleCat` `MonoidAlgebra` `MonoidAlgebra.ring` `CommRing.toRing` `ModuleCat.moduleCategory` `toModuleMonoidAlgebra` `ofModuleMonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `hV1` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `unitIsoAddEquiv` `AddHom.toFun` `LinearMap.toAddHom` `RingHom.id` `Semiring.toNonAssocSemiring` `hV2` `Representation` `LinearMap` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring` `ρ`	—	`RingHomInvPair.ids` `Representation.asModuleEquiv_symm_map_rho` `Representation.single_smul` `LinearEquiv.apply_symm_apply` `one_smul` `Representation.ofModule_asModule_act` `AddEquiv.apply_symm_apply`

SimpleGraph

Definitions

Name	Category	Theorems
`Iso` 📖	CompOp	30 math math: `Iso.map_adj_iff`, `isVertexCover_preimage_iso`, `Iso.reachable_iff`, `isContained_iff_exists_iso_subgraph`, `Iso.symm_apply_reachable`, `hasseDualIso_apply`, `Iso.map_symm_apply`, `Copy.range_toSubgraph`, `IsTuranMaximal.nonempty_iso_turanGraph`, `IsContained.exists_iso_subgraph`, `Iso.map_mem_edgeSet_iff`, `Iso.apply_mem_neighborSet_iff`, `ConnectedComponent.iso_inv_image_comp_eq_iff_eq_map`, `IsIndContained.exists_iso_subgraph`, `isVertexCover_image_iso`, `ConnectedComponent.iso_image_comp_eq_map_iff_eq_comp`, `Iso.mapNeighborSet_apply_coe`, `Iso.comap_apply`, `isIndContained_iff_exists_iso_subgraph`, `Iso.degree_eq`, `isTuranMaximal_iff_nonempty_iso_turanGraph`, `Copy.toSubgraph_surjOn`, `Iso.mapNeighborSet_symm_apply_coe`, `hasseDualIso_symm_apply`, `killCopies_def`, `Iso.coe_comp`, `isCompleteMultipartite_iff`, `card_edgeFinset_eq_extremalNumber_top_iff_nonempty_iso_turanGraph`, `Iso.map_apply`, `Iso.comap_symm_apply`

---

← Back to Index