Theorems · Definition · field theory

finGaloisGroupMap

{k : Type u_1} →
  {K : Type u_2} →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] →
          {L₁ L₂ : (FiniteGaloisIntermediateField k K)ᵒᵖ} →
            (L₁ ⟶ L₂) → ((Opposite.unop L₁).finGaloisGroup ⟶ (Opposite.unop L₂).finGaloisGroup)

For FiniteGaloisIntermediateField s L₁ and L₂ with L₂ ≤ L₁ the restriction homomorphism from Gal(L₁/k) to Gal(L₂/k)

Defined in

Mathlib.FieldTheory.Galois.Profinite

Cited by

2 results in Mathlib

Foundations

Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebra