← all areas

Namespace M4aHerbrand 148 theorems

— 110 · AdeleBaseChange 3 · Bridge 2 · GenuineDescent 11 · IdeleGaloisDescent 21 · unitIdelesTrivialOn 1

directly in M4aHerbrand 110

• Componentwise splitting of the genuine adelic norm M4aHerbrand.genuineAdelicNorm_componentwise 1 below · cited by 13 · depth 15
• Local norm scales the valuation by the residue degree M4aHerbrand.valuation_norm_adicCompletion_eq_pow_inertiaDeg 0 below · cited by 20 · depth 15
• Local rigidity of adele base-change data M4aHerbrand.adeleBaseChange_local_rigidity 0 below · cited by 7 · depth 16
• Idelic norm of a uniformizer idele M4aHerbrand.exists_idelicNorm_uniformizerIdele_eq_pow_inertiaDeg_mul_localUnit 3 below · cited by 29 · depth 16
• Upper ramification groups lie in the local image of the idelic Artin map M4aHerbrand.exists_isAdjuster_pow_idelicArtinMap_eq_of_mem_upperRamificationGroup 302 below · cited by 1 · depth 16
• Product formula for the idelic Artin map, totally positive case M4aHerbrand.finprod_idelicArtinMap_idelesTrivialOn_eq_one_of_totallyPositive 2 below · cited by 2 · depth 16
• First inequality for idele classes of a cyclic extension M4aHerbrand.ideleClass_normCoset_index_ne_zero_and_finrank_dvd 56 below · cited by 6 · depth 16
• Idelic Artin map at one place: Frobenius modulo inertia M4aHerbrand.idelicArtinMap_single_mul_zpow_inv_mem_inertia_of_isArithFrobAt 137 below · cited by 9 · depth 16
• Ramification theorem: inertia lies in the image of local units M4aHerbrand.inertia_le_map_unitIdelesTrivialOn_compl_singleton_of_idelicArtinMap 252 below · cited by 6 · depth 16
• Congruence units at ramified places are idelic norms M4aHerbrand.unitIdele_mem_idelicNorm_range 2 below · cited by 9 · depth 16
• First inequality for cyclic extensions, with base-change datum M4aHerbrand.exists_adeleBaseChange_normCoset_index_ne_zero_and_finrank_dvd 55 below · cited by 1 · depth 17
• Artin image of level-n units lies in Gⁿ(w∣ v) M4aHerbrand.idelicArtinMap_mem_upperRamificationGroup_of_isAdjuster_pow 283 below · cited by 3 · depth 17
• Kernel of the local component of the idelic Artin map M4aHerbrand.idelicArtinMap_single_eq_one_iff_exists_finprod_smul_eq 258 below · cited by 3 · depth 17
• Level congruence and real positivity descend along the idelic norm M4aHerbrand.idelicNorm_levelCongr_and_realPos 2 below · cited by 1 · depth 17
• Local images under the idelic Artin map: decomposition and inertia M4aHerbrand.map_idelesTrivialOn_eq_decomp_and_map_unitIdelesTrivialOn_eq_inertia_of_isCyclic 250 below · cited by 1 · depth 17
• Compatibility of idelic Artin maps with restriction to a subextension M4aHerbrand.restrictNormalHom_idelicArtinMap_eq 7 below · cited by 4 · depth 17
• Valuation of the adelic norm at a finite place M4aHerbrand.valuation_adelicNorm_eq_finprod_pow_inertiaDeg 2 below · cited by 2 · depth 17
• Single-place idèle generating a decomposition group at a cyclic layer M4aHerbrand.exists_forall_mem_zpowers_idelicArtinMap_single_of_isCyclic 249 below · cited by 1 · depth 18
• Global invariant maps on H² of idèle classes, p odd M4aHerbrand.exists_invariant_groupCohomology_ideleClassGroup_of_isPGroup_of_ne_two 371 below · cited by 1 · depth 18
• Tate cardinalities of the finite S-ideles of a cyclic extension M4aHerbrand.finSIdele_tateCard_eq_localDegreeProd 39 below · cited by 3 · depth 18
• Idelic Artin map sends local norms at v into H' M4aHerbrand.idelicArtinMap_single_mem_map_subtype_of_finprod_smul_eq 139 below · cited by 4 · depth 18
• Tate cardinalities of the archimedean ideles of a cyclic extension M4aHerbrand.infiniteIdele_tateCard_eq_localDegreeProd 20 below · cited by 3 · depth 18
• Local components of the idelic Artin map are reciprocity maps M4aHerbrand.isLocalReciprocityMap_of_idelicArtinMap_single 260 below · cited by 1 · depth 18
• Image of Eᵥ^×: decomposition group, of 𝒪ᵥ^×: inertia group M4aHerbrand.map_idelesTrivialOn_eq_decomp_and_map_unitIdelesTrivialOn_eq_inertia 253 below · cited by 2 · depth 18
• Herbrand quotient of the S-units of a cyclic extension M4aHerbrand.sUnit_tateCard_mul_localDegreeProd 1 below · cited by 3 · depth 18
• Uniqueness of Galois descent data on AdeleRing R F M4aHerbrand.subsingleton_ideleGaloisDescent 0 below · cited by 71 · depth 18
• Positive-degree cohomology of idèle and S-idèle class groups agree M4aHerbrand.bijective_groupCohomology_map_toSIdeleClass 65 below · cited by 3 · depth 19
• Descending the idèle class invariant system one Galois layer M4aHerbrand.exists_adeleBaseChange_invariant_groupCohomology_ideleClassGroup_map_eq_of_invariant 300 below · cited by 2 · depth 19
• Class formation axioms for the T-idèle class group M4aHerbrand.exists_fundamentalClass_sIdeleClassGroup 248 below · cited by 2 · depth 19
• Equivariance of the concentrated-idèle embedding at a finite place M4aHerbrand.exists_hom_adicCompletion_res_decomp_ideles_apply 6 below · cited by 3 · depth 19
• Local w-component maps are D_w-equivariant on idèle units M4aHerbrand.exists_hom_res_decomp_ideles_adicCompletion_apply 4 below · cited by 18 · depth 19
• Existence of an idèle-class frame for a Galois layer M4aHerbrand.exists_ideleGaloisDescent_concentrated_lam_rho 9 below · cited by 1 · depth 19
• Invariant maps at a p-group layer with local value 1/|D_w| M4aHerbrand.exists_invariant_forall_inv_map_localFundamentalClass_eq_one_div_natCard_decomp_of_isPGroup 370 below · cited by 2 · depth 19
• Invariant maps for the idèle class formation, p odd M4aHerbrand.exists_invariant_groupCohomology_ideleClassGroup_forall_comp_eq_index_smul_of_ne_two 384 below · cited by 2 · depth 19
• Finite-level degree-one duality for the S-idèle class group M4aHerbrand.exists_level_forall_relationHom_sIdeleClassGroup_extends_or_map_delta_ne_zero 488 below · cited by 2 · depth 19
• Local–global compatibility of the idelic Artin map at w M4aHerbrand.exists_localCoordinate_carry_eq_zsmul_and_div_natCard_decomp_eq_of_idelicArtinMap 241 below · cited by 2 · depth 19
• Herbrand quotient of the fibre-and-box finite S-idele group M4aHerbrand.finSIdeleFibreBox_tateCard_eq_localDegreeProd 38 below · cited by 1 · depth 19
• Dirichlet's S-unit theorem: the rank of 𝒪_{K,S}^× M4aHerbrand.finrank_sUnit_eq_univ 0 below · cited by 1 · depth 19
• Herbrand quotient of the fibre-grouped archimedean ideles M4aHerbrand.infiniteIdeleFibre_tateCard_eq_localDegreeProd 19 below · cited by 1 · depth 19
• Existence of a Galois descent datum on the adele ring M4aHerbrand.nonempty_ideleGaloisDescent 0 below · cited by 16 · depth 19
• Fixed ranks of S-units, finite places and infinite places M4aHerbrand.sUnitQuot_fixedRank_eq 0 below · cited by 1 · depth 19
• Unit idèles trivial on T meet principal idèles trivially M4aHerbrand.disjoint_unitIdelesTrivialOn_principalIdeles 0 below · cited by 1 · depth 20
• A fundamental class in H²(G, C_F) for the idèle class group M4aHerbrand.exists_fundamentalClass_ideleClassGroup 205 below · cited by 4 · depth 20
• One-step descent of the idèle-class fundamental class, p odd M4aHerbrand.exists_fundamentalClass_ideleClassGroup_map_eq_finrank_smul_of_ne_two 296 below · cited by 1 · depth 20
• Fundamental class of the idèle class group, p-part of local classes M4aHerbrand.exists_fundamentalClass_ideleClassGroup_smul_res_eq_smul_localFundamentalClass_of_ne_two 383 below · cited by 1 · depth 20
• Equivariance of the idèle class quotient map M4aHerbrand.exists_hom_ideles_ideleClassGroup_apply 0 below · cited by 5 · depth 20
• Equivariant idèle base change and Hilbert 90 for idèle classes M4aHerbrand.exists_hom_res_ideles_and_ideleClassGroup_injective_range_eq_invariants_of_isScalarTower 6 below · cited by 5 · depth 20
• Tate's reciprocity law for idèle classes, p-group case M4aHerbrand.exists_invariant_forall_inv_map_eq_finsum_of_forall_localFundamentalClass_of_isPGroup 368 below · cited by 3 · depth 20
• Local Artin map computes carry classes on an enlarged layer M4aHerbrand.exists_mk_localArtin_eq_pow_and_infNatTrans_carryFun_eq_smul_of_enlargedLayer 220 below · cited by 1 · depth 20
• Vanishing of Tate cohomology of the unit idèles outside T M4aHerbrand.subsingleton_tateCohomology_unitIdelesTrivialOn_of_ramificationIdx_eq_one 63 below · cited by 1 · depth 20
• Invariant maps for a p-group layer, assembled from hypotheses M4aHerbrand.exists_invariant_forall_inv_map_eq_finsum_of_forall_localFundamentalClass_of_isPGroup_of_children 312 below · cited by 1 · depth 21
• An S-ramified existence theorem for S-idèle class groups M4aHerbrand.exists_isGalois_forall_prod_sClassAct_eq_pow_of_isPrimitiveRoot 271 below · cited by 1 · depth 21
• H²(Gal(F/E), C_F) is cyclic of order |G| M4aHerbrand.exists_natCard_H2_eq_card_and_span_eq_top_ideleClassGroup 201 below · cited by 2 · depth 21
• Invariant map on H²(G,C_F) for cyclic layers M4aHerbrand.exists_surjective_and_invariant_map_eq_finsum_of_isCyclic 291 below · cited by 1 · depth 21
• A p-adic comparison constant for the local fundamental classes M4aHerbrand.exists_unit_forall_exists_localFundamentalClass_eq_smul_res_and_pow_dvd_of_ne_two 376 below · cited by 1 · depth 21
• Free rank of the S-units of a number field M4aHerbrand.finrank_sUnit_eq 0 below · cited by 5 · depth 21
• Sum of local invariants is unchanged by corestriction M4aHerbrand.finsum_div_natCard_decomp_cores_eq_finsum_div_natCard_inf_decomp 156 below · cited by 2 · depth 21
• Local invariants of a global class sum to zero (p-group layer) M4aHerbrand.finsum_div_natCard_decomp_eq_zero_of_isPGroup 316 below · cited by 1 · depth 21
• Sum of local coordinates in ℚ/ℤ is unchanged by inflation M4aHerbrand.finsum_div_natCard_decomp_map_eq_finsum_div_natCard_decomp_of_isScalarTower 123 below · cited by 2 · depth 21
• Persistence of the p-th-power norm condition on S-idèle classes M4aHerbrand.forall_exists_prod_fixingSubgroup_sClassAct_eq_pow_of_ringHom_of_forall_exists 8 below · cited by 1 · depth 21
• Restriction of an idele Galois descent datum to an intermediate field M4aHerbrand.ideleGaloisDescent_restrict_intermediateField 1 below · cited by 8 · depth 21
• Vanishing of positive-degree cohomology of unit idèles outside T M4aHerbrand.isZero_groupCohomology_unitIdelesTrivialOn_of_ramificationIdx_eq_one 29 below · cited by 1 · depth 21
• Reciprocity for p-primary idèle classes at a finite layer M4aHerbrand.map_pi_eq_zero_iff_finsum_eq_zero_of_pow_smul_eq_zero 376 below · cited by 3 · depth 21
• Local coordinates over F^H of a restricted idèle class M4aHerbrand.map_prG_eq_smul_fixedField_of_map_prG_eq_smul 110 below · cited by 2 · depth 21
• Semilocal degree-two class equals index times a restricting class M4aHerbrand.zsmul_map_eq_zsmul_index_smul_of_zsmul_res_eq_zsmul_map_of_comap_decomp 11 below · cited by 1 · depth 21
• Properties of the invariant map of a cyclic layer M4aHerbrand.card_nsmul_eq_zero_and_map_eq_zero_and_exists_eq_one_div_of_forall_localSum_eq_finsum 265 below · cited by 1 · depth 22
• Local invariants unchanged by inflation, numerical form M4aHerbrand.div_natCard_decomp_eq_div_natCard_decomp_under_of_map_map_eq_zsmul_of_isScalarTower 110 below · cited by 3 · depth 22
• A carry class generating H² of the idèle class group M4aHerbrand.exists_addOrderOf_carry_eq_card_and_span_eq_top_ideleClassGroup_of_isCyclic 160 below · cited by 3 · depth 22
• Archimedean coordinate maps of the idèle units are decomposition-equivariant M4aHerbrand.exists_hom_res_infPlaceDecomp_ideles_localUnits_apply 4 below · cited by 6 · depth 22
• Archimedean coordinate morphisms on idèle units at infinite places M4aHerbrand.exists_hom_res_inf_infPlaceDecomp_ideles_completion_apply 4 below · cited by 2 · depth 22
• Norm group of an exponent-p extension unramified outside S M4aHerbrand.exists_isGalois_principalIdeles_sup_range_idelicNorm_eq_of_isPrimitiveRoot 265 below · cited by 1 · depth 22
• A local-sum invariant on H²(G,I_F) for cyclic extensions M4aHerbrand.exists_localSum_forall_eq_finsum_groupCohomology_ideles 138 below · cited by 1 · depth 22
• Surjectivity of H²(G,I_F)→ H²(G,C_F) for cyclic G M4aHerbrand.exists_map_eq_groupCohomology_ideleClassGroup_of_isCyclic 6 below · cited by 1 · depth 22
• Restriction of an idèlic H² class comes from the intermediate layer M4aHerbrand.exists_map_eq_map_res_ideles 1 below · cited by 1 · depth 22
• Exactness at H²(G,I_F) for a cyclic layer M4aHerbrand.exists_map_eq_of_map_eq_zero_groupCohomology_ideles_of_isCyclic 4 below · cited by 1 · depth 22
• Capturing an inflated idèle class over a second splitting field M4aHerbrand.exists_map_map_eq_map_map_of_dvd_natCard_decomp 240 below · cited by 1 · depth 22
• Transport of local bridge data between places over E M4aHerbrand.exists_map_prG_eq_zsmul_of_map_prG_eq_zsmul_of_under_eq 12 below · cited by 3 · depth 22
• Order and cyclicity of H² of idèle classes, p-group case M4aHerbrand.exists_natCard_H2_eq_card_and_span_eq_top_ideleClassGroup_of_isPGroup 188 below · cited by 2 · depth 22
• Restricting the idèle representation to a subgroup M4aHerbrand.exists_res_ideles_iso_res_mulEquiv_fixedField 2 below · cited by 2 · depth 22
• A generator of H²(P,C_F) with prescribed local restrictions M4aHerbrand.exists_span_eq_top_forall_map_inclusion_localFundamentalClass_eq_map_inclusion_of_isPGroup_of_ne_two 374 below · cited by 1 · depth 22
• A p-adic comparison constant for local fundamental classes M4aHerbrand.exists_unit_forall_exists_localFundamentalClass_eq_smul_res_and_pow_dvd_of_forall_map_inclusion_eq 12 below · cited by 1 · depth 22
• Local readings of a global class sum to zero: cyclic layer M4aHerbrand.finsum_div_natCard_decomp_eq_zero_of_isCyclic 243 below · cited by 2 · depth 22
• Sylow descent for vanishing of a sum of local invariants M4aHerbrand.finsum_sylow_eq_zero_iff_finsum_eq_zero_of_pow_smul_eq_zero 124 below · cited by 1 · depth 22
• Local coordinates on idèle cohomology: injectivity, finiteness, surjectivity M4aHerbrand.injective_and_finite_and_surjective_localCoordinates_groupCohomology_ideles 39 below · cited by 9 · depth 22
• Local coordinates and idèle cohomology at a subgroup H M4aHerbrand.injective_and_finite_and_surjective_localCoordinates_groupCohomology_res_ideles 42 below · cited by 2 · depth 22
• Sylow descent for vanishing in degree-two idèle class cohomology M4aHerbrand.map_pi_eq_zero_iff_map_pi_eq_zero_sylow_of_pow_smul_eq_zero 5 below · cited by 1 · depth 22
• Restriction to the Sylow fixed field preserves the local coordinates M4aHerbrand.map_prG_eq_smul_sylow_of_map_prG_eq_smul 111 below · cited by 1 · depth 22
• Local component commutes with conjugation in cohomology M4aHerbrand.map_prG_map_eq_map_map_prH_of_smul_eq 4 below · cited by 1 · depth 22
• Local coordinate maps at w and hw agree up to conjugation M4aHerbrand.map_prH_eq_map_map_prH_of_smul_eq 5 below · cited by 1 · depth 22
• A Galois-stable unit idèle group forces T to be fibred over E M4aHerbrand.mem_iff_mem_of_under_eq_of_smul_unitIdelesTrivialOn 5 below · cited by 1 · depth 22
• Unit idèles trivial on T as coinduced local units M4aHerbrand.nonempty_unitIdelesTrivialOn_iso_pi_coind_localIntegerUnits 10 below · cited by 1 · depth 22
• Invariant idèle class of exact order [F:E] modulo norms M4aHerbrand.exists_classAct_eq_and_pow_mem_range_ideleClassNorm_iff_of_isCyclic 140 below · cited by 1 · depth 23
• Global fundamental class and its local components, odd p M4aHerbrand.exists_fundamentalClass_ideleClassGroup_res_eq_localFundamentalClass_of_isPGroup_of_ne_two 373 below · cited by 1 · depth 23
• Local coordinate maps at w as H∩ D_w-morphisms M4aHerbrand.exists_hom_res_inf_decomp_ideles_adicCompletion_apply 4 below · cited by 1 · depth 23
• Inflation commutes with taking the W-component of idèles M4aHerbrand.map_decomp_map_ideles_eq_map_map_decomp_under_of_isScalarTower 0 below · cited by 2 · depth 23
• Vanishing of archimedean coordinates of inflated idele classes in H² M4aHerbrand.map_inclusion_map_subtype_map_ideles_eq_zero_infinitePlace_of_forall_eq_one 0 below · cited by 1 · depth 23
• Vanishing of local components of an inflated idèle class M4aHerbrand.map_inclusion_map_subtype_map_ideles_eq_zero_of_dvd_natCard_decomp 111 below · cited by 1 · depth 23
• Local coordinates in cohomology at conjugate places agree M4aHerbrand.map_prG_eq_map_map_prG_of_smul_eq 5 below · cited by 5 · depth 23
• Injectivity of H²(K^×)→ H²(I_K) for p-group layers M4aHerbrand.map_two_res_units_ideles_injective_of_isPGroup 121 below · cited by 1 · depth 23
• Triviality of the Artin map product on single-place idèles M4aHerbrand.prod_idelicArtinMap_single_eq_one 3 below · cited by 1 · depth 23
• Fundamental class in H² of the idèle class group for p-extensions M4aHerbrand.exists_fundamentalClass_ideleClassGroup_of_isPGroup 192 below · cited by 1 · depth 24
• First inequality: [F:E] divides #̂ H⁰(C_F) M4aHerbrand.ideleClassGroup_tateCard_zero_ne_zero_and_finrank_dvd 55 below · cited by 1 · depth 24
• First inequality: Herbrand quotient of the idele class group M4aHerbrand.ideleClass_herbrandQuotient_eq_finrank 55 below · cited by 3 · depth 24
• Compatibility of local W-coordinate maps under restriction M4aHerbrand.map_inclusion_map_subtype_eq_map_inclusion_map_decomp 0 below · cited by 1 · depth 24
• Archimedean local components of p-primary degree-2 classes vanish M4aHerbrand.map_prInf_eq_zero_of_pow_smul_eq_zero 3 below · cited by 1 · depth 24
• Tate ̂ H⁰, ̂ H⁻¹ of a cyclic group on idèle classes M4aHerbrand.nonempty_tate_addEquiv_ideleClass 1 below · cited by 3 · depth 24
• Idelic norm-coset index equals the idele class Tate number M4aHerbrand.idelicNormCoset_index_eq_ideleClassTateCard 0 below · cited by 2 · depth 25
• Vanishing at chosen places kills idèle cohomology classes M4aHerbrand.eq_zero_of_forall_localCoordinates_above_eq_zero_groupCohomology_ideles 43 below · cited by 1 · depth 26
• A concentrated idèle 2-cocycle above one place M4aHerbrand.exists_two_cocycle_ideles_mem_unitIdelesOutside_and_map_prG_eq_zsmul_and_eq_zero 20 below · cited by 1 · depth 27
• Coinduced local units map into the idèles, with coordinate pins M4aHerbrand.exists_hom_coind_ideles_finPart_eq_and_eq_one 18 below · cited by 1 · depth 28

M4aHerbrand.AdeleBaseChange 3

• Idèle boxes lie in the image of the idelic norm M4aHerbrand.AdeleBaseChange.ideleBox_le_range_idelicNorm 7 below · cited by 5 · depth 18
• Local criterion for membership in the idelic norm group M4aHerbrand.AdeleBaseChange.mem_range_idelicNorm_of_forall_exists_norm_eq 2 below · cited by 5 · depth 19
• Openness of the idelic norm group of a Galois extension M4aHerbrand.AdeleBaseChange.isOpen_range_idelicNorm 12 below · cited by 1 · depth 25

M4aHerbrand.Bridge 2

• Transitivity of adèle base change in a tower M4aHerbrand.Bridge.genuineBeta_comp_of_tower 2 below · cited by 4 · depth 20
• Finite conorm raises valuations to e(w∣ v); contents correspond M4aHerbrand.Bridge.valued_finiteConorm_apply_and_finprod_pow_eq 0 below · cited by 4 · depth 20

M4aHerbrand.GenuineDescent 11

• Adelic norm of a principal adele is the field norm M4aHerbrand.GenuineDescent.adelicNorm_genuineBaseChange_algebraMap 0 below · cited by 31 · depth 16
• Continuity of the adelic norm A_M → A_K M4aHerbrand.GenuineDescent.continuous_adelicNorm_genuineBaseChange 0 below · cited by 33 · depth 16
• Infinite coordinates of the genuine Galois descent action M4aHerbrand.GenuineDescent.genuineDescentDatum_act_fst_apply 1 below · cited by 33 · depth 18
• Finite coordinates of the genuine Galois descent action M4aHerbrand.GenuineDescent.genuineDescentDatum_act_snd_apply 2 below · cited by 38 · depth 18
• Idelic norm of an archimedean unit idele at a real place M4aHerbrand.GenuineDescent.idelicNorm_genuineBaseChange_archCentralUnit_of_isReal 2 below · cited by 1 · depth 19
• Finiteness of idele class characters with prescribed composite with the norm M4aHerbrand.GenuineDescent.finite_setOf_monoidHom_comp_idelicNorm_genuineBaseChange_eq_of_prime 105 below · cited by 1 · depth 20
• Galois descent, Hilbert 90 and norm for idèles M4aHerbrand.GenuineDescent.injective_beta_and_fixed_iff_and_h90_and_prod_unitsAct_eq_idelicNorm 1 below · cited by 25 · depth 21
• Base change of idèles reflects principality M4aHerbrand.GenuineDescent.unitsMap_beta_mem_principalIdeles_iff 2 below · cited by 4 · depth 21
• Genuine adèlic base change preserves unit idèles trivial above S M4aHerbrand.GenuineDescent.map_beta_unitIdelesTrivialOn_placesOverPrimes_le 0 below · cited by 2 · depth 22
• Descent of an invariant idele character along a cyclic extension M4aHerbrand.GenuineDescent.exists_ideleChar_comp_idelicNorm_eq_of_unitsAct_invariant 208 below · cited by 4 · depth 26
• Adelic base change is a closed embedding on ideles M4aHerbrand.GenuineDescent.isClosedEmbedding_unitsMap_genuineBaseChange 0 below · cited by 6 · depth 30

M4aHerbrand.IdeleGaloisDescent 21

• Descent data stabilise the unit idèles outside primes above S M4aHerbrand.IdeleGaloisDescent.stabilizesUnitIdeles_placesOverPrimes 6 below · cited by 3 · depth 19
• Galois descent datum yields a multiplicative action on idèle classes M4aHerbrand.IdeleGaloisDescent.exists_mulDistribMulAction_smul_eq_classAct 0 below · cited by 13 · depth 20
• Genuine idèle base change is Galois-equivariant in a tower M4aHerbrand.IdeleGaloisDescent.unitsAct_map_genuineBaseChange 4 below · cited by 6 · depth 22
• Closedness of the cyclic norm image in the idele group M4aHerbrand.IdeleGaloisDescent.isClosed_range_prod_unitsAct_pow 8 below · cited by 1 · depth 27
• Hilbert's Theorem 90 for ideles: cyclic norm one gives a coboundary M4aHerbrand.IdeleGaloisDescent.exists_eq_inv_mul_unitsAct_of_prod_unitsAct_pow_eq_one 40 below · cited by 5 · depth 28
• Properness of the twisted coboundary map on ideles M4aHerbrand.IdeleGaloisDescent.exists_isCompact_forall_exists_unitsAct_eq_and_eq_mul_of_unitsAct_mul_inv_mem 42 below · cited by 2 · depth 28
• Adeles fixed by σ form the adele ring of the fixed field M4aHerbrand.IdeleGaloisDescent.exists_ringEquiv_adeleRing_eqLocus_act 1 below · cited by 1 · depth 28
• Galois invariance on norm-one ideles extends to all ideles M4aHerbrand.IdeleGaloisDescent.apply_unitsAct_eq_of_forall_mem_normOneIdeles 1 below · cited by 3 · depth 29
• Bijectivity of s ↦ σ(s) - cs on adeles M4aHerbrand.IdeleGaloisDescent.bijective_act_sub_algebraMap_mul_of_norm_ne_one 0 below · cited by 3 · depth 29
• Unramified characters identify conjugate uniformiser ideles M4aHerbrand.IdeleGaloisDescent.apply_unitsAct_det_heckeGen_eq_apply_det_heckeGen_of_asIdeal_eq_smul_of_isUnramifiedCharAt 6 below · cited by 1 · depth 30
• Haar transport along z ↦ σ(z)z⁻¹ for norm-one ideles M4aHerbrand.IdeleGaloisDescent.exists_pos_forall_integral_ker_idelicNorm_eq_mul_integral_haarQuotient_unitsAct_mul_inv 49 below · cited by 3 · depth 30
• Galois invariance of the idele norm M4aHerbrand.IdeleGaloisDescent.ideleNorm_unitsAct 0 below · cited by 2 · depth 30
• Galois descent on A_L^× fixes base-changed ideles M4aHerbrand.IdeleGaloisDescent.unitsAct_idelesBaseChange 1 below · cited by 1 · depth 30
• Measure-preserving twisted difference operator s ↦ σ(s) - cs on adeles M4aHerbrand.IdeleGaloisDescent.exists_continuousAddEquiv_measurePreserving_act_sub_algebraMap_mul_of_norm_ne_one 2 below · cited by 2 · depth 31
• Galois swap of unitary idele characters up to ‖·‖^{iτ} M4aHerbrand.IdeleGaloisDescent.exists_forall_apply_unitsAct_eq_mul_normPowChar_of_forall_mem_normOneIdeles_eq_swap 48 below · cited by 1 · depth 31
• Haar measure on A_L is invariant under a descent datum M4aHerbrand.IdeleGaloisDescent.measurePreserving_act_adelicAddHaar 0 below · cited by 1 · depth 31
• Galois action on adeles splits into archimedean and finite parts M4aHerbrand.IdeleGaloisDescent.exists_ringEquiv_prod_forall_act_eq 1 below · cited by 2 · depth 33
• Galois action on adeles splits into continuous archimedean and finite parts M4aHerbrand.IdeleGaloisDescent.exists_ringEquiv_prod_forall_act_eq_ed2 2 below · cited by 1 · depth 33
• Cyclic invariance kills ξ on norm-one ideles M4aHerbrand.IdeleGaloisDescent.apply_eq_one_of_idelicNorm_eq_one_of_forall_apply_unitsAct_eq 42 below · cited by 1 · depth 34
• Galois descent on adeles permutes components isometrically M4aHerbrand.IdeleGaloisDescent.exists_norm_act_apply_eq_norm_apply 6 below · cited by 2 · depth 34
• Galois action on ideles preserves Haar measure M4aHerbrand.IdeleGaloisDescent.measurePreserving_unitsAct 0 below · cited by 1 · depth 34

M4aHerbrand.unitIdelesTrivialOn 1

• Unit idèles U_F^T as an H-module via the fixed field M4aHerbrand.unitIdelesTrivialOn.nonempty_res_iso_fixedField_and_groupCohomology_iso 2 below · cited by 1 · depth 21