← all areas

Namespace IharaTower 17 theorems

— 12 · CornerData 1 · RungAssembly 3 · RungDatum 1

directly in IharaTower 12

• Two-leg degeneracy descent between levels N and Nq IharaTower.exists_degeneracyDescent_iDegL_jDegL_two 5 below · cited by 2 · depth 12
• Residual injectivity of combined raising at diamond-invariant corner IharaTower.exists_eq_smul_of_iComb_eq_smul_of_isEis_kernel_pair_of_diamond_invariant 1 below · cited by 1 · depth 12
• A rung datum from the two q-degeneracy legs at level Nq IharaTower.exists_rungDatum_two 7 below · cited by 1 · depth 12
• Ihara clause and Ihara datum at a corner rung IharaTower.iharaClauseAt_and_isIharaDataAt_cornerRung 2 below · cited by 2 · depth 12
• Ihara clause for a one-leg corner rung IharaTower.iharaClauseAt_cornerRung_one 3 below · cited by 1 · depth 12
• Restricting a perfect self-adjoint pairing to an idempotent corner IharaTower.exists_levelPairing_cornerSubmodule_of_le 0 below · cited by 2 · depth 13
• Perfect self-adjoint pairing restricts to a level pairing on a corner IharaTower.exists_levelPairing_cornerSubmodule_of_stable_of_selfAdjoint 4 below · cited by 2 · depth 13
• Stabilisation of a Hecke corner intertwines α̃ with U_q IharaTower.iDegL_one_unitRoot_sub_iDegL_intertwines_heckeT 0 below · cited by 1 · depth 13
• Trace-side U_q relations on Hecke corners by adjointness IharaTower.jDegL_heckeT_eq_of_adjoint_corner 0 below · cited by 1 · depth 13
• Degeneracy traces intertwine U_q with the unit root IharaTower.jDegL_heckeT_eq_unitRoot_smul_of_ordinary_refinement 1 below · cited by 2 · depth 13
• Res-equivariance of the degeneracy traces on the ordinary corner IharaTower.jDegL_smul_eq_res_smul_jDegL_of_generators_of_ordinary_refinement 3 below · cited by 1 · depth 13
• Saturation and rank force a residually injective map onto eigen-submodules IharaTower.map_torsionBySet_eq_of_forall_eq_smul_of_finrank_le 0 below · cited by 2 · depth 15

IharaTower.CornerData 1

• Stable orthogonal complement of a refinement corner IharaTower.CornerData.exists_orthogonal_stable_complement_of_corner_le_of_selfAdjoint 1 below · cited by 1 · depth 13

IharaTower.RungAssembly 3

• Rung Δ-value from the unit-root quadratic relation IharaTower.RungAssembly.map_delta_of_sq_sub 0 below · cited by 1 · depth 12
• Rung element of a two-leg datum as a quadratic form IharaTower.RungAssembly.deltaComb_two 0 below · cited by 1 · depth 13
• Ihara clause for an assembled rung datum IharaTower.RungAssembly.iharaClauseAt_rungDatumOfLegs 0 below · cited by 1 · depth 13

IharaTower.RungDatum 1

• Restricting a rung datum along an isometric embedding IharaTower.RungDatum.exists_restrict 0 below · cited by 1 · depth 12