Decomposition

📁 Source: Mathlib/Algebra/DirectSum/Decomposition.lean

Statistics

Metric	Count
Definitions `Decomposition`, `decompose'`, `ofAddHom`, `ofLinearMap`, `chooseDecomposition`, `IsHomogeneous`, `addCommGroupSetLike`, `decompose`, `decomposeAddEquiv`, `decomposeLinearEquiv`	10
Theorems `ext`, `mem_iff`, `decompose'_eq`, `inductionOn`, `isInternal`, `left_inv`, `right_inv`, `decomposeAddEquiv_apply`, `decomposeAddEquiv_symm_apply`, `decomposeLinearEquiv_apply`, `decomposeLinearEquiv_symm_apply`, `decomposeLinearEquiv_symm_comp_lof`, `decompose_add`, `decompose_coe`, `decompose_lhom_ext`, `decompose_neg`, `decompose_of_mem`, `decompose_of_mem_ne`, `decompose_of_mem_same`, `decompose_smul`, `decompose_sub`, `decompose_sum`, `decompose_symm_add`, `decompose_symm_neg`, `decompose_symm_of`, `decompose_symm_sub`, `decompose_symm_sum`, `decompose_symm_zero`, `decompose_zero`, `degree_eq_of_mem_mem`, `instSubsingletonDecomposition`, `sum_support_decompose`	32
Total	42

DirectSum

Definitions

Name	Category	Theorems
`Decomposition` 📖	CompData	1 math math: `instSubsingletonDecomposition`
`addCommGroupSetLike` 📖	CompOp	4 math math: `decompose_sub`, `decompose_symm_sub`, `decompose_symm_neg`, `decompose_neg`
`decompose` 📖	CompOp	60 math math: `decompose_sub`, `Decomposition.decompose'_eq`, `decompose_of_mem_same`, `decomposeAlgEquiv_symm_apply`, `LinearMap.IsSymmetric.directSum_decompose_apply`, `decompose_eq_mul_idempotent`, `decompose_of_mem`, `decompose_symm_sub`, `coe_decompose_mul_add_of_left_mem`, `decompose_symm_neg`, `coe_decompose_mul_of_left_mem_of_le`, `decompose_symm_one`, `coe_decompose_mul_of_left_mem`, `GradedAlgebra.proj_recompose`, `decompose_mul_add_left`, `decompose_symm_algebraMap`, `decompose_symm_add`, `coe_decompose_mul_of_right_mem_of_not_le`, `coe_decompose_mul_of_left_mem_of_not_le`, `decompose_algebraMap`, `AddMonoidAlgebra.GradesBy.decompose_single`, `GradedRing.mem_support_iff`, `coe_decompose_mul_of_right_mem`, `GradedTensorProduct.auxEquiv_tmul`, `decomposeLinearEquiv_apply`, `coe_decompose_mul_add_of_right_mem`, `decompose_zero`, `decomposeLinearEquiv_symm_apply`, `decomposeAlgEquiv_apply`, `AddMonoidAlgebra.grade.decompose_single`, `decompose_of_mem_ne`, `Submodule.IsHomogeneous.mem_iff`, `SetLike.IsHomogeneous.mem_iff`, `decompose_symm_mul`, `GradedAlgebra.proj_apply`, `decomposeAddEquiv_symm_apply`, `GradedRing.projZeroRingHom_apply`, `decompose_symm_zero`, `decomposeAddEquiv_apply`, `decompose_mul`, `decompose_coe`, `decompose_one`, `decompose_mul_add_right`, `AddMonoidAlgebra.decomposeAux_eq_decompose`, `coe_decompose_mul_of_left_mem_zero`, `coe_decompose_mul_of_right_mem_of_le`, `sum_support_decompose`, `coe_decompose_mul_of_right_mem_zero`, `AddSubmonoidClass.IsHomogeneous.mem_iff`, `GradedAlgebra.mem_support_iff`, `decompose_symm_of`, `AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen`, `decompose_neg`, `decompose_symm_sum`, `decompose_add`, `decompose_sum`, `decompose_smul`, `GradedRing.proj_apply`, `GradedRing.proj_recompose`, `Ideal.IsHomogeneous.mem_iff`
`decomposeAddEquiv` 📖	CompOp	2 math math: `decomposeAddEquiv_symm_apply`, `decomposeAddEquiv_apply`
`decomposeLinearEquiv` 📖	CompOp	3 math math: `decomposeLinearEquiv_apply`, `decomposeLinearEquiv_symm_comp_lof`, `decomposeLinearEquiv_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`decomposeAddEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidDirectSum` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `decomposeAddEquiv` `Equiv` `Equiv.instEquivLike` `decompose`	—	—
`decomposeAddEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidDirectSum` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `decomposeAddEquiv` `Equiv` `Equiv.instEquivLike` `Equiv.symm` `decompose`	—	—
`decomposeLinearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `DirectSum` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `instAddCommMonoidDirectSum` `instModule` `Submodule.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `decomposeLinearEquiv` `Equiv` `AddSubmonoidClass.toAddCommMonoid` `Submodule.addSubmonoidClass` `Equiv.instEquivLike` `decompose`	—	`Submodule.addSubmonoidClass` `RingHomInvPair.ids`
`decomposeLinearEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `DirectSum` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `instAddCommMonoidDirectSum` `instModule` `Submodule.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `decomposeLinearEquiv` `Equiv` `AddSubmonoidClass.toAddCommMonoid` `Submodule.addSubmonoidClass` `Equiv.instEquivLike` `Equiv.symm` `decompose`	—	`Submodule.addSubmonoidClass` `RingHomInvPair.ids`
`decomposeLinearEquiv_symm_comp_lof` 📖	mathematical	—	`LinearMap.comp` `Submodule` `SetLike.instMembership` `Submodule.setLike` `DirectSum` `Submodule.addCommMonoid` `instAddCommMonoidDirectSum` `Submodule.module` `instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearEquiv.symm` `decomposeLinearEquiv` `lof` `Submodule.subtype`	—	`Submodule.addSubmonoidClass` `LinearMap.ext` `RingHomCompTriple.ids` `RingHomInvPair.ids` `decompose_symm_of`
`decompose_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidDirectSum`	—	`map_add` `AddMonoidHomClass.toAddHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`decompose_coe` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of`	—	`decompose_symm_of` `Equiv.apply_symm_apply`
`decompose_lhom_ext` 📖	—	`LinearMap.comp` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `Submodule.subtype`	—	—	`Submodule.addSubmonoidClass` `RingHomCompTriple.ids` `LinearMap.ext` `RingHomInvPair.ids` `Function.Surjective.forall` `LinearEquiv.surjective` `linearMap_ext` `LinearMap.comp.congr_simp` `decomposeLinearEquiv_symm_comp_lof` `DFunLike.congr_fun`
`decompose_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `AddCommGroup.toAddCommMonoid` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addCommGroupSetLike`	—	`AddSubgroupClass.toAddSubmonoidClass` `map_neg` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`decompose_of_mem` 📖	mathematical	`SetLike.instMembership`	`DFunLike.coe` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of`	—	`decompose_coe`
`decompose_of_mem_ne` 📖	mathematical	`SetLike.instMembership`	`DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose`	—	`decompose_of_mem` `of_eq_of_ne` `ZeroMemClass.coe_zero`
`decompose_of_mem_same` 📖	mathematical	`SetLike.instMembership`	`DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose`	—	`decompose_of_mem` `of_eq_same`
`decompose_smul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `Submodule` `SetLike.instMembership` `Submodule.setLike` `AddSubmonoidClass.toAddCommMonoid` `Submodule.addSubmonoidClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `instAddCommMonoidDirectSum` `instModule` `Submodule.module`	—	`Submodule.addSubmonoidClass` `map_smul` `RingHomInvPair.ids` `SemilinearMapClass.toMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass`
`decompose_sub` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `AddCommGroup.toAddCommMonoid` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `SubNegMonoid.toSub` `addCommGroupSetLike`	—	`AddSubgroupClass.toAddSubmonoidClass` `map_sub` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`decompose_sum` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `Finset.sum` `instAddCommMonoidDirectSum`	—	`map_sum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`decompose_symm_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `decompose` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidDirectSum`	—	`map_add` `AddMonoidHomClass.toAddHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`decompose_symm_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `AddCommGroup.toAddCommMonoid` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `decompose` `AddSubgroupClass.toAddCommGroup` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addCommGroupSetLike`	—	`AddSubgroupClass.toAddSubmonoidClass` `map_neg` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`decompose_symm_of` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `decompose` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of`	—	`coeAddMonoidHom_of`
`decompose_symm_sub` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `AddCommGroup.toAddCommMonoid` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `decompose` `AddSubgroupClass.toAddCommGroup` `SubNegMonoid.toSub` `addCommGroupSetLike`	—	`AddSubgroupClass.toAddSubmonoidClass` `map_sub` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`decompose_symm_sum` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `decompose` `Finset.sum` `instAddCommMonoidDirectSum`	—	`map_sum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`decompose_symm_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `decompose` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`decompose_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`degree_eq_of_mem_mem` 📖	—	`SetLike.instMembership`	—	—	`Mathlib.Tactic.Contrapose.contrapose₂` `decompose_of_mem_same` `decompose_of_mem_ne`
`instSubsingletonDecomposition` 📖	mathematical	—	`Decomposition`	—	`Function.LeftInverse.eq_rightInverse`
`sum_support_decompose` 📖	mathematical	—	`Finset.sum` `DFinsupp.support` `SetLike.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `DFinsupp` `DFinsupp.instDFunLike`	—	`AddSubmonoidClass.toZeroMemClass` `Equiv.symm_apply_apply` `sum_support_of` `decompose_symm_sum` `Finset.sum_congr` `decompose_symm_of`

DirectSum.AddSubmonoidClass.IsHomogeneous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`DirectSum.SetLike.IsHomogeneous` `SetLike.instMembership`	—	—	`SetLike.ext` `mem_iff`
`mem_iff` 📖	mathematical	`DirectSum.SetLike.IsHomogeneous`	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `DirectSum.decompose`	—	`AddSubmonoidClass.toZeroMemClass` `DirectSum.sum_support_decompose` `sum_mem`

DirectSum.Decomposition

Definitions

Name	Category	Theorems
`decompose'` 📖	CompOp	7 math math: `decompose'_eq`, `MvPolynomial.weightedDecomposition.decompose'_apply`, `MvPolynomial.decomposition.decompose'_apply`, `MvPolynomial.weightedDecomposition.decompose'_eq`, `left_inv`, `right_inv`, `MvPolynomial.decomposition.decompose'_eq`
`ofAddHom` 📖	CompOp	—
`ofLinearMap` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`decompose'_eq` 📖	mathematical	—	`decompose'` `DFunLike.coe` `Equiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `DirectSum.decompose`	—	—
`inductionOn` 📖	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—	`AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `DirectSum.IsInternal.addSubmonoid_iSup_eq_top` `isInternal` `AddSubmonoid.instAddSubmonoidClass` `Equiv.left_inv` `Equiv.right_inv` `AddSubmonoid.iSup_induction`
`isInternal` 📖	mathematical	—	`DirectSum.IsInternal`	—	`Function.RightInverse.injective` `right_inv` `Function.LeftInverse.surjective` `left_inv`
`left_inv` 📖	mathematical	—	`DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `DirectSum.coeAddMonoidHom` `decompose'`	—	—
`right_inv` 📖	mathematical	—	`DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `DirectSum.coeAddMonoidHom` `decompose'`	—	—

DirectSum.IsInternal

Definitions

Name	Category	Theorems
`chooseDecomposition` 📖	CompOp	—

DirectSum.SetLike

Definitions

Name	Category	Theorems
`IsHomogeneous` 📖	MathDef	6 math math: `IsHomogeneous.subsemiringClosure`, `Subsemiring.isHomogeneous_iff_subset_iInter`, `Subsemiring.isHomogeneous_iff_forall_subset`, `HomogeneousSubsemiring.isHomogeneous`, `HomogeneousSubsemiring.is_homogeneous'`, `IsHomogeneous.subsemiringClosure_of_isHomogeneousElem`

---

← Back to Index