Supplementary results for abelian extension #

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

def MonoidHom.pi {M : Type u_1} {ι : Type u_2} {N : ι → Type u_3} [MulOneClass M] [(i : ι) → MulOneClass (N i)] (f : (i : ι) → M →* N i) :

M →* (i : ι) → N i

Combine a family of MonoidHoms f_i : M →* N_i into M →* ∏ i, N i given by x ↦ (i ↦ f_i x).

Equations

MonoidHom.pi f = { toFun := fun (x : M) (i : ι) => (f i) x, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

def AddMonoidHom.pi {M : Type u_1} {ι : Type u_2} {N : ι → Type u_3} [AddZeroClass M] [(i : ι) → AddZeroClass (N i)] (f : (i : ι) → M →+ N i) :

M →+ (i : ι) → N i

Combine a family of AddMonoidHoms f_i : M →+ N_i into M →+ ∏ i, N i given by x ↦ (i ↦ f_i x).

Equations

AddMonoidHom.pi f = { toFun := fun (x : M) (i : ι) => (f i) x, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem AddMonoidHom.pi_apply {M : Type u_1} {ι : Type u_2} {N : ι → Type u_3} [AddZeroClass M] [(i : ι) → AddZeroClass (N i)] (f : (i : ι) → M →+ N i) (x : M) (i : ι) :

(AddMonoidHom.pi f) x i = (f i) x

source

@[simp]

theorem MonoidHom.pi_apply {M : Type u_1} {ι : Type u_2} {N : ι → Type u_3} [MulOneClass M] [(i : ι) → MulOneClass (N i)] (f : (i : ι) → M →* N i) (x : M) (i : ι) :

(MonoidHom.pi f) x i = (f i) x

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) :

(MonoidHom.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) :

(AddMonoidHom.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

IntermediateField.piRestrictNormalHom E = MonoidHom.pi fun (i : ι) => AlgEquiv.restrictNormalHom ↥(E i)

Instances For

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)] :

Gal(↥(⨆ (i : ι), E i)/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