HomOrthogonal

📁 Source: Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean

Statistics

Metric	Count
Definitions HomOrthogonal, matrixDecomposition, matrixDecompositionAddEquiv, matrixDecompositionLinearEquiv	4
Theorems eq_zero, equiv_of_iso, matrixDecompositionAddEquiv_apply, matrixDecompositionAddEquiv_symm_apply, matrixDecompositionLinearEquiv_apply, matrixDecompositionLinearEquiv_symm_apply, matrixDecomposition_apply, matrixDecomposition_comp, matrixDecomposition_id, matrixDecomposition_symm_apply	10
Total	14

CategoryTheory

Definitions

Name	Category	Theorems
HomOrthogonal 📖	MathDef	—

CategoryTheory.HomOrthogonal

Definitions

Name	Category	Theorems
matrixDecomposition 📖	CompOp	4 math math: matrixDecomposition_id, matrixDecomposition_comp, matrixDecomposition_apply, matrixDecomposition_symm_apply
matrixDecompositionAddEquiv 📖	CompOp	4 math math: matrixDecompositionLinearEquiv_symm_apply, matrixDecompositionLinearEquiv_apply, matrixDecompositionAddEquiv_symm_apply, matrixDecompositionAddEquiv_apply
matrixDecompositionLinearEquiv 📖	CompOp	2 math math: matrixDecompositionLinearEquiv_symm_apply, matrixDecompositionLinearEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero 📖	mathematical	CategoryTheory.HomOrthogonal	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
equiv_of_iso 📖	mathematical	InvariantBasisNumber CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.Preadditive.instSemiringEnd CategoryTheory.HomOrthogonal	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite Cardinal.eq nonempty_fintype Cardinal.mk_fintype Cardinal.instCharZero Matrix.square_of_invertible Finite.of_fintype matrixDecomposition_comp CategoryTheory.Iso.hom_inv_id matrixDecomposition_id CategoryTheory.Iso.inv_hom_id Equiv.ofPreimageEquiv_map
matrixDecompositionAddEquiv_apply 📖	mathematical	CategoryTheory.HomOrthogonal	DFunLike.coe AddEquiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Pi.instAdd Matrix Set.Elem Set.preimage Set Set.instSingletonSet CategoryTheory.End Matrix.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CategoryTheory.Preadditive.instRingEnd EquivLike.toFunLike AddEquiv.instEquivLike matrixDecompositionAddEquiv CategoryTheory.CategoryStruct.comp Set.instMembership CategoryTheory.eqToHom CategoryTheory.Limits.biproduct.components	—	CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite
matrixDecompositionAddEquiv_symm_apply 📖	mathematical	CategoryTheory.HomOrthogonal	DFunLike.coe AddEquiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite Pi.instAdd Matrix Set.Elem Set.preimage Set Set.instSingletonSet CategoryTheory.End Matrix.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CategoryTheory.Preadditive.instRingEnd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm matrixDecompositionAddEquiv CategoryTheory.Limits.biproduct.matrix CategoryTheory.CategoryStruct.comp Set.instMembership CategoryTheory.eqToHom CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite
matrixDecompositionLinearEquiv_apply 📖	mathematical	CategoryTheory.HomOrthogonal	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Pi.addCommMonoid Matrix Set.Elem Set.preimage Set Set.instSingletonSet CategoryTheory.End Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CategoryTheory.Preadditive.instRingEnd CategoryTheory.Linear.homModule Pi.module Matrix.module CategoryTheory.Linear.instModuleEnd EquivLike.toFunLike LinearEquiv.instEquivLike matrixDecompositionLinearEquiv Equiv.toFun AddEquiv.toEquiv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Pi.instAdd Matrix.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib matrixDecompositionAddEquiv	—	RingHomInvPair.ids CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite
matrixDecompositionLinearEquiv_symm_apply 📖	mathematical	CategoryTheory.HomOrthogonal	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite Pi.addCommMonoid Matrix Set.Elem Set.preimage Set Set.instSingletonSet CategoryTheory.End Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CategoryTheory.Preadditive.instRingEnd AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Pi.module Matrix.module CategoryTheory.Linear.instModuleEnd CategoryTheory.Linear.homModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm matrixDecompositionLinearEquiv Equiv.invFun AddEquiv.toEquiv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Pi.instAdd Matrix.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib matrixDecompositionAddEquiv	—	RingHomInvPair.ids CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite
matrixDecomposition_apply 📖	mathematical	CategoryTheory.HomOrthogonal	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biproduct CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite EquivLike.toFunLike Equiv.instEquivLike matrixDecomposition CategoryTheory.CategoryStruct.comp Set Set.instMembership Set.preimage Set.instSingletonSet CategoryTheory.eqToHom CategoryTheory.Limits.biproduct.components	—	CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite
matrixDecomposition_comp 📖	mathematical	CategoryTheory.HomOrthogonal	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite EquivLike.toFunLike Equiv.instEquivLike matrixDecomposition CategoryTheory.CategoryStruct.comp Finite.of_fintype Matrix Set.Elem Set.preimage Set Set.instSingletonSet CategoryTheory.End Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Subtype.fintype Set.instMembership CategoryTheory.End.mul NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CategoryTheory.Preadditive.instRingEnd	—	CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite Finite.of_fintype Matrix.ext CategoryTheory.Category.assoc CategoryTheory.Category.comp_id Finset.sum_congr CategoryTheory.eqToHom_trans_assoc CategoryTheory.Category.id_comp CategoryTheory.Limits.biproduct.total CategoryTheory.Preadditive.sum_comp CategoryTheory.Preadditive.comp_sum Finset.sum_congr_set eq_zero CategoryTheory.Limits.comp_zero
matrixDecomposition_id 📖	mathematical	CategoryTheory.HomOrthogonal	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite EquivLike.toFunLike Equiv.instEquivLike matrixDecomposition CategoryTheory.CategoryStruct.id Matrix Set.Elem Set.preimage Set Set.instSingletonSet CategoryTheory.End Matrix.one Set.instMembership MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CategoryTheory.Preadditive.instRingEnd CategoryTheory.End.one	—	Matrix.ext CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.Limits.bicone_ι_π_self CategoryTheory.Limits.biproduct.ι_π_ne CategoryTheory.Limits.comp_zero
matrixDecomposition_symm_apply 📖	mathematical	CategoryTheory.HomOrthogonal	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biproduct CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite EquivLike.toFunLike Equiv.instEquivLike Equiv.symm matrixDecomposition CategoryTheory.Limits.biproduct.matrix CategoryTheory.CategoryStruct.comp Set Set.instMembership Set.preimage Set.instSingletonSet CategoryTheory.eqToHom CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite

---

← Back to Index