Documentation

Iwasawalib.FieldTheory.Galois.Abelian

Supplementary results for abelian extension #

Product of a family of group homomorphisms (should go mathlib) #

source
theorem MonoidHom.ker_pi {M : Type u_1} {ι : Type u_2} {N : ι → Type u_3} [Group M] [(i : ι) → MulOneClass (N i)] (f : (i : ι) → M →* N i) :
(pi f).ker = ⨅ (i : ι), (f i).ker
source
theorem AddMonoidHom.ker_pi {M : Type u_1} {ι : Type u_2} {N : ι → Type u_3} [AddGroup M] [(i : ι) → AddZeroClass (N i)] (f : (i : ι) → M →+ N i) :
(pi f).ker = ⨅ (i : ι), (f i).ker

The group homomorphism Gal(⨆ i, E_i/F) → Π i, Gal(E_i/F) #

source
theorem IntermediateField.fixingSubgroup_iSup {F : Type u_1} {K : Type u_2} {ι : Type u_3} [Field F] [Field K] [Algebra F K] (E : ι → IntermediateField F K) :
(⨆ (i : ι), E i).fixingSubgroup = ⨅ (i : ι), (E i).fixingSubgroup

TODO: go mathlib

source
noncomputable def IntermediateField.piRestrictNormalHom {F : Type u_1} {K : Type u_2} {ι : Type u_3} [Field F] [Field K] [Algebra F K] (E : ι → IntermediateField F K) [∀ (i : ι), Normal F ↥(E i)] :
Gal(K/F) →* (i : ι) → Gal(↥(E i)/F)

The group homomorphism Gal(K/F) → Π i, Gal(E_i/F) for a family E_i of intermediate fields of K / F which are normal over F.

Equations
Instances For
    source
    theorem IntermediateField.continuous_piRestrictNormalHom {F : Type u_1} {K : Type u_2} {ι : Type u_3} [Field F] [Field K] [Algebra F K] (E : ι → IntermediateField F K) [∀ (i : ι), Normal F ↥(E i)] :
    Continuous ⇑(piRestrictNormalHom E)
    source
    theorem IntermediateField.ker_piRestrictNormalHom {F : Type u_1} {K : Type u_2} {ι : Type u_3} [Field F] [Field K] [Algebra F K] (E : ι → IntermediateField F K) [∀ (i : ι), Normal F ↥(E i)] :
    (piRestrictNormalHom E).ker = (⨆ (i : ι), E i).fixingSubgroup
    source
    theorem IntermediateField.injective_piRestrictNormalHom_of_iSup_eq_top {F : Type u_1} {K : Type u_2} {ι : Type u_3} [Field F] [Field K] [Algebra F K] (E : ι → IntermediateField F K) [∀ (i : ι), Normal F ↥(E i)] (h : ⨆ (i : ι), E i = ⊤) :
    Function.Injective ⇑(piRestrictNormalHom E)
    source
    noncomputable def IntermediateField.piRestrictNormalHom' {F : Type u_1} {K : Type u_2} {ι : Type u_3} [Field F] [Field K] [Algebra F K] (E : ι → IntermediateField F K) [∀ (i : ι), Normal F ↥(E i)] (E' : IntermediateField F K) (h : ⨆ (i : ι), E i = E') :
    Gal(↥E'/F) →* (i : ι) → Gal(↥(E i)/F)

    The (injective) group homomorphism Gal((⨆ i, E_i)/F) → Π i, Gal(E_i/F) for a family E_i of intermediate fields of K / F which are normal over F.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem IntermediateField.continuous_piRestrictNormalHom' {F : Type u_1} {K : Type u_2} {ι : Type u_3} [Field F] [Field K] [Algebra F K] (E : ι → IntermediateField F K) [∀ (i : ι), Normal F ↥(E i)] (E' : IntermediateField F K) (h : ⨆ (i : ι), E i = E') :
      Continuous ⇑(piRestrictNormalHom' E E' h)
      source
      theorem IntermediateField.injective_piRestrictNormalHom' {F : Type u_1} {K : Type u_2} {ι : Type u_3} [Field F] [Field K] [Algebra F K] (E : ι → IntermediateField F K) [∀ (i : ι), Normal F ↥(E i)] (E' : IntermediateField F K) (h : ⨆ (i : ι), E i = E') :
      Function.Injective ⇑(piRestrictNormalHom' E E' h)

      Compositum of abelian extensions is abelian #

      source
      instance IntermediateField.isAbelianGalois_iSup {F : Type u_1} {K : Type u_2} {ι : Type u_3} [Field F] [Field K] [Algebra F K] (E : ι → IntermediateField F K) [∀ (i : ι), IsAbelianGalois F ↥(E i)] :
      IsAbelianGalois F ↥(⨆ (i : ι), E i)
      source
      instance IntermediateField.isAbelianGalois_sup {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (E1 E2 : IntermediateField F K) [IsAbelianGalois F ↥E1] [IsAbelianGalois F ↥E2] :
      IsAbelianGalois F ↥(E1 ⊔ E2)

      Abelian extension can be transferred by ring isomorphisms #

      source
      theorem IsAbelianGalois.of_algEquiv {F : Type u_4} {E : Type u_5} [Field F] [Field E] {E' : Type u_6} [Field E'] [Algebra F E'] [Algebra F E] [IsAbelianGalois F E] (f : E ≃ₐ[F] E') :
      IsAbelianGalois F E'

      TODO: go mathlib

      source
      theorem IsAbelianGalois.of_equiv_equiv {F : Type u_4} {E : Type u_5} [Field F] [Field E] [Algebra F E] {M : Type u_6} {N : Type u_7} [Field M] [Field N] [Algebra M N] {f : F ≃+* M} {g : E ≃+* N} (hcomp : (algebraMap M N).comp ↑f = (↑g).comp (algebraMap F E)) [IsAbelianGalois F E] :
      IsAbelianGalois M N

      TODO: go mathlib