← all areas

Namespace IntermediateField 60 theorems

— 58 · IsUnramifiedOutside 2

directly in IntermediateField 58

• Degree bound for a K-endomorphism of a quadratic extension IntermediateField.finrank_fieldRange_le_of_adjoin_pair_eq_top 0 below · cited by 1 · depth 10
• Norms on K(μ_{q^N-1}) are already attained on K IntermediateField.exists_norm_eq_adjoin_rootsOfUnity_padic 17 below · cited by 7 · depth 14
• Finiteness and normality of K(μ_{q^N-1}) over a p-adic field IntermediateField.finiteDimensional_normal_adjoin_rootsOfUnity_padic 0 below · cited by 9 · depth 14
• Degree of K(μ_{q^N-1})/K as order of #κ IntermediateField.finrank_adjoin_rootsOfUnity_padic_eq_orderOf 15 below · cited by 8 · depth 14
• Frobenius automorphism of K(μ_{q^N-1})/K over a q-adic field IntermediateField.exists_frobenius_adjoin_rootsOfUnity_padic 10 below · cited by 3 · depth 15
• Finiteness of K^×/(K^×)ⁿ for K/ℚ_q finite IntermediateField.finite_units_quotient_range_powMonoidHom_padic 13 below · cited by 1 · depth 15
• Degree bound for the reduction of a finite extension of 𝔽(x) IntermediateField.finrank_adjoin_range_le_finrank_of_transcendental 0 below · cited by 1 · depth 15
• Degree of F(μ_m) equals number of conjugates of ζ₀ IntermediateField.finrank_adjoin_rootsOfUnity_eq_card_rootSet 0 below · cited by 1 · depth 15
• Domain criterion for k⊗_𝔽κ from a degree count IntermediateField.isDomain_tensorProduct_of_finrank_le_finrank_adjoin_range 0 below · cited by 1 · depth 15
• Power map on μ_m extends to an F-automorphism IntermediateField.exists_algEquiv_adjoin_rootsOfUnity_apply_eq_pow 0 below · cited by 2 · depth 16
• Cyclic Frobenius generator of K(μ_{q^N-1})/K over ℚ_q IntermediateField.exists_generator_frobenius_adjoin_rootsOfUnity_padic 16 below · cited by 6 · depth 16
• Finite extensions of ℚ_q come from number fields IntermediateField.exists_le_adjoin_padicEmbedding_image 1 below · cited by 5 · depth 16
• Finiteness of ℚ_q generated by a finite subfield of ℚ̄ IntermediateField.finiteDimensional_adjoin_padicEmbedding_image 0 below · cited by 6 · depth 16
• Inertia at q ∤ d_F fixes F pointwise IntermediateField.inertiaSubgroupIn_le_fixingSubgroup_of_not_dvd_discr 0 below · cited by 1 · depth 16
• Trivial inertia above q implies q ∤ d_F IntermediateField.not_dvd_discr_of_inertiaSubgroupIn_le_fixingSubgroup 3 below · cited by 3 · depth 16
• Cyclotomic field ℚ(ζ_p^{k+1}) is unramified outside S ni p IntermediateField.adjoin_isUnramifiedOutside_of_isPrimitiveRoot_pow 1 below · cited by 8 · depth 17
• Simple transcendental extension is the rational function field IntermediateField.exists_algEquiv_adjoin_simple_ratFunc_of_transcendental 0 below · cited by 11 · depth 17
• Units of K are norms from K(μ_{q^N-1}) IntermediateField.exists_norm_eq_of_nnnorm_eq_one_adjoin_rootsOfUnity_padic 46 below · cited by 2 · depth 17
• Enlarging an extension unramified outside S to a normal one IntermediateField.exists_normal_isUnramifiedOutside_of_le 3 below · cited by 25 · depth 17
• An unramified étale ℤₚ-level for a finite unramified K IntermediateField.exists_etale_padicInt_integers_of_inertia_le_fixingSubgroup 2 below · cited by 1 · depth 18
• Cofinality of finite levels over K above a finite level over ℚ IntermediateField.exists_finiteDimensional_fixingSubgroup_le_localGaloisToGlobal_fixingSubgroupEquiv_symm 2 below · cited by 5 · depth 18
• Global level subgroups are cofinal over a finite q-adic level IntermediateField.exists_finiteDimensional_localGaloisToGlobal_fixingSubgroupEquiv_symm_le 5 below · cited by 6 · depth 18
• A transcendental element lies outside K(yⁿ) for n ≥ 2 IntermediateField.not_mem_adjoin_pow_of_transcendental 0 below · cited by 1 · depth 18
• Derivations stable on F are stable on F(α), α separable IntermediateField.apply_mem_adjoin_simple_of_leibniz_of_isSeparable 0 below · cited by 1 · depth 19
• Every degree is realised by a μ_{q^N-1} extension of a local field IntermediateField.exists_finrank_adjoin_rootsOfUnity_padic_eq 17 below · cited by 4 · depth 19
• Transport of finite stabilisers along r under cofinality IntermediateField.exists_forall_mem_fixingSubgroup_smul_eq_of_cofinal 2 below · cited by 1 · depth 19
• Degree of L over K(p(s)) for s transcendental generating L IntermediateField.finrank_adjoin_aeval_of_transcendental 0 below · cited by 1 · depth 19
• Units of an algebraic extension are fixed by a finite-level subgroup IntermediateField.exists_finiteDimensional_forall_mem_fixingSubgroup_smul_eq 1 below · cited by 2 · depth 20
• Existence of non-norms in a cyclic p-adic extension IntermediateField.exists_forall_norm_ne_of_isCyclic_padic 37 below · cited by 1 · depth 20
• Galois S-level Fsupseteq L' with p-th power norm relation IntermediateField.exists_le_isGalois_dvd_finrank_forall_prod_fixingSubgroup_sClassAct_eq_pow 284 below · cited by 1 · depth 20
• Solvability of Galois groups of finite extensions of ℚ_q IntermediateField.isSolvable_algEquiv_of_padic 12 below · cited by 14 · depth 20
• Galois closure of an S-unramified level is S-unramified IntermediateField.isUnramifiedOutside_normalClosure 3 below · cited by 6 · depth 20
• Adjoining a p-th root of an S-unit, p ∈ S IntermediateField.isUnramifiedOutside_sup_adjoin_of_pow_eq 0 below · cited by 8 · depth 20
• Monotonicity of K(μ_{q^N-1}) along divisibility IntermediateField.adjoin_rootsOfUnity_padic_mono 0 below · cited by 1 · depth 21
• Every element of an algebraic extension has an open stabiliser IntermediateField.exists_finiteDimensional_forall_mem_fixingSubgroup_apply_eq 0 below · cited by 1 · depth 21
• Embedding an abstract S-unramified Galois extension into a Galois S-level IntermediateField.exists_le_isGalois_ringHom_dvd_finrank_of_ramificationIdx_eq_one 8 below · cited by 1 · depth 21
• Existence of a uniformiser in a finite extension of ℚ_q IntermediateField.exists_uniformiser_padic 3 below · cited by 6 · depth 21
• Norms scale the q-adic absolute value by the degree IntermediateField.norm_algebraNorm_eq_pow_finrank_padic 0 below · cited by 2 · depth 21
• Ring isomorphisms of finite extensions of ℚ_q are ℚ_q-linear isometries IntermediateField.apply_algebraMap_eq_and_norm_apply_eq_of_ringEquiv_of_padic 0 below · cited by 1 · depth 22
• Above any S-level lies an S-level of relative degree divisible by p IntermediateField.exists_le_isUnramifiedOutside_dvd_finrank 2 below · cited by 1 · depth 22
• Galois correspondence H ≅ Gal(F/F^H), pinned on values IntermediateField.exists_mulEquiv_fixedField_apply_eq 0 below · cited by 1 · depth 22
• Ramification index one over an unramified base gives unramified outside S IntermediateField.isUnramifiedOutside_of_forall_ramificationIdx_eq_one 0 below · cited by 1 · depth 22
• Cofinality conditions for a level map restrict to a finite subextension IntermediateField.cofinal_comp_fixingSubgroupEquiv_symm 0 below · cited by 1 · depth 23
• Extending a multiplicative, K-linearly coherent map on a generating monoid IntermediateField.exists_algHom_adjoin_apply_eq_of_isAlgebraic_of_transcendental 0 below · cited by 1 · depth 23
• Extending x ↦ c to L(x,y) → A along a root IntermediateField.exists_algHom_adjoin_pair_of_transcendental_of_minpoly_eq_map 0 below · cited by 1 · depth 23
• Monic relation of full degree is the minimal polynomial IntermediateField.minpoly_adjoin_simple_eq_map_of_natDegree_le_finrank 0 below · cited by 1 · depth 23
• Finite layers lie in finite τ-stable layers IntermediateField.exists_finiteDimensional_le_forall_mem_of_algEquiv 0 below · cited by 3 · depth 24
• Form descent for one-variable function fields IntermediateField.finiteDimensional_adjoin_and_isSeparable_of_form_of_isAlgebraic_of_isCurveOver 5 below · cited by 1 · depth 26
• Linear disjointness descends finiteness over K₀(x) IntermediateField.finiteDimensional_adjoin_of_linearDisjoint_of_transcendental 0 below · cited by 5 · depth 26
• Adjoining a finite Galois-stable separable set gives a finite Galois extension IntermediateField.finiteDimensional_and_isGalois_adjoin_of_forall_algEquiv_apply_mem 0 below · cited by 1 · depth 26
• Subfields of κ((q)) remain integral after constant field extension IntermediateField.isDomain_tensorProduct_of_le_laurentSeries 0 below · cited by 2 · depth 26
• Gal(E/F) as a faithful finite action on E with fixed field F IntermediateField.exists_mulSemiringAction_faithful_smul_eq_iff_coe_mem_of_isGalois_extendScalars 0 below · cited by 2 · depth 27
• Elements of ℚ(ζ_N) fixed by s≡ 1 mod p lie in ℚ(ζₚ) IntermediateField.coe_mem_adjoin_exp_of_forall_ringHom_apply_eq 0 below · cited by 1 · depth 28
• Complex embedding sending a primitive q-th root of unity to e^{2π i/q} IntermediateField.exists_ringHom_complex_apply_eq_exp_of_isPrimitiveRoot 0 below · cited by 2 · depth 28
• Simple radical extensions with n invertible are finite separable of degree ≤ n IntermediateField.finiteDimensional_and_finrank_le_and_isSeparable_of_pow_eq_of_adjoin_simple_eq_top 0 below · cited by 1 · depth 30
• Uniformly bounded finite subextensions give [F(S):F]≤ n IntermediateField.finiteDimensional_adjoin_and_finrank_le_of_forall_finset 0 below · cited by 1 · depth 31
• Linear disjointness of k and κ((q)) over κ IntermediateField.injective_of_apply_tmul_eq_coeffMap_of_le_laurentSeries 0 below · cited by 3 · depth 31
• Field-theoretic Bertini lemma for a generic linear form IntermediateField.mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent 0 below · cited by 1 · depth 31

IntermediateField.IsUnramifiedOutside 2

• Normal closure preserves being unramified outside S IntermediateField.IsUnramifiedOutside.normalClosure 2 below · cited by 25 · depth 18
• Adjoining a p-th root of an S-unit keeps unramifiedness outside S IntermediateField.IsUnramifiedOutside.sup_adjoin_simple_of_pow_mem 0 below · cited by 5 · depth 21