Theorems · Definition · field theory

finGaloisGroupFunctor

(k : Type u_1) →
  (K : Type u_2) →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] → CategoryTheory.Functor (FiniteGaloisIntermediateField k K)ᵒᵖ FiniteGrp.{u_2}

The functor from FiniteGaloisIntermediateField (ordered by reverse inclusion) to FiniteGrp, mapping each FiniteGaloisIntermediateField L to Gal (L/k)

Defined in: Mathlib.FieldTheory.Galois.Profinite
Cited by: 2 results in Mathlib
Foundations: Depth 154 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field Field Algebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Functorstatement · cited by 16,252
Algebrastatement and proof · cited by 11,388
Oppositestatement and proof · cited by 8,081
Fieldstatement and proof · cited by 7,404
Opposite.unopproof · cited by 2,231
FiniteGaloisIntermediateFieldstatement and proof · cited by 32
FiniteGrpstatement · cited by 11
FiniteGaloisIntermediateField.finGaloisGroupproof · cited by 2
finGaloisGroupMapproof · cited by 2
finGaloisGroupMap.map_compproof · cited by 0
finGaloisGroupMap.map_idproof · cited by 0

Cited by3

Results whose statement or proof uses this declaration.

InfiniteGalois.asProfiniteGaloisGroupFunctorproof · cited by 13
InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_projstatement · cited by 1
InfiniteGalois.proj_of_leproof · cited by 1