Documentation

TauCeti.FieldTheory.GaloisCohomology.Inflation

The units along a tower of Galois extensions #

Let K ⊆ L ⊆ M be a tower of fields with L/K normal. Restriction Gal(M/K) → Gal(L/K) and the inclusion Lˣ → Mˣ are compatible: σ(ι(a)) = ι(σ|_L(a)) for σ ∈ Gal(M/K) and a ∈ Lˣ. This file records the inclusion as a morphism unitsInflationHom K L M from the restriction of the Gal(L/K)-representation Lˣ to the Gal(M/K)-representation Mˣ. Through groupCohomology.map (AlgEquiv.restrictNormalHom L) it induces the inflation maps

Hⁿ(Gal(L/K), Lˣ) → Hⁿ(Gal(M/K), Mˣ),

in particular the inflation of relative Brauer groups H²(Gal(L/K), Lˣ) → H²(Gal(M/K), Mˣ) along which local invariants are compared.

More generally, for K ⊆ K' and L ⊆ M' with M' a K'-algebra, every σ ∈ Gal(M'/K') is K-linear and restricts to L. The inclusion Lˣ → M'ˣ is then a morphism unitsBaseChangeHom K L K' M' from the restriction of Lˣ along Gal(M'/K') → Gal(L/K) to M'ˣ. Together with that homomorphism it induces the base change map Hⁿ(Gal(L/K), Lˣ) → Hⁿ(Gal(M'/K'), M'ˣ).

For K' = L and M' = M the base change map is restriction Hⁿ(Gal(M/K), Mˣ) → Hⁿ(Gal(M/L), Mˣ), and inflation from Gal(E/K) followed by restriction to Gal(M/L) is base change from E/K to M/L (map_unitsInflationHom_comp_map_unitsBaseChangeHom). In degree two, for M/K finite Galois, inflation and restriction form the exact sequence

0 → H²(Gal(L/K), Lˣ) → H²(Gal(M/K), Mˣ) → H²(Gal(M/L), Mˣ)

(map_unitsInflationHom_two_injective, mem_range_map_unitsInflationHom_two_iff): this is the inflation-restriction sequence of Gal(M/L) → Gal(M/K) → Gal(L/K), whose hypothesis H¹(Gal(M/L), Mˣ) = 0 is Hilbert's Theorem 90, and whose quotient term is identified with H²(Gal(L/K), Lˣ) because the units of M fixed by Gal(M/L) are the units of L. In the language of relative Brauer groups, Br(M/K) ∩ ker(res_{M/L}) = Br(L/K).

Main definitions #

Main results #

References #

source
theorem TauCeti.exists_unitsMap_eq_of_forall_apply_eq {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [IsGalois F E] {x : Eˣ} (hx : ∀ (σ : Gal(E/F)), σ ↑x = ↑x) :
∃ (a : Fˣ), (Units.map ↑(algebraMap F E)) a = x

A Galois-fixed unit comes from the base field: a unit of a Galois extension E/F, not necessarily finite, that is fixed by Gal(E/F) is the image of a unit of F.

source
noncomputable def TauCeti.unitsInflationHom (K L M : Type u) [Field K] [Field L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [Normal K L] :
Rep.res (AlgEquiv.restrictNormalHom L) (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) ⟶ Rep.ofMulDistribMulAction Gal(M/K) Mˣ

The units along a tower of Galois extensions: for K ⊆ L ⊆ M with L/K normal, the inclusion Lˣ → Mˣ is a morphism of Gal(M/K)-representations from Lˣ, on which Gal(M/K) acts through restriction to L, to Mˣ. It is the coefficient map of inflation Hⁿ(Gal(L/K), Lˣ) → Hⁿ(Gal(M/K), Mˣ).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.unitsInflationHom_apply (K L M : Type u) [Field K] [Field L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [Normal K L] (a : Lˣ) :
    (Rep.Hom.hom (unitsInflationHom K L M)) (Rep.toAdditive.symm (Additive.ofMul a)) = Rep.toAdditive.symm (Additive.ofMul ((Units.map ↑(algebraMap L M)) a))

    unitsInflationHom K L M is the inclusion Lˣ → Mˣ.

    source
    noncomputable def TauCeti.unitsBaseChangeHom (K L : Type u) [Field K] [Field L] [Algebra K L] [Normal K L] (K' M' : Type u) [Field K'] [Field M'] [Algebra K K'] [Algebra K' M'] [Algebra K M'] [IsScalarTower K K' M'] [Algebra L M'] [IsScalarTower K L M'] :
    Rep.res ((AlgEquiv.restrictNormalHom L).comp (AlgEquiv.restrictScalarsHom K)) (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) ⟶ Rep.ofMulDistribMulAction Gal(M'/K') M'ˣ

    The units along a base change of Galois extensions: for K ⊆ K' and L ⊆ M' with L/K normal and M' a K'-algebra, the inclusion Lˣ → M'ˣ is a morphism of Gal(M'/K')-representations from Lˣ, on which Gal(M'/K') acts through restriction to L, to M'ˣ. Together with the homomorphism Gal(M'/K') → Gal(L/K) it induces the cohomology map Hⁿ(Gal(L/K), Lˣ) → Hⁿ(Gal(M'/K'), M'ˣ).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem TauCeti.unitsBaseChangeHom_apply (K L : Type u) [Field K] [Field L] [Algebra K L] [Normal K L] (K' M' : Type u) [Field K'] [Field M'] [Algebra K K'] [Algebra K' M'] [Algebra K M'] [IsScalarTower K K' M'] [Algebra L M'] [IsScalarTower K L M'] (a : Lˣ) :
      (Rep.Hom.hom (unitsBaseChangeHom K L K' M')) (Rep.toAdditive.symm (Additive.ofMul a)) = Rep.toAdditive.symm (Additive.ofMul ((Units.map ↑(algebraMap L M')) a))

      unitsBaseChangeHom K L K' M' is the inclusion Lˣ → M'ˣ.

      source
      theorem TauCeti.toMul_mapCocycles₂_unitsBaseChangeHom (K E L M : Type) [Field K] [Field E] [Field L] [Field M] [Algebra K E] [Algebra K L] [Algebra K M] [Algebra E M] [Algebra L M] [IsScalarTower K E M] [IsScalarTower K L M] [Normal K E] (c : ↥(groupCohomology.cocycles₂ (Rep.ofMulDistribMulAction Gal(E/K) Eˣ))) (g h : Gal(M/L)) :
      Additive.toMul (Rep.toAdditive (((CategoryTheory.ConcreteCategory.hom (groupCohomology.mapCocycles₂ ((AlgEquiv.restrictNormalHom E).comp (AlgEquiv.restrictScalarsHom K)) (unitsBaseChangeHom K E L M))) c) (g, h))) = (Units.map ↑(algebraMap E M)) (Additive.toMul (Rep.toAdditive (c (((AlgEquiv.restrictNormalHom E).comp (AlgEquiv.restrictScalarsHom K)) g, ((AlgEquiv.restrictNormalHom E).comp (AlgEquiv.restrictScalarsHom K)) h))))

      The values of a 2-cocycle pushed along unitsBaseChangeHom K E L M are the images in Mˣ of its values at the restrictions to E.

      source
      theorem TauCeti.map_unitsInflationHom_comp_map_unitsBaseChangeHom (K E L M : Type) [Field K] [Field E] [Field L] [Field M] [Algebra K E] [Algebra K L] [Algebra K M] [Algebra E M] [Algebra L M] [IsScalarTower K E M] [IsScalarTower K L M] [Normal K E] [Normal K M] (n : ℕ) :
      CategoryTheory.CategoryStruct.comp (groupCohomology.map (AlgEquiv.restrictNormalHom E) (unitsInflationHom K E M) n) (groupCohomology.map ((AlgEquiv.restrictNormalHom M).comp (AlgEquiv.restrictScalarsHom K)) (unitsBaseChangeHom K M L M) n) = groupCohomology.map ((AlgEquiv.restrictNormalHom E).comp (AlgEquiv.restrictScalarsHom K)) (unitsBaseChangeHom K E L M) n

      Inflation followed by restriction is base change. For K ⊆ E ⊆ M and K ⊆ L ⊆ M, inflating a class of Hⁿ(Gal(E/K), Eˣ) to Hⁿ(Gal(M/K), Mˣ) and restricting it to Hⁿ(Gal(M/L), Mˣ) is the base change map from E/K to M/L.

      source
      theorem TauCeti.map_unitsInflationHom_two_injective (K L M : Type) [Field K] [Field L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [Normal K L] [FiniteDimensional K M] [IsGalois K M] :
      Function.Injective ⇑(ModuleCat.Hom.hom (groupCohomology.map (AlgEquiv.restrictNormalHom L) (unitsInflationHom K L M) 2))

      Inflation into H²(Gal(M/K), Mˣ) is injective. For a tower K ⊆ L ⊆ M with M/K finite Galois and L/K normal, inflation H²(Gal(L/K), Lˣ) → H²(Gal(M/K), Mˣ) is injective: by Hilbert 90, H¹(Gal(M/L), Mˣ) = 0.

      source
      theorem TauCeti.mem_range_map_unitsInflationHom_two_iff (K L M : Type) [Field K] [Field L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [Normal K L] [FiniteDimensional K M] [IsGalois K M] (x : ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(M/K) Mˣ) 2)) :
      x ∈ (ModuleCat.Hom.hom (groupCohomology.map (AlgEquiv.restrictNormalHom L) (unitsInflationHom K L M) 2)).range ↔ (CategoryTheory.ConcreteCategory.hom (groupCohomology.map ((AlgEquiv.restrictNormalHom M).comp (AlgEquiv.restrictScalarsHom K)) (unitsBaseChangeHom K M L M) 2)) x = 0

      The inflation-restriction sequence of relative Brauer groups. For a tower K ⊆ L ⊆ M with M/K finite Galois and L/K normal, a class of H²(Gal(M/K), Mˣ) is inflated from H²(Gal(L/K), Lˣ) exactly when its restriction to H²(Gal(M/L), Mˣ) vanishes. Restriction is the base change map unitsBaseChangeHom K M L M along Gal(M/L) → Gal(M/K).