← all areas

Namespace IharaLemma 24 theorems

— 18 · IdempotentSplitting 6

directly in IharaLemma 18

• Idempotent splitting of a stable submodule with orthogonal complement IharaLemma.exists_isCompl_orthogonal_of_isIdempotentElem_of_selfAdjoint 0 below · cited by 2 · depth 13
• Elements of mathfrak mᵢ are topologically nilpotent on the eᵢ-corner IharaLemma.exists_pow_smul_corner_mem_maximalIdeal_smul 0 below · cited by 10 · depth 13
• Freeness of the corner submodule at an idempotent IharaLemma.free_cornerSubmodule 0 below · cited by 7 · depth 13
• Saturation and rank force equality of images at a corner IharaLemma.map_codRestrict_eq_of_residual 0 below · cited by 1 · depth 13
• Corner transport along an 𝒪-linear intertwining map IharaLemma.map_le_cornerSubmodule_of_adjoin_eq_top_of_forall_exists_partner 2 below · cited by 2 · depth 13
• Transport of idempotent corners along an intertwining map IharaLemma.map_le_cornerSubmodule_of_forall_ne_exists_intertwining 0 below · cited by 2 · depth 13
• Fullness of a corner under adic generalised eigenvector conditions IharaLemma.mem_cornerSubmodule_of_forall_exists_pow_sub_algebraMap_smul_mem 0 below · cited by 5 · depth 13
• Vanishing on a corner against a topologically nilpotent intertwiner IharaLemma.eq_zero_of_mem_cornerSubmodule_of_intertwining_nilpotent 0 below · cited by 1 · depth 14
• Injectivity of a localised map with S-torsion kernel IharaLemma.injective_of_ker_le_torsion 0 below · cited by 1 · depth 14
• Divisibility reflected by an injective reduction IharaLemma.resInj_of_reduction 0 below · cited by 2 · depth 14
• Kernel bound ker(red)⊆varpi V localises IharaLemma.resKer_localized 0 below · cited by 2 · depth 14
• Order-n residually trivial element acts trivially on a corner IharaLemma.smul_eq_self_of_mem_cornerSubmodule_of_pow_eq_one 0 below · cited by 1 · depth 14
• Commuting squares of modules descend to localisations IharaLemma.square_localized 0 below · cited by 2 · depth 14
• Finiteness of the corner submodule eV over the base ring IharaLemma.finite_cornerSubmodule 0 below · cited by 2 · depth 15
• Localised modules descend along a surjection of base rings IharaLemma.isLocalizedModule_comap_primeCompl 0 below · cited by 2 · depth 15
• Idempotent splitting of a finite algebra over a complete local ring IharaLemma.nonempty_idempotentSplitting_of_finite 1 below · cited by 8 · depth 15
• Idempotent corner realises localisation at a maximal ideal IharaLemma.isLocalizedModule_toCorner 0 below · cited by 1 · depth 16
• Finite modules over an I-adically precomplete ring are precomplete IharaLemma.isPrecomplete_of_finite 0 below · cited by 1 · depth 16

IharaLemma.IdempotentSplitting 6

• Annihilated elements lie in the corner of the splitting IharaLemma.IdempotentSplitting.eq_smul_of_smul_eq_zero 0 below · cited by 2 · depth 15
• Corner maps of an idempotent splitting are localizations IharaLemma.IdempotentSplitting.isLocalizedModule_toCorner_maximalIdeal 1 below · cited by 6 · depth 15
• Corner rings of an idempotent splitting are module-finite IharaLemma.IdempotentSplitting.finite_cornerRing 0 below · cited by 2 · depth 16
• Freeness of the corner ring over a local base IharaLemma.IdempotentSplitting.free_cornerRing 0 below · cited by 1 · depth 16
• Maximal ideal of a splitting as kernel of a residual corner point IharaLemma.IdempotentSplitting.mem_maxIdeal_iff_apply_toCornerRing_eq_zero 0 below · cited by 2 · depth 17
• Corner of a free module is free over the corner ring IharaLemma.IdempotentSplitting.exists_basis_cornerSubmodule_coe_eq_smul 0 below · cited by 1 · depth 26