Isotypic

📁 Source: Mathlib/RingTheory/SimpleModule/Isotypic.lean

Statistics

Metric	Count
Definitions `setIsotypicComponents`, `IsIsotypic`, `IsIsotypicOfType`, `endAlgEquiv`, `endRingEquiv`, `setIsotypicComponents`, `IsFullyInvariant`, `fullyInvariantSubmodule`, `algEquiv`, `ringEquiv`, `isotypicComponent`, `isotypicComponents`	12
Theorems `isotypicComponent`, `isotypicComponents`, `linearEquiv_finsupp`, `linearEquiv_fun`, `of_injective`, `of_self`, `of_subsingleton`, `submodule_linearEquiv_fun`, `isIsotypic`, `isotypicComponent`, `linearEquiv_finsupp`, `linearEquiv_fun`, `of_injective`, `of_isSimpleModule`, `of_isotypicComponent_eq_top`, `of_linearEquiv_type`, `of_subsingleton`, `isIsotypicOfType_iff`, `isIsotypicOfType_iff_type`, `isIsotypic_iff`, `isotypicComponent_eq`, `le_comap_isotypicComponent`, `setIsotypicComponents_apply`, `setIsotypicComponents_symm_apply`, `isotypicComponent`, `of_mem_isotypicComponents`, `le_isotypicComponent`, `le_linearEquiv_of_le_sSup`, `le_linearEquiv_of_sSup_eq_top`, `linearEquiv_of_le_sSup`, `linearEquiv_of_sSup_eq_top`, `map_le_isotypicComponent`, `bot_lt_isotypicComponent`, `bot_lt_isotypicComponents`, `eq_isotypicComponent_iff`, `eq_isotypicComponent_of_le`, `instFiniteElemSubmoduleIsotypicComponentsOfIsNoetherian`, `instIsSemisimpleModuleSubtypeMemSubmoduleIsotypicComponent`, `instIsSemisimpleModuleSubtypeMemSubmoduleValSetIsotypicComponents`, `instIsSimpleModuleSubtypeMemSubmoduleValSetSetOfNonemptyLinearEquivId`, `instNontrivialSubtypeMemSubmoduleValSetIsotypicComponents`, `isFullyInvariant_iff_isTwoSided`, `isFullyInvariant_iff_le_imp_isotypicComponent_le`, `isFullyInvariant_iff_sSup_isotypicComponents`, `isIsotypicOfType_submodule_iff`, `isIsotypic_iff_isFullyInvariant_imp_bot_or_top`, `isIsotypic_submodule_iff`, `isotypicComponent_eq_top_iff`, `le_isotypicComponent_iff`, `mem_fullyInvariantSubmodule_iff`, `mem_isotypicComponents_iff`, `sSupIndep_isotypicComponents`, `sSup_isotypicComponents`	53
Total	65

GaloisCoinsertion

Definitions

Name	Category	Theorems
`setIsotypicComponents` 📖	CompOp	—

IsIsotypic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isotypicComponent` 📖	mathematical	—	`IsIsotypic` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `isotypicComponent` `Submodule.addCommGroup` `Submodule.module`	—	`IsIsotypicOfType.isIsotypic` `IsIsotypicOfType.isotypicComponent`
`isotypicComponents` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instMembership` `isotypicComponents`	`IsIsotypic` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module`	—	`isotypicComponent`
`linearEquiv_finsupp` 📖	mathematical	`IsIsotypic`	`IsSimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `Submodule.zero` `Finsupp.instAddCommMonoid` `Submodule.addCommMonoid` `Finsupp.module`	—	`RingHomInvPair.ids` `IsAtomic.exists_atom` `Submodule.instNontrivial` `isAtomic_of_complementedLattice` `Submodule.instIsModularLattice` `Submodule.instIsCompactlyGenerated` `IsSemisimpleModule.toComplementedLattice` `IsIsotypicOfType.linearEquiv_finsupp` `isSimpleModule_iff_isAtom` `isEmpty_or_nonempty` `not_subsingleton` `Equiv.subsingleton` `Unique.instSubsingleton`
`linearEquiv_fun` 📖	mathematical	`IsIsotypic`	`IsSimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Pi.addCommMonoid` `Submodule.addCommMonoid` `Pi.Function.module`	—	`RingHomInvPair.ids` `IsAtomic.exists_atom` `Submodule.instNontrivial` `isAtomic_of_complementedLattice` `Submodule.instIsModularLattice` `Submodule.instIsCompactlyGenerated` `IsSemisimpleModule.toComplementedLattice` `IsIsotypicOfType.linearEquiv_fun` `isSimpleModule_iff_isAtom` `not_subsingleton` `Equiv.subsingleton` `Unique.instSubsingleton` `Fin.isEmpty'`
`of_injective` 📖	—	`IsIsotypic` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	—	—	`RingHomInvPair.ids` `RingHomSurjective.invPair` `IsSimpleModule.congr` `IsIsotypicOfType.of_linearEquiv_type` `RingHomSurjective.ids` `IsIsotypicOfType.of_injective`
`of_self` 📖	—	`IsIsotypic` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring`	—	—	`RingHomInvPair.ids` `IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule` `IsSimpleModule.congr` `RingHomCompTriple.ids`
`of_subsingleton` 📖	mathematical	—	`IsIsotypic`	—	`IsIsotypicOfType.isIsotypic` `IsIsotypicOfType.of_subsingleton`
`submodule_linearEquiv_fun` 📖	mathematical	`IsIsotypic` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module`	`Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `IsSimpleModule` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule.addCommMonoid` `Pi.addCommMonoid` `Pi.Function.module`	—	`RingHomInvPair.ids` `linearEquiv_fun` `IsSemisimpleModule.submodule` `RingHomSurjective.invPair` `Submodule.subtype_injective` `RingHomSurjective.ids` `Submodule.map_subtype_le` `IsSimpleModule.congr` `RingHomCompTriple.ids`

IsIsotypicOfType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIsotypic` 📖	mathematical	`IsIsotypicOfType`	`IsIsotypic`	—	`RingHomCompTriple.ids`
`isotypicComponent` 📖	mathematical	—	`IsIsotypicOfType` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `isotypicComponent` `Submodule.addCommGroup` `Submodule.module`	—	`RingHomInvPair.ids` `isIsotypicOfType_submodule_iff` `Submodule.linearEquiv_of_le_sSup` `instIsSimpleModuleSubtypeMemSubmoduleValSetSetOfNonemptyLinearEquivId` `RingHomCompTriple.ids`
`linearEquiv_finsupp` 📖	mathematical	`IsIsotypicOfType`	`LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module`	—	`RingHomInvPair.ids` `IsSemisimpleModule.exists_linearEquiv_dfinsupp` `RingHomCompTriple.ids`
`linearEquiv_fun` 📖	mathematical	`IsIsotypicOfType`	`LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Pi.addCommMonoid` `Pi.Function.module`	—	`RingHomInvPair.ids` `IsSemisimpleModule.exists_linearEquiv_fin_dfinsupp` `RingHomCompTriple.ids` `Finite.of_fintype`
`of_injective` 📖	—	`IsIsotypicOfType` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	—	—	`RingHomInvPair.ids` `RingHomSurjective.invPair` `IsSimpleModule.congr` `RingHomCompTriple.ids` `RingHomSurjective.ids`
`of_isSimpleModule` 📖	mathematical	—	`IsIsotypicOfType`	—	`RingHomCompTriple.ids` `RingHomInvPair.ids` `isAtom_iff_eq_top` `IsSimpleModule.toIsSimpleOrder` `isSimpleModule_iff_isAtom`
`of_isotypicComponent_eq_top` 📖	mathematical	`isotypicComponent` `Top.top` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instTop`	`IsIsotypicOfType`	—	`RingHomInvPair.ids` `Submodule.linearEquiv_of_sSup_eq_top` `instIsSimpleModuleSubtypeMemSubmoduleValSetSetOfNonemptyLinearEquivId` `RingHomCompTriple.ids`
`of_linearEquiv_type` 📖	—	`IsIsotypicOfType`	—	—	`RingHomInvPair.ids` `RingHomCompTriple.ids`
`of_subsingleton` 📖	mathematical	—	`IsIsotypicOfType`	—	`IsSimpleModule.nontrivial` `not_subsingleton` `Function.Injective.subsingleton` `Submodule.subtype_injective`

IsSemisimpleModule

Definitions

Name	Category	Theorems
`endAlgEquiv` 📖	CompOp	—
`endRingEquiv` 📖	CompOp	—

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIsotypicOfType_iff` 📖	mathematical	—	`IsIsotypicOfType`	—	`RingHomInvPair.ids` `IsIsotypicOfType.of_injective` `injective`
`isIsotypicOfType_iff_type` 📖	mathematical	—	`IsIsotypicOfType`	—	`RingHomInvPair.ids` `IsIsotypicOfType.of_linearEquiv_type`
`isIsotypic_iff` 📖	mathematical	—	`IsIsotypic`	—	`RingHomInvPair.ids` `IsIsotypic.of_injective` `injective`
`isotypicComponent_eq` 📖	mathematical	—	`isotypicComponent`	—	`RingHomInvPair.ids` `Set.ext` `Nonempty.congr` `RingHomCompTriple.ids`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_comap_isotypicComponent` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `isotypicComponent` `Submodule.comap` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`sSup_le` `RingHomSurjective.ids` `Submodule.map_le_iff_le_comap` `IsSimpleModule.congr` `LE.le.trans_eq` `Submodule.map_le_isotypicComponent` `LinearEquiv.isotypicComponent_eq`

OrderIso

Definitions

Name	Category	Theorems
`setIsotypicComponents` 📖	CompOp	2 math math: `setIsotypicComponents_apply`, `setIsotypicComponents_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`setIsotypicComponents_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Set` `Set.Elem` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `isotypicComponents` `CompleteSublattice` `Submodule.completeLattice` `SetLike.instMembership` `CompleteSublattice.instSetLike` `fullyInvariantSubmodule` `Set.instLE` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `RelIso.instFunLike` `setIsotypicComponents` `iSup` `CompleteSublattice.instSupSet` `Set.instMembership`	—	—
`setIsotypicComponents_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `CompleteSublattice` `Submodule.completeLattice` `SetLike.instMembership` `CompleteSublattice.instSetLike` `fullyInvariantSubmodule` `Set` `Set.Elem` `isotypicComponents` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Set.instLE` `RelIso.instFunLike` `RelIso.symm` `setIsotypicComponents` `setOf` `Set.instMembership`	—	—

Submodule

Definitions

Name	Category	Theorems
`IsFullyInvariant` 📖	MathDef	8 math math: `isFullyInvariant_iff_sSup_isotypicComponents`, `eq_isotypicComponent_iff`, `IsFullyInvariant.isotypicComponent`, `mem_fullyInvariantSubmodule_iff`, `mem_isotypicComponents_iff`, `IsFullyInvariant.of_mem_isotypicComponents`, `isFullyInvariant_iff_isTwoSided`, `isFullyInvariant_iff_le_imp_isotypicComponent_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_isotypicComponent` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `isotypicComponent` `SetLike.instMembership` `setLike` `addCommGroup` `module`	—	`le_sSup`
`le_linearEquiv_of_le_sSup` 📖	mathematical	`IsSemisimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `Set` `Set.instMembership` `addCommGroup` `module` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice`	`LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `addCommMonoid`	—	`RingHomInvPair.ids` `RingHomSurjective.invPair` `sSup_eq_iSup` `inclusion_injective` `IsSimpleModule.congr` `isSemisimpleModule_biSup_of_isSemisimpleModule_submodule` `RingHomSurjective.ids` `le_linearEquiv_of_sSup_eq_top` `sSup_image` `biSup_comap_subtype_eq_top` `map_le_iff_le_comap` `RingHomCompTriple.ids` `subtype_injective`
`le_linearEquiv_of_sSup_eq_top` 📖	mathematical	`SupSet.sSup` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `Top.top` `instTop`	`Set` `Set.instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	—	`IsSimpleModule.nontrivial` `RingHomInvPair.ids` `ComplementedLattice.exists_isCompl` `IsSemisimpleModule.toComplementedLattice` `RingHomCompTriple.ids` `LinearMap.exists_ne_zero_of_sSup_eq_top` `LinearMap.ne_zero_of_surjective` `linearProjOfIsCompl_surjective` `LinearMap.linearEquiv_of_ne_zero` `IsSemisimpleModule.submodule` `RingHomSurjective.ids` `map_subtype_le` `subtype_injective`
`linearEquiv_of_le_sSup` 📖	mathematical	`IsSimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `Set` `Set.instMembership` `addCommGroup` `module` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice`	`LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `addCommMonoid`	—	`RingHomInvPair.ids` `le_linearEquiv_of_le_sSup` `instIsSemisimpleModuleOfIsSimpleModule` `isSimpleModule_iff_isAtom` `IsSimpleModule.congr` `IsAtom.le_iff_eq` `RingHomCompTriple.ids`
`linearEquiv_of_sSup_eq_top` 📖	mathematical	`IsSimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `Set` `Set.instMembership` `addCommGroup` `module` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `Top.top` `instTop`	`LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `addCommMonoid`	—	`isSemisimpleModule_of_isSemisimpleModule_submodule'` `instIsSemisimpleModuleOfIsSimpleModule` `sSup_eq_iSup'` `RingHomInvPair.ids` `le_linearEquiv_of_sSup_eq_top` `isSimpleModule_iff_isAtom` `IsSimpleModule.congr` `IsAtom.le_iff_eq` `RingHomCompTriple.ids`
`map_le_isotypicComponent` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `isotypicComponent` `SetLike.instMembership` `setLike` `addCommGroup` `module`	—	`RingHomSurjective.ids` `RingHomCompTriple.ids` `range_subtype` `LinearMap.range_comp` `LinearMap.injective_or_eq_zero` `le_sSup` `LinearMap.range.congr_simp` `LinearMap.range_zero`

Submodule.IsFullyInvariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isotypicComponent` 📖	mathematical	—	`Submodule.IsFullyInvariant` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `isotypicComponent`	—	`LinearMap.le_comap_isotypicComponent`
`of_mem_isotypicComponents` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instMembership` `isotypicComponents`	`Submodule.IsFullyInvariant`	—	`isotypicComponent`

(root)

Definitions

Name	Category	Theorems
`IsIsotypic` 📖	MathDef	10 math math: `IsIsotypic.isotypicComponents`, `IsIsotypicOfType.isIsotypic`, `isIsotypic_submodule_iff`, `IsIsotypic.isotypicComponent`, `IsIsotypic.of_subsingleton`, `LinearEquiv.isIsotypic_iff`, `mem_isotypicComponents_iff`, `isSimpleRing_isArtinianRing_iff`, `isIsotypic_iff_isFullyInvariant_imp_bot_or_top`, `IsSimpleRing.isIsotypic`
`IsIsotypicOfType` 📖	MathDef	11 math math: `isIsotypicOfType_submodule_iff`, `eq_isotypicComponent_iff`, `isotypicComponent_eq_top_iff`, `isIsotypic_submodule_iff`, `LinearEquiv.isIsotypicOfType_iff_type`, `IsIsotypicOfType.of_isotypicComponent_eq_top`, `IsIsotypicOfType.of_subsingleton`, `LinearEquiv.isIsotypicOfType_iff`, `IsIsotypicOfType.of_isSimpleModule`, `le_isotypicComponent_iff`, `IsIsotypicOfType.isotypicComponent`
`fullyInvariantSubmodule` 📖	CompOp	3 math math: `OrderIso.setIsotypicComponents_apply`, `mem_fullyInvariantSubmodule_iff`, `OrderIso.setIsotypicComponents_symm_apply`
`isotypicComponent` 📖	CompOp	14 math math: `bot_lt_isotypicComponent`, `eq_isotypicComponent_iff`, `isotypicComponent_eq_top_iff`, `eq_isotypicComponent_of_le`, `Submodule.IsFullyInvariant.isotypicComponent`, `IsIsotypic.isotypicComponent`, `instIsSemisimpleModuleSubtypeMemSubmoduleIsotypicComponent`, `Submodule.le_isotypicComponent`, `Submodule.map_le_isotypicComponent`, `le_isotypicComponent_iff`, `LinearMap.le_comap_isotypicComponent`, `isFullyInvariant_iff_le_imp_isotypicComponent_le`, `IsIsotypicOfType.isotypicComponent`, `LinearEquiv.isotypicComponent_eq`
`isotypicComponents` 📖	CompOp	9 math math: `isFullyInvariant_iff_sSup_isotypicComponents`, `OrderIso.setIsotypicComponents_apply`, `sSup_isotypicComponents`, `sSupIndep_isotypicComponents`, `mem_isotypicComponents_iff`, `instFiniteElemSubmoduleIsotypicComponentsOfIsNoetherian`, `instIsSemisimpleModuleSubtypeMemSubmoduleValSetIsotypicComponents`, `instNontrivialSubtypeMemSubmoduleValSetIsotypicComponents`, `OrderIso.setIsotypicComponents_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_lt_isotypicComponent` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Bot.bot` `Submodule.instBot` `isotypicComponent` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module`	—	`LT.lt.trans_le` `bot_lt_iff_ne_bot` `Submodule.nontrivial_iff_ne_bot` `IsSimpleModule.nontrivial` `Submodule.le_isotypicComponent`
`bot_lt_isotypicComponents` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instMembership` `isotypicComponents`	`Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Bot.bot` `Submodule.instBot`	—	`bot_lt_isotypicComponent`
`eq_isotypicComponent_iff` 📖	mathematical	—	`isotypicComponent` `IsIsotypicOfType` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module` `Submodule.IsFullyInvariant`	—	`IsIsotypicOfType.isotypicComponent` `Submodule.IsFullyInvariant.isotypicComponent` `LE.le.antisymm` `le_isotypicComponent_iff` `IsSemisimpleModule.eq_bot_or_exists_simple_le` `IsSemisimpleModule.submodule` `Eq.trans_le` `LinearEquiv.isotypicComponent_eq` `RingHomInvPair.ids` `isIsotypicOfType_submodule_iff` `isFullyInvariant_iff_le_imp_isotypicComponent_le`
`eq_isotypicComponent_of_le` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instMembership` `isotypicComponents` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	`isotypicComponent` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module`	—	`RingHomInvPair.ids` `isIsotypicOfType_submodule_iff` `IsIsotypicOfType.isotypicComponent` `LinearEquiv.isotypicComponent_eq`
`instFiniteElemSubmoduleIsotypicComponentsOfIsNoetherian` 📖	mathematical	—	`Finite` `Set.Elem` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `isotypicComponents`	—	`Set.finite_coe_iff` `WellFoundedGT.finite_of_sSupIndep` `wellFoundedGT` `sSupIndep_isotypicComponents`
`instIsSemisimpleModuleSubtypeMemSubmoduleIsotypicComponent` 📖	mathematical	—	`IsSemisimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `isotypicComponent` `Submodule.addCommGroup` `Submodule.module`	—	`isotypicComponent.eq_1` `sSup_eq_iSup` `isSemisimpleModule_biSup_of_isSemisimpleModule_submodule` `IsSemisimpleModule.congr`
`instIsSemisimpleModuleSubtypeMemSubmoduleValSetIsotypicComponents` 📖	mathematical	—	`IsSemisimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Set` `Set.instMembership` `isotypicComponents` `Submodule.addCommGroup` `Submodule.module`	—	`instIsSemisimpleModuleSubtypeMemSubmoduleIsotypicComponent` `instIsSemisimpleModuleOfIsSimpleModule`
`instIsSimpleModuleSubtypeMemSubmoduleValSetSetOfNonemptyLinearEquivId` 📖	mathematical	—	`IsSimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Set` `Set.instMembership` `setOf` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule.addCommMonoid` `Submodule.module` `Submodule.addCommGroup`	—	`RingHomInvPair.ids` `IsSimpleModule.congr`
`instNontrivialSubtypeMemSubmoduleValSetIsotypicComponents` 📖	mathematical	—	`Nontrivial` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Set` `Set.instMembership` `isotypicComponents`	—	`Submodule.nontrivial_iff_ne_bot` `LT.lt.ne'` `bot_lt_isotypicComponents`
`isFullyInvariant_iff_isTwoSided` 📖	mathematical	—	`Submodule.IsFullyInvariant` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.IsTwoSided`	—	`instIsConcreteLE` `Equiv.forall_congr_right` `Ideal.isTwoSided_iff`
`isFullyInvariant_iff_le_imp_isotypicComponent_le` 📖	mathematical	—	`Submodule.IsFullyInvariant` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `isotypicComponent` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module`	—	`sSup_le` `RingHomCompTriple.ids` `IsSemisimpleModule.extension_property` `Submodule.subtype_injective` `le_trans` `RingHomSurjective.ids` `Submodule.range_subtype` `LinearMap.range_comp` `LinearEquiv.range_comp` `le_refl` `Submodule.map_le_iff_le_comap` `LE.le.trans` `Eq.ge` `IsSemisimpleModule.sSup_simples_le` `Submodule.map_le_isotypicComponent`
`isFullyInvariant_iff_sSup_isotypicComponents` 📖	mathematical	—	`Submodule.IsFullyInvariant` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Submodule` `Set.instHasSubset` `isotypicComponents` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	—	`sSup_image` `CompleteSublattice.coe_iSup` `iSup_congr_Prop` `Equiv.right_inv` `CompleteSublattice.sSupClosed` `Submodule.IsFullyInvariant.of_mem_isotypicComponents`
`isIsotypicOfType_submodule_iff` 📖	mathematical	—	`IsIsotypicOfType` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule.addCommMonoid`	—	`RingHomInvPair.ids` `Subtype.forall'` `Equiv.forall_congr_right` `RingHomSurjective.invPair` `Submodule.subtype_injective` `RingHomSurjective.ids` `Submodule.map_subtype_le` `LinearEquiv.isSimpleModule_iff` `RingHomCompTriple.ids`
`isIsotypic_iff_isFullyInvariant_imp_bot_or_top` 📖	mathematical	—	`IsIsotypic` `Bot.bot` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instBot` `Top.top` `Submodule.instTop`	—	`top_unique` `LE.le.trans` `Eq.ge` `isotypicComponent_eq_top_iff` `isFullyInvariant_iff_le_imp_isotypicComponent_le` `IsSemisimpleModule.eq_bot_or_exists_simple_le` `IsSemisimpleModule.submodule` `Submodule.IsFullyInvariant.isotypicComponent` `LT.lt.ne'` `bot_lt_isotypicComponent`
`isIsotypic_submodule_iff` 📖	mathematical	—	`IsIsotypic` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module` `IsIsotypicOfType`	—	`Subtype.forall'` `Equiv.forall_congr_right` `RingHomInvPair.ids` `RingHomSurjective.invPair` `Submodule.subtype_injective` `RingHomSurjective.ids` `Submodule.map_subtype_le` `LinearEquiv.isSimpleModule_iff` `LinearEquiv.isIsotypicOfType_iff_type`
`isotypicComponent_eq_top_iff` 📖	mathematical	—	`isotypicComponent` `Top.top` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instTop` `IsIsotypicOfType`	—	`top_le_iff` `le_isotypicComponent_iff` `LinearEquiv.isIsotypicOfType_iff`
`le_isotypicComponent_iff` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `isotypicComponent` `IsIsotypicOfType` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module`	—	`IsIsotypicOfType.of_injective` `IsIsotypicOfType.isotypicComponent` `Submodule.inclusion_injective` `LE.le.trans` `Eq.ge` `IsSemisimpleModule.sSup_simples_le` `sSup_le_sSup` `RingHomInvPair.ids` `isIsotypicOfType_submodule_iff`
`mem_fullyInvariantSubmodule_iff` 📖	mathematical	—	`Submodule` `CompleteSublattice` `Submodule.completeLattice` `SetLike.instMembership` `CompleteSublattice.instSetLike` `fullyInvariantSubmodule` `Submodule.IsFullyInvariant`	—	—
`mem_isotypicComponents_iff` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instMembership` `isotypicComponents` `IsIsotypic` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module` `Submodule.IsFullyInvariant`	—	`IsIsotypic.isotypicComponent` `Submodule.IsFullyInvariant.isotypicComponent` `LT.lt.ne'` `bot_lt_isotypicComponent` `IsSemisimpleModule.eq_bot_or_exists_simple_le` `IsSemisimpleModule.submodule` `eq_isotypicComponent_iff` `isIsotypic_submodule_iff`
`sSupIndep_isotypicComponents` 📖	mathematical	—	`sSupIndep` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.completeLattice` `isotypicComponents`	—	`disjoint_iff` `of_not_not` `instIsSemisimpleModuleSubtypeMemSubmoduleIsotypicComponent` `instIsSemisimpleModuleOfIsSimpleModule` `IsSemisimpleModule.of_injective` `inf_le_left` `Submodule.inclusion_injective` `IsSemisimpleModule.eq_bot_or_exists_simple_le` `RingHomInvPair.ids` `Submodule.le_linearEquiv_of_le_sSup` `LE.le.trans` `inf_le_right` `IsSimpleModule.congr` `eq_isotypicComponent_of_le` `LinearEquiv.isotypicComponent_eq`
`sSup_isotypicComponents` 📖	mathematical	—	`SupSet.sSup` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `isotypicComponents` `Top.top` `Submodule.instTop`	—	`isFullyInvariant_iff_sSup_isotypicComponents` `CompleteSublattice.top_mem` `top_unique` `LE.le.trans` `Eq.le` `sSup_le_sSup`

iSupIndep

Definitions

Name	Category	Theorems
`algEquiv` 📖	CompOp	—
`ringEquiv` 📖	CompOp	—

---

← Back to Index