← all areas

Namespace Submodule 62 theorems

— 61 · Quotient 1

directly in Submodule 61

• No cofixed line from ramified inertia and a branch swap Submodule.not_exists_cofixed_line_of_inertia_and_branch_swap 0 below · cited by 1 · depth 7
• Proper submodule of an 𝔽ₚ-module of order p² is a line Submodule.eq_span_singleton_of_card_eq_sq 0 below · cited by 3 · depth 9
• Stable line in an mathbb Fₚ-plane: fixed or cofixed Submodule.stableLine_fixed_or_cofixed_of_absorbing 0 below · cited by 1 · depth 9
• Torsion of a quotient by a lattice: #(V/L)[n]=n^{rk L} Submodule.natCard_torsionBy_quotient_eq_pow_finrank 0 below · cited by 9 · depth 11
• Linear growth of I^m-torsion when q-torsion is finite Submodule.natCard_torsionBySet_pow_linear_of_finite_torsionBy 3 below · cited by 3 · depth 12
• Choosing dim D indices cutting out 0 in D Submodule.exists_finset_card_eq_finrank_forall_eq_zero_of_forall_exists_apply_ne_zero 0 below · cited by 1 · depth 13
• Linear growth of #(X/I^mX) in powers of q Submodule.natCard_quotient_pow_smul_top_linear_of_finite_quotient 0 below · cited by 2 · depth 13
• Finite a-torsion implies finite a^k-torsion Submodule.finite_torsionBy_pow_of_finite_torsionBy 0 below · cited by 2 · depth 14
• Finite subsets of a directed family of submodules Submodule.exists_mem_forall_of_finset_of_directed 4 below · cited by 1 · depth 15
• Saturation of I· M in a free module Submodule.mem_ideal_smul_top_of_smul_mem_of_free_of_noZeroSMulDivisors_quotient 0 below · cited by 1 · depth 15
• Finite adelic elements are determined by their local components Submodule.eq_of_forall_finiteAdeleEvalAt_eq 0 below · cited by 31 · depth 16
• Every finite adelic element has an integer multiple in widehatΛ Submodule.exists_ne_zero_natCast_smul_mem_finiteAdeleBox 1 below · cited by 7 · depth 16
• A ring element projecting a finite module onto stabilised I^N-torsion Submodule.exists_smul_eq_self_and_smul_mem_torsionBySet_of_torsionBySet_pow_succ_eq 0 below · cited by 3 · depth 16
• Finite idèle of D with prescribed local unit components Submodule.exists_units_finiteAdeleEvalAt_eq 2 below · cited by 48 · depth 16
• Dimension of a preimage subspace: rank–nullity for `comap` Submodule.finrank_comap_eq_finrank_ker_add_finrank_range_inf 0 below · cited by 1 · depth 16
• Dimension of a product of subspaces Submodule.finrank_pi_univ_eq_sum 0 below · cited by 1 · depth 16
• Localisation of a lattice intersection at a finite place Submodule.localBox_inf 1 below · cited by 74 · depth 16
• Adelic box of a lattice is cut out place by place Submodule.mem_finiteAdeleBox_iff_forall_finiteAdeleEvalAt_mem_localBox 0 below · cited by 104 · depth 16
• Local box of an adelically conjugated lattice Submodule.mem_localBox_conjByFiniteIdele_iff 3 below · cited by 62 · depth 16
• Eigenvalues on a lattice-preserving family are integral Submodule.moduleFinite_adjoin_eigenvalues_of_map_le_of_span_eq_top 0 below · cited by 1 · depth 16
• Left D^×-equivariance of the idelic lattice dictionary Submodule.ofFiniteIdele_diagonal_mul 0 below · cited by 21 · depth 16
• Injectivity of the idelic lattice dictionary Submodule.ofFiniteIdele_eq_ofFiniteIdele_iff 0 below · cited by 23 · depth 16
• A full ℤ-lattice is cut out by its adelic box Submodule.ofFiniteIdele_one 0 below · cited by 55 · depth 16
• Index of lattices is the product of local indices Submodule.relIndex_toAddSubgroup_eq_finprod_relIndex_localBox 4 below · cited by 19 · depth 16
• Invariance of Λ^β under right multiplication by widehatΛ^× Submodule.conjByFiniteIdele_mul_eq_of_mem_finiteIdeleStabilizer 0 below · cited by 16 · depth 17
• A ℤ-submodule of a ℚ-vector space is determined by its localisations Submodule.eq_of_forall_prime_span_ratLocalizedAt_eq 2 below · cited by 2 · depth 17
• Local components patch to an element of DotimesA_ℚ^f Submodule.exists_forall_finiteAdeleEvalAt_eq 0 below · cited by 26 · depth 17
• Base change k⊗_{A/𝔪}J[𝔪] as ι-eigenspace in k⊗_ℤJ[I] Submodule.exists_injective_linearMap_baseChange_torsionBySet_range_eq_eigenspace 0 below · cited by 1 · depth 17
• p-adic approximation: Λᵥ=(Λ⊗ 1)+p^kΛᵥ Submodule.exists_mem_add_one_tmul_pow_mul_of_mem_localBox 1 below · cited by 10 · depth 17
• Prescribing a unit of D⊗mathbb A_f at one place Submodule.exists_units_finiteAdeleEvalAt_eq_of_forall_ne 2 below · cited by 15 · depth 17
• Adelic box of a conjugated lattice equals gwidehatΛ g⁻¹ Submodule.finiteAdeleBox_conjByFiniteIdele 0 below · cited by 34 · depth 17
• Coordinates for the local box of a ℤ-basis lattice Submodule.mem_localBox_iff_exists_eq_sum_basis_tmul 0 below · cited by 13 · depth 17
• Membership in a ℤ-submodule from prime-by-prime multipliers Submodule.mem_of_forall_prime_exists_smul_mem 0 below · cited by 2 · depth 17
• Membership in the ℤ_{(ℓ)}-span: denominators prime to ℓ Submodule.mem_span_ratLocalizedAt_iff 0 below · cited by 2 · depth 17
• Translating a full lattice by a finite idele Submodule.fg_and_span_eq_top_ofFiniteIdele 0 below · cited by 5 · depth 18
• Adelic box of D∩ gwidehatΛ equals gwidehatΛ Submodule.finiteAdeleBox_ofFiniteIdele 0 below · cited by 19 · depth 18
• Diagonal left translation conjugates the associated order Submodule.mem_conjByFiniteIdele_diagonal_mul_iff 0 below · cited by 5 · depth 18
• Local components of the lattice cut out by a finite idele Submodule.mem_localBox_ofFiniteIdele_iff 3 below · cited by 8 · depth 18
• Fixed vectors of a semilinear Galois action span Submodule.span_fixedPoints_semilinear_eq_top 0 below · cited by 2 · depth 18
• A generator of E modulo rP over A Submodule.exists_generator_of_perfectPairing_antisymm_of_quotient_dual_of_finrank_eq_two_mul 0 below · cited by 1 · depth 19
• Local components of a finite adele lie in the lattice almost everywhere Submodule.eventually_finiteAdeleEvalAt_mem_localBox 0 below · cited by 5 · depth 20
• Subspaces fixed pointwise by a compact operator are finite-dimensional Submodule.finiteDimensional_of_isCompactOperator_of_forall_apply_eq 0 below · cited by 1 · depth 20
• A perfect pairing from orthogonal saturated sublattices of ℤ^ι Submodule.exists_isPerfPair_dotProduct_of_saturated 0 below · cited by 1 · depth 21
• Isotropic submodules of a free rank-two module are cyclic Submodule.exists_eq_span_singleton_of_forall_bilin_eq_zero_of_isReduced 0 below · cited by 1 · depth 23
• Submodules of finite ℤₚ-modules are p-adically closed Submodule.mem_of_forall_exists_sub_mem_pow_smul_top 1 below · cited by 1 · depth 24
• Submodules of free modules over a principal ideal domain are free Submodule.free_of_free_of_isPrincipalIdealRing 0 below · cited by 1 · depth 25
• Submodules of finite modules are I-adically closed Submodule.iInf_sup_pow_smul_top_eq_of_le_jacobson 0 below · cited by 1 · depth 25
• Fixed vectors of an injective q-semilinear endomorphism span Submodule.span_fixedPoints_eq_top_of_frobenius_semilinear_injective 0 below · cited by 3 · depth 26
• Conjugation by a finite idèle preserves intersections and inclusions Submodule.conjByFiniteIdele_inf_and_conjByFiniteIdele_mono 6 below · cited by 1 · depth 28
• Dividing by the diagonal trivialises the component at w Submodule.finiteAdeleEvalAt_finiteIdeleDiagonal_inv_mul_eq_one 0 below · cited by 1 · depth 28
• Conjugate orders agree up to r-power denominators, elementwise Submodule.forall_exists_pow_smul_conj_mem_of_conjByFiniteIdele_finiteIdeleDiagonal_mul_eq_of_mem_asIdeal 6 below · cited by 1 · depth 28
• Divisibility by a prime element descends from a localisation Submodule.mem_smul_top_of_isLocalizedModule_primeCompl_of_isPrime_span_singleton 0 below · cited by 1 · depth 29
• Base change of subspaces over a field commutes with intersection Submodule.baseChange_inf 0 below · cited by 1 · depth 30
• Two full ℤ-lattices have equal local boxes almost everywhere Submodule.exists_finset_forall_not_mem_localBox_eq 1 below · cited by 3 · depth 30
• Gluing local conjugators to a finite idele conjugating lattices Submodule.exists_units_forall_finiteAdeleEvalAt_eq_conjByFiniteIdele_eq 4 below · cited by 2 · depth 30
• Gluing local submodules with invertible quotients Submodule.exists_invertible_quotient_and_forall_localized_eq 2 below · cited by 1 · depth 32
• Elementary words over Dᵥ rewritten over Λ[1/p] times a unit Submodule.exists_list_prod_elementary_tmul_one_mul_eq_of_mem_asIdeal 0 below · cited by 1 · depth 33
• Bounded orthonormal families force dim V ≤ D Submodule.finiteDimensional_and_finrank_le_of_forall_orthonormal_card_le_of_definite 0 below · cited by 1 · depth 33
• Nakayama's lemma over an I-adically complete ring Submodule.eq_top_of_isAdicComplete_of_fg_of_sup_smul_eq_top 0 below · cited by 1 · depth 35
• Base change preserves dimensions of complementary lattices in S² Submodule.finrank_baseChange_eq_finrank_of_isCompl_of_eq_span_image 0 below · cited by 1 · depth 37
• Index of a full-rank submodule equals the determinant ideal's index Submodule.natCard_quotient_eq_natCard_quotient_span_det 0 below · cited by 1 · depth 37

Submodule.Quotient 1

• Local torsion above I forces torsion in J/γ J Submodule.Quotient.isOfFinAddOrder_of_forall_isMaximal_of_subalgebra_fg 0 below · cited by 1 · depth 10