Theorems · Theorem · field theory

InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj

∀ {k : Type u_3} {K : Type u_4} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  (g : ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop)
  {L₁ L₂ : FiniteGaloisIntermediateField k K} (h : L₁ ⟶ L₂),
  (CategoryTheory.ConcreteCategory.hom ((finGaloisGroupFunctor k K).map h.op)) ((InfiniteGalois.proj L₂) g) =
    (InfiniteGalois.proj L₁) g

Defined in

Mathlib.FieldTheory.Galois.Profinite

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra