NYLL
Module

InfiniteGaloisCorrespondence.lean

Nyll.ValuedFieldTheory.Ramification.GaloisValuation.AbsoluteGalois.InfiniteGaloisCorrespondence
107 declarations indexed from sourceView source ↗

Module documentation

Provides the public declarations in the RamificationTheory.GaloisValuation.AbsoluteGalois.InfiniteGaloisCorrespondence Lean module.

Imports2
Imported by9

Declarations

theorem

quotientAction_ker_eq_normalCore

L28 ↗
RamificationTheory.Field.absoluteGaloisGroup.quotientAction_ker_eq_normalCore
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem quotientAction_ker_eq_normalCore
    {G : Type*} [Group G] (H : Subgroup G) :
    (MulAction.toPermHom G (G ⧸ H)).ker = H.normalCore
theorem

normalCore_finiteIndex_of_finite_quotient

L51 ↗
RamificationTheory.Field.absoluteGaloisGroup.normalCore_finiteIndex_of_finite_quotient
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem normalCore_finiteIndex_of_finite_quotient
    {G : Type*} [Group G] (H : Subgroup G) [Finite (G ⧸ H)] :
    H.normalCore.FiniteIndex
theorem

finiteDimensional_comap_algEquiv

L58 ↗
RamificationTheory.Field.absoluteGaloisGroup.finiteDimensional_comap_algEquiv
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem finiteDimensional_comap_algEquiv
    {F : Type u} {A : Type v} {B : Type w} [Field F] [Field A] [Field B]
    [Algebra F A] [Algebra F B]
    (e : A ≃ₐ[F] B) (E : IntermediateField F B)
    [FiniteDimensional F E] :
    FiniteDimensional F (E.comap e.toAlgHom)
theorem

finiteDimensional_map_algEquiv

L89 ↗
RamificationTheory.Field.absoluteGaloisGroup.finiteDimensional_map_algEquiv
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem finiteDimensional_map_algEquiv
    {F : Type u} {A : Type v} {B : Type w} [Field F] [Field A] [Field B]
    [Algebra F A] [Algebra F B]
    (e : A ≃ₐ[F] B) (E : IntermediateField F A)
    [FiniteDimensional F E] :
    FiniteDimensional F (E.map e.toAlgHom)
def

semilinearRingEquivPreimageIntermediateField

L123 ↗
RamificationTheory.Field.absoluteGaloisGroup.semilinearRingEquivPreimageIntermediateField
Documentation

Pull back an intermediate field along a ring equivalence which is semilinear over a base-field equivalence. This is the finite-level source needed for Krull-continuity of conjugation by such a semilinear equivalence.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · full declaration
def semilinearRingEquivPreimageIntermediateField
    {F : Type u} {F' : Type w} {Ω : Type v} {Ω' : Type z}
    [Field F] [Field F'] [Field Ω] [Field Ω']
    [Algebra F Ω] [Algebra F' Ω']
    (τ : F ≃+* F') (e : Ω ≃+* Ω')
    (he : ∀ x : F,
      e (algebraMap F Ω x) = algebraMap F' Ω' (τ x))
    (E : IntermediateField F' Ω') : IntermediateField F Ω where
  carrier := {x : Ω | e x ∈ E}
  zero_mem' := by
    simp
  one_mem' := by
    simp
  add_mem' := by
    intro x y hx hy
    simpa using E.add_mem hx hy
  mul_mem' := by
    intro x y hx hy
    simpa using E.mul_mem hx hy
  inv_mem' := by
    intro x hx
    simpa using E.inv_mem hx
  algebraMap_mem' := by
    intro x
    change e (algebraMap F Ω x) ∈ E
    rw [he x]
    exact E.algebraMap_mem (τ x)
theorem

mem_semilinearRingEquivPreimageIntermediateField_iff

L153 ↗
RamificationTheory.Field.absoluteGaloisGroup.mem_semilinearRingEquivPreimageIntermediateField_iff
Documentation

States the theorem mem_semilinearRingEquivPreimageIntermediateField_iff.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem mem_semilinearRingEquivPreimageIntermediateField_iff
    {F : Type u} {F' : Type w} {Ω : Type v} {Ω' : Type z}
    [Field F] [Field F'] [Field Ω] [Field Ω']
    [Algebra F Ω] [Algebra F' Ω']
    (τ : F ≃+* F') (e : Ω ≃+* Ω')
    (he : ∀ x : F,
      e (algebraMap F Ω x) = algebraMap F' Ω' (τ x))
    (E : IntermediateField F' Ω') (x : Ω) :
    x ∈ semilinearRingEquivPreimageIntermediateField τ e he E ↔ e x ∈ E
theorem

semilinearRingEquivPreimageIntermediateField_symm_mem

L165 ↗
RamificationTheory.Field.absoluteGaloisGroup.semilinearRingEquivPreimageIntermediateField_symm_mem
Documentation

States the theorem semilinearRingEquivPreimageIntermediateField_symm_mem.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem semilinearRingEquivPreimageIntermediateField_symm_mem
    {F : Type u} {F' : Type w} {Ω : Type v} {Ω' : Type z}
    [Field F] [Field F'] [Field Ω] [Field Ω']
    [Algebra F Ω] [Algebra F' Ω']
    (τ : F ≃+* F') (e : Ω ≃+* Ω')
    (he : ∀ x : F,
      e (algebraMap F Ω x) = algebraMap F' Ω' (τ x))
    (E : IntermediateField F' Ω') {x : Ω'} (hx : x ∈ E) :
    e.symm x ∈ semilinearRingEquivPreimageIntermediateField τ e he E
theorem

finiteDimensional_semilinearRingEquivPreimageIntermediateField

L178 ↗
RamificationTheory.Field.absoluteGaloisGroup.finiteDimensional_semilinearRingEquivPreimageIntermediateField
Documentation

The semilinear pullback of a finite intermediate field is finite.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem finiteDimensional_semilinearRingEquivPreimageIntermediateField
    {F : Type u} {F' : Type w} {Ω : Type v} {Ω' : Type z}
    [Field F] [Field F'] [Field Ω] [Field Ω']
    [Algebra F Ω] [Algebra F' Ω']
    (τ : F ≃+* F') (e : Ω ≃+* Ω')
    (he : ∀ x : F,
      e (algebraMap F Ω x) = algebraMap F' Ω' (τ x))
    (E : IntermediateField F' Ω') [FiniteDimensional F' E] :
    FiniteDimensional F
      (semilinearRingEquivPreimageIntermediateField τ e he E)
theorem

semilinear_conjugation_continuous

L236 ↗
RamificationTheory.Field.absoluteGaloisGroup.semilinear_conjugation_continuous
Documentation

Conjugation by a semilinear equivalence of an algebraic closure is continuous for the Krull topology. The semilinear base action is recorded explicitly by he, and the group homomorphism is required only to have the corresponding conjugation formula on underlying ring equivalences.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem semilinear_conjugation_continuous
    {F : Type u} {F' : Type w} {Ω : Type v} {Ω' : Type z}
    [Field F] [Field F'] [Field Ω] [Field Ω']
    [Algebra F Ω] [Algebra F' Ω']
    (τ : F ≃+* F') (e : Ω ≃+* Ω')
    (he : ∀ x : F,
      e (algebraMap F Ω x) = algebraMap F' Ω' (τ x))
    (φ : Gal(Ω / F) →* Gal(Ω' / F'))
    (hφ : ∀ g : Gal(Ω / F),
      (φ g).toRingEquiv =
        e.symm.trans (g.toRingEquiv.trans e)) :
    Continuous φ
theorem

algEquiv_autCongr_continuous

L279 ↗
RamificationTheory.Field.absoluteGaloisGroup.algEquiv_autCongr_continuous
Documentation

Algebra-equivalence conjugation is continuous for Krull topologies.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem algEquiv_autCongr_continuous
    {F : Type u} {A : Type v} {B : Type w} [Field F] [Field A] [Field B]
    [Algebra F A] [Algebra F B]
    (e : A ≃ₐ[F] B) :
    Continuous (AlgEquiv.autCongr e : Gal(A / F) → Gal(B / F))
theorem

algEquiv_autCongr_symm_continuous

L314 ↗
RamificationTheory.Field.absoluteGaloisGroup.algEquiv_autCongr_symm_continuous
Documentation

The inverse of algebra-equivalence conjugation is continuous for Krull topologies.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem algEquiv_autCongr_symm_continuous
    {F : Type u} {A : Type v} {B : Type w} [Field F] [Field A] [Field B]
    [Algebra F A] [Algebra F B]
    (e : A ≃ₐ[F] B) :
    Continuous ((AlgEquiv.autCongr e).symm : Gal(B / F) → Gal(A / F))
def

separableClosureExtensionAlgEquiv

L325 ↗
RamificationTheory.Field.absoluteGaloisGroup.separableClosureExtensionAlgEquiv
Documentation

Extend a K-automorphism of the absolute separable closure to the fixed chosen algebraic closure. The extension is canonical because AlgebraicClosure K is purely inseparable over SeparableClosure K.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
def separableClosureExtensionAlgEquiv
    (K : Type u) [Field K]
    (τ : Gal(SeparableClosure K/K)) :
    Gal(AlgebraicClosure K / K)
def

restrictToSeparableClosure

L375 ↗
RamificationTheory.Field.absoluteGaloisGroup.restrictToSeparableClosure
Documentation

Restrict an absolute Galois element of the chosen algebraic closure to the absolute separable closure.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · full declaration
def restrictToSeparableClosure
    (K : Type u) [Field K] :
    Gal(AlgebraicClosure K / K) →* Gal(SeparableClosure K / K) where
  toFun σ := AlgEquiv.separableClosure σ
  map_one' := by
    ext x
    rfl
  map_mul' σ τ := by
    ext x
    rfl
theorem

separableClosureExtensionAlgEquiv_restricts

L388 ↗
RamificationTheory.Field.absoluteGaloisGroup.separableClosureExtensionAlgEquiv_restricts
Documentation

States the theorem separableClosureExtensionAlgEquiv_restricts.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem separableClosureExtensionAlgEquiv_restricts
    (K : Type u) [Field K]
    (τ : Gal(SeparableClosure K/K)) (x : SeparableClosure K) :
    separableClosureExtensionAlgEquiv K τ x = τ x
theorem

restrictToSeparableClosure_extension

L414 ↗
RamificationTheory.Field.absoluteGaloisGroup.restrictToSeparableClosure_extension
Documentation

States the theorem restrictToSeparableClosure_extension.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem restrictToSeparableClosure_extension
    (K : Type u) [Field K] (τ : Gal(SeparableClosure K/K)) :
    AlgEquiv.separableClosure (separableClosureExtensionAlgEquiv K τ) = τ
theorem

extension_restrictToSeparableClosure

L422 ↗
RamificationTheory.Field.absoluteGaloisGroup.extension_restrictToSeparableClosure
Documentation

States the theorem extension_restrictToSeparableClosure.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem extension_restrictToSeparableClosure
    (K : Type u) [Field K] (σ : Gal(AlgebraicClosure K/K)) :
    separableClosureExtensionAlgEquiv K (AlgEquiv.separableClosure σ) = σ
def

separableClosureMulEquiv

L452 ↗
RamificationTheory.Field.absoluteGaloisGroup.separableClosureMulEquiv
Documentation

The algebraic absolute Galois group of the chosen algebraic closure is canonically the Galois group of the absolute separable closure.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · full declaration
def separableClosureMulEquiv
    (K : Type u) [Field K] :
    Gal(AlgebraicClosure K / K) ≃* Gal(SeparableClosure K / K) where
  toFun σ := AlgEquiv.separableClosure σ
  invFun τ := separableClosureExtensionAlgEquiv K τ
  left_inv σ := extension_restrictToSeparableClosure K σ
  right_inv τ := restrictToSeparableClosure_extension K τ
  map_mul' σ τ := by
    ext x
    rfl
theorem

separableClosureMulEquiv_continuous

L464 ↗
RamificationTheory.Field.absoluteGaloisGroup.separableClosureMulEquiv_continuous
Documentation

States the theorem separableClosureMulEquiv_continuous.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem separableClosureMulEquiv_continuous
    (K : Type u) [Field K] :
    Continuous (separableClosureMulEquiv K :
      Gal(AlgebraicClosure K / K) → Gal(SeparableClosure K / K))
theorem

lift_separableClosure_le_absoluteSeparableClosure

L494 ↗
RamificationTheory.Field.absoluteGaloisGroup.lift_separableClosure_le_absoluteSeparableClosure
Documentation

States the theorem lift_separableClosure_le_absoluteSeparableClosure.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem lift_separableClosure_le_absoluteSeparableClosure
    (K : Type u) [Field K]
    (E : IntermediateField K (AlgebraicClosure K)) :
    IntermediateField.lift (separableClosure K E) ≤
      (separableClosure K (AlgebraicClosure K))
def

separablePartInAbsoluteSeparableClosure

L505 ↗
RamificationTheory.Field.absoluteGaloisGroup.separablePartInAbsoluteSeparableClosure
Documentation

The separable part of a finite algebraic-closure intermediate field, viewed inside the absolute separable closure.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
def separablePartInAbsoluteSeparableClosure
    (K : Type u) [Field K]
    (E : IntermediateField K (AlgebraicClosure K)) :
    IntermediateField K (SeparableClosure K)
theorem

finiteDimensional_separablePartInAbsoluteSeparableClosure

L513 ↗
RamificationTheory.Field.absoluteGaloisGroup.finiteDimensional_separablePartInAbsoluteSeparableClosure
Documentation

States the theorem finiteDimensional_separablePartInAbsoluteSeparableClosure.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem finiteDimensional_separablePartInAbsoluteSeparableClosure
    (K : Type u) [Field K]
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    FiniteDimensional K (separablePartInAbsoluteSeparableClosure K E)
theorem

separableClosureExtension_mem_fixingSubgroup_of_mem_separablePart

L532 ↗
RamificationTheory.Field.absoluteGaloisGroup.separableClosureExtension_mem_fixingSubgroup_of_mem_separablePart
Documentation

States the theorem separableClosureExtension_mem_fixingSubgroup_of_mem_separablePart.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem separableClosureExtension_mem_fixingSubgroup_of_mem_separablePart
    (K : Type u) [Field K]
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E]
    (τ : Gal(SeparableClosure K/K))
    (hτ : τ ∈ (separablePartInAbsoluteSeparableClosure K E).fixingSubgroup) :
    separableClosureExtensionAlgEquiv K τ ∈ E.fixingSubgroup
theorem

separableClosureMulEquiv_symm_continuous

L595 ↗
RamificationTheory.Field.absoluteGaloisGroup.separableClosureMulEquiv_symm_continuous
Documentation

States the theorem separableClosureMulEquiv_symm_continuous.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem separableClosureMulEquiv_symm_continuous
    (K : Type u) [Field K] :
    Continuous ((separableClosureMulEquiv K).symm :
      Gal(SeparableClosure K / K) → Gal(AlgebraicClosure K / K))
def

separableClosureContinuousMulEquiv

L622 ↗
RamificationTheory.Field.absoluteGaloisGroup.separableClosureContinuousMulEquiv
Documentation

Topological identification of the usual algebraic-closure absolute Galois group with the Galois group of the absolute separable closure.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · full declaration
def separableClosureContinuousMulEquiv
    (K : Type u) [Field K] :
    Gal(AlgebraicClosure K / K) ≃ₜ* Gal(SeparableClosure K / K) where
  toMulEquiv := separableClosureMulEquiv K
  continuous_toFun := separableClosureMulEquiv_continuous K
  continuous_invFun := separableClosureMulEquiv_symm_continuous K
def

ofIntermediateFieldInExtension

L631 ↗
RamificationTheory.Field.absoluteGaloisGroup.ofIntermediateFieldInExtension
Documentation

The natural inclusion Gal(M/E) -> Gal(M/K) for an intermediate field E of a field extension M/K.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · full declaration
def ofIntermediateFieldInExtension
    {K : Type u} {M : Type v} [Field K] [Field M] [Algebra K M]
    (E : IntermediateField K M) :
    Gal(M / E) →* Gal(M / K) where
  toFun σ := σ.restrictScalars K
  map_one' := rfl
  map_mul' _ _ := rfl
theorem

ofIntermediateFieldInExtension_apply

L641 ↗
RamificationTheory.Field.absoluteGaloisGroup.ofIntermediateFieldInExtension_apply
Documentation

States the theorem ofIntermediateFieldInExtension_apply.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem ofIntermediateFieldInExtension_apply
    {K : Type u} {M : Type v} [Field K] [Field M] [Algebra K M]
    (E : IntermediateField K M) (σ : Gal(M/E)) :
    ofIntermediateFieldInExtension E σ = σ.restrictScalars K
theorem

range_ofIntermediateFieldInExtension

L648 ↗
RamificationTheory.Field.absoluteGaloisGroup.range_ofIntermediateFieldInExtension
Documentation

The image of Gal(M/E) in Gal(M/K) is exactly the subgroup fixing E.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem range_ofIntermediateFieldInExtension
    {K : Type u} {M : Type v} [Field K] [Field M] [Algebra K M]
    (E : IntermediateField K M) :
    MonoidHom.range (ofIntermediateFieldInExtension E) = E.fixingSubgroup
theorem

restrictNormalHom_ker_eq_range_ofIntermediateFieldInExtension

L667 ↗
RamificationTheory.Field.absoluteGaloisGroup.restrictNormalHom_ker_eq_range_ofIntermediateFieldInExtension
Documentation

Exactness of the finite-level Galois restriction map: ker(Gal(M/K) -> Gal(E/K)) is the image of Gal(M/E) -> Gal(M/K).

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
Lean source · statement
theorem restrictNormalHom_ker_eq_range_ofIntermediateFieldInExtension
    {K : Type u} {M : Type v} [Field K] [Field M] [Algebra K M]
    (E : IntermediateField K M) [Normal K E] :
    (AlgEquiv.restrictNormalHom E : Gal(M / K) →* Gal(E / K)).ker =
      MonoidHom.range (ofIntermediateFieldInExtension E)
def

ofIntermediateField

L679 ↗
RamificationTheory.Field.absoluteGaloisGroup.ofIntermediateField
Documentation

The natural inclusion Gal(K^al/E) → G_K, for an intermediate field E ⊆ K^al.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · full declaration
def ofIntermediateField (E : IntermediateField K (AlgebraicClosure K)) :
    Gal(AlgebraicClosure K / E) →* Gal(AlgebraicClosure K / K) where
  toFun σ := σ.restrictScalars K
  map_one' := rfl
  map_mul' _ _ := rfl
theorem

ofIntermediateField_apply

L687 ↗
RamificationTheory.Field.absoluteGaloisGroup.ofIntermediateField_apply
Documentation

States the theorem ofIntermediateField_apply.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem ofIntermediateField_apply
    (E : IntermediateField K (AlgebraicClosure K))
    (σ : Gal(AlgebraicClosure K/E)) :
    ofIntermediateField K E σ = σ.restrictScalars K
theorem

range_ofIntermediateField

L694 ↗
RamificationTheory.Field.absoluteGaloisGroup.range_ofIntermediateField
Documentation

The image of Gal(K^al/E) in G_K is exactly the subgroup fixing E.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem range_ofIntermediateField
    (E : IntermediateField K (AlgebraicClosure K)) :
    MonoidHom.range (ofIntermediateField K E) = E.fixingSubgroup
theorem

ofIntermediateField_injective

L711 ↗
RamificationTheory.Field.absoluteGaloisGroup.ofIntermediateField_injective
Documentation

The natural inclusion Gal(K^al/E) → G_K is injective.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem ofIntermediateField_injective
    (E : IntermediateField K (AlgebraicClosure K)) :
    Function.Injective (ofIntermediateField K E)
theorem

ofIntermediateField_eq_iff

L721 ↗
RamificationTheory.Field.absoluteGaloisGroup.ofIntermediateField_eq_iff
Documentation

States the theorem ofIntermediateField_eq_iff.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem ofIntermediateField_eq_iff
    (E : IntermediateField K (AlgebraicClosure K))
    (σ τ : Gal(AlgebraicClosure K/E)) :
    ofIntermediateField K E σ = ofIntermediateField K E τ ↔ σ = τ
theorem

finiteDimensional_extendScalars_sup

L727 ↗
RamificationTheory.Field.absoluteGaloisGroup.finiteDimensional_extendScalars_sup
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem finiteDimensional_extendScalars_sup
    (k : Type u) (M : Type v) [Field k] [Field M] [Algebra k M]
    (E F : IntermediateField k M)
    [FiniteDimensional k E] [FiniteDimensional k F] :
    FiniteDimensional E
      (IntermediateField.extendScalars (F := E) (E := E ⊔ F) le_sup_left)
theorem

ofIntermediateFieldInExtension_continuous

L770 ↗
RamificationTheory.Field.absoluteGaloisGroup.ofIntermediateFieldInExtension_continuous
Documentation

For a finite intermediate extension E/K, the natural inclusion Gal(M/E) → Gal(M/K) is continuous for the two Krull topologies.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem ofIntermediateFieldInExtension_continuous
    {k : Type u} {M : Type v} [Field k] [Field M] [Algebra k M]
    [IsGalois k M]
    (E : IntermediateField k M) [FiniteDimensional k E] :
    Continuous (ofIntermediateFieldInExtension E)
theorem

finiteDimensional_restrictScalars

L802 ↗
RamificationTheory.Field.absoluteGaloisGroup.finiteDimensional_restrictScalars
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem finiteDimensional_restrictScalars
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E]
    (F : IntermediateField E (AlgebraicClosure K)) [FiniteDimensional E F] :
    FiniteDimensional K (F.restrictScalars K)
theorem

ofIntermediateField_continuous

L831 ↗
RamificationTheory.Field.absoluteGaloisGroup.ofIntermediateField_continuous
Documentation

The natural inclusion Gal(K^al/E) → G_K is continuous for the Krull topologies when E/K is finite.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem ofIntermediateField_continuous
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    Continuous (ofIntermediateField K E)
def

openSubgroupOfFiniteIntermediateField

L862 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteIntermediateField
Documentation

The finite-subextension open subgroup of G_K corresponding to E ⊆ K^al. This is the concrete form of G_E ≤ G_K.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
def openSubgroupOfFiniteIntermediateField
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    OpenSubgroup (Gal(AlgebraicClosure K / K))
theorem

openSubgroupOfFiniteIntermediateField_toSubgroup

L869 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteIntermediateField_toSubgroup
Documentation

States the theorem openSubgroupOfFiniteIntermediateField_toSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem openSubgroupOfFiniteIntermediateField_toSubgroup
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    (openSubgroupOfFiniteIntermediateField K E :
      Subgroup (Gal(AlgebraicClosure K / K))) =
      E.fixingSubgroup
theorem

mem_openSubgroupOfFiniteIntermediateField

L878 ↗
RamificationTheory.Field.absoluteGaloisGroup.mem_openSubgroupOfFiniteIntermediateField
Documentation

States the theorem mem_openSubgroupOfFiniteIntermediateField.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem mem_openSubgroupOfFiniteIntermediateField
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E]
    (σ : Gal(AlgebraicClosure K/K)) :
    σ ∈ openSubgroupOfFiniteIntermediateField K E ↔
      ∀ x ∈ E, σ x = x
theorem

openSubgroupOfFiniteIntermediateField_le

L888 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteIntermediateField_le
Documentation

The finite-intermediate-field open subgroup construction is contravariant: if E ≤ F, then G_F ≤ G_E inside G_K.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem openSubgroupOfFiniteIntermediateField_le
    (E F : IntermediateField K (AlgebraicClosure K))
    [FiniteDimensional K E] [FiniteDimensional K F] (hEF : E ≤ F) :
    (openSubgroupOfFiniteIntermediateField K F :
      Subgroup (Gal(AlgebraicClosure K / K))) ≤
      openSubgroupOfFiniteIntermediateField K E
def

openSubgroupOfFiniteIntermediateFieldSup

L900 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteIntermediateFieldSup
Documentation

The finite-subextension open subgroup attached to the compositum E ⊔ F. Its underlying subgroup is the intersection of the open subgroups attached to E and F.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
def openSubgroupOfFiniteIntermediateFieldSup
    (E F : IntermediateField K (AlgebraicClosure K))
    [FiniteDimensional K E] [FiniteDimensional K F] :
    OpenSubgroup (Gal(AlgebraicClosure K / K))
theorem

openSubgroupOfFiniteIntermediateFieldSup_toSubgroup

L910 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteIntermediateFieldSup_toSubgroup
Documentation

States the theorem openSubgroupOfFiniteIntermediateFieldSup_toSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem openSubgroupOfFiniteIntermediateFieldSup_toSubgroup
    (E F : IntermediateField K (AlgebraicClosure K))
    [FiniteDimensional K E] [FiniteDimensional K F] :
    (openSubgroupOfFiniteIntermediateFieldSup K E F :
      Subgroup (Gal(AlgebraicClosure K / K))) =
      (openSubgroupOfFiniteIntermediateField K E :
        Subgroup (Gal(AlgebraicClosure K / K))) ⊓
        openSubgroupOfFiniteIntermediateField K F
theorem

mem_openSubgroupOfFiniteIntermediateFieldSup

L922 ↗
RamificationTheory.Field.absoluteGaloisGroup.mem_openSubgroupOfFiniteIntermediateFieldSup
Documentation

States the theorem mem_openSubgroupOfFiniteIntermediateFieldSup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem mem_openSubgroupOfFiniteIntermediateFieldSup
    (E F : IntermediateField K (AlgebraicClosure K))
    [FiniteDimensional K E] [FiniteDimensional K F]
    (σ : Gal(AlgebraicClosure K/K)) :
    σ ∈ openSubgroupOfFiniteIntermediateFieldSup K E F ↔
      σ ∈ openSubgroupOfFiniteIntermediateField K E ∧
        σ ∈ openSubgroupOfFiniteIntermediateField K F
theorem

range_ofIntermediateField_sup

L940 ↗
RamificationTheory.Field.absoluteGaloisGroup.range_ofIntermediateField_sup
Documentation

States the theorem range_ofIntermediateField_sup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem range_ofIntermediateField_sup
    (E F : IntermediateField K (AlgebraicClosure K)) :
    MonoidHom.range (ofIntermediateField K (E ⊔ F)) =
      E.fixingSubgroup ⊓ F.fixingSubgroup
theorem

mem_range_ofIntermediateField_sup_iff

L947 ↗
RamificationTheory.Field.absoluteGaloisGroup.mem_range_ofIntermediateField_sup_iff
Documentation

States the theorem mem_range_ofIntermediateField_sup_iff.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem mem_range_ofIntermediateField_sup_iff
    (E F : IntermediateField K (AlgebraicClosure K))
    (σ : Gal(AlgebraicClosure K/K)) :
    σ ∈ MonoidHom.range (ofIntermediateField K (E ⊔ F)) ↔
      σ ∈ E.fixingSubgroup ∧ σ ∈ F.fixingSubgroup
def

openSubgroupOfNormalClosureFiniteIntermediateField

L956 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfNormalClosureFiniteIntermediateField
Documentation

The normal-closure open subgroup contained in the open subgroup attached to a finite intermediate field.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
def openSubgroupOfNormalClosureFiniteIntermediateField
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    OpenSubgroup (Gal(AlgebraicClosure K / K))
theorem

openSubgroupOfNormalClosureFiniteIntermediateField_toSubgroup

L964 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfNormalClosureFiniteIntermediateField_toSubgroup
Documentation

States the theorem openSubgroupOfNormalClosureFiniteIntermediateField_toSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem openSubgroupOfNormalClosureFiniteIntermediateField_toSubgroup
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    (openSubgroupOfNormalClosureFiniteIntermediateField K E :
      Subgroup (Gal(AlgebraicClosure K / K))) =
      (IntermediateField.normalClosure K E
        (AlgebraicClosure K)).fixingSubgroup
theorem

openSubgroupOfNormalClosureFiniteIntermediateField_le

L973 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfNormalClosureFiniteIntermediateField_le
Documentation

The normal-closure open subgroup lies inside the open subgroup for E.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem openSubgroupOfNormalClosureFiniteIntermediateField_le
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    (openSubgroupOfNormalClosureFiniteIntermediateField K E :
      Subgroup (Gal(AlgebraicClosure K / K))) ≤
      openSubgroupOfFiniteIntermediateField K E
def

openSubgroupOfFiniteIntermediateFieldEquiv

L984 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteIntermediateFieldEquiv
Documentation

The open subgroup Gal(K^al/E) ≤ G_K is canonically isomorphic to the ordinary Galois group Gal(K^al/E).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
def openSubgroupOfFiniteIntermediateFieldEquiv
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    openSubgroupOfFiniteIntermediateField K E ≃* Gal(AlgebraicClosure K / E)
theorem

openSubgroupOfFiniteIntermediateFieldEquiv_apply

L991 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteIntermediateFieldEquiv_apply
Documentation

States the theorem openSubgroupOfFiniteIntermediateFieldEquiv_apply.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem openSubgroupOfFiniteIntermediateFieldEquiv_apply
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E]
    (σ : openSubgroupOfFiniteIntermediateField K E) :
    openSubgroupOfFiniteIntermediateFieldEquiv K E σ =
      { AlgEquiv.toRingEquiv (σ : Gal(AlgebraicClosure K / K)) with
        commutes' := σ.2 }
theorem

coe_openSubgroupOfFiniteIntermediateFieldEquiv_symm_apply

L1001 ↗
RamificationTheory.Field.absoluteGaloisGroup.coe_openSubgroupOfFiniteIntermediateFieldEquiv_symm_apply
Documentation

States the theorem coe_openSubgroupOfFiniteIntermediateFieldEquiv_symm_apply.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem coe_openSubgroupOfFiniteIntermediateFieldEquiv_symm_apply
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E]
    (σ : Gal(AlgebraicClosure K/E)) :
    ((openSubgroupOfFiniteIntermediateFieldEquiv K E).symm σ :
      Gal(AlgebraicClosure K / K)) =
      ofIntermediateField K E σ
theorem

openSubgroupOfFiniteIntermediateFieldEquiv_continuous

L1011 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteIntermediateFieldEquiv_continuous
Documentation

The identification between the finite-subextension open subgroup and Gal(K^al/E) is continuous from the open subgroup to the Galois group.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem openSubgroupOfFiniteIntermediateFieldEquiv_continuous
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    Continuous (openSubgroupOfFiniteIntermediateFieldEquiv K E :
      openSubgroupOfFiniteIntermediateField K E → Gal(AlgebraicClosure K / E))
theorem

openSubgroupOfFiniteIntermediateFieldEquiv_symm_continuous

L1056 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteIntermediateFieldEquiv_symm_continuous
Documentation

The inverse identification Gal(K^al/E) → Gal(K^al/E) ≤ G_K is continuous for finite E/K.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem openSubgroupOfFiniteIntermediateFieldEquiv_symm_continuous
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    Continuous ((openSubgroupOfFiniteIntermediateFieldEquiv K E).symm :
      Gal(AlgebraicClosure K / E) → openSubgroupOfFiniteIntermediateField K E)
def

openSubgroupOfFiniteIntermediateFieldContinuousMulEquiv

L1073 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteIntermediateFieldContinuousMulEquiv
Documentation

The finite-subextension open subgroup is topologically isomorphic to Gal(K^al/E).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
def openSubgroupOfFiniteIntermediateFieldContinuousMulEquiv
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    openSubgroupOfFiniteIntermediateField K E ≃ₜ*
      Gal(AlgebraicClosure K / E)
theorem

range_ofIntermediateField_eq_openSubgroup

L1083 ↗
RamificationTheory.Field.absoluteGaloisGroup.range_ofIntermediateField_eq_openSubgroup
Documentation

The range of the natural inclusion is the finite-subextension open subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem range_ofIntermediateField_eq_openSubgroup
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    MonoidHom.range (ofIntermediateField K E) =
      (openSubgroupOfFiniteIntermediateField K E :
        Subgroup (Gal(AlgebraicClosure K / K)))
theorem

isOpen_range_ofIntermediateField

L1093 ↗
RamificationTheory.Field.absoluteGaloisGroup.isOpen_range_ofIntermediateField
Documentation

In particular, the image of Gal(K^al/E) inside G_K is open whenever E/K is finite.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem isOpen_range_ofIntermediateField
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    IsOpen (MonoidHom.range (ofIntermediateField K E) :
      Set (Gal(AlgebraicClosure K / K)))
theorem

mem_range_ofIntermediateField_iff

L1101 ↗
RamificationTheory.Field.absoluteGaloisGroup.mem_range_ofIntermediateField_iff
Documentation

States the theorem mem_range_ofIntermediateField_iff.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem mem_range_ofIntermediateField_iff
    (E : IntermediateField K (AlgebraicClosure K))
    (σ : Gal(AlgebraicClosure K/K)) :
    σ ∈ MonoidHom.range (ofIntermediateField K E) ↔
      σ ∈ E.fixingSubgroup
instance

fixingSubgroup_normal_of_normal

L1110 ↗
RamificationTheory.Field.absoluteGaloisGroup.fixingSubgroup_normal_of_normal
Documentation

If E/K is normal inside K^al, then the subgroup fixing E is normal in G_K.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
instance fixingSubgroup_normal_of_normal
    (E : IntermediateField K (AlgebraicClosure K)) [Normal K E] :
    E.fixingSubgroup.Normal
theorem

openSubgroupOfFiniteIntermediateField_normal

L1118 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteIntermediateField_normal
Documentation

The finite-subextension open subgroup is normal when the finite subextension is normal over K.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem openSubgroupOfFiniteIntermediateField_normal
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E]
    [Normal K E] :
    ((openSubgroupOfFiniteIntermediateField K E :
      Subgroup (Gal(AlgebraicClosure K / K)))).Normal
theorem

openSubgroupOfNormalClosureFiniteIntermediateField_normal

L1127 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfNormalClosureFiniteIntermediateField_normal
Documentation

The normal-closure open subgroup is normal in G_K.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem openSubgroupOfNormalClosureFiniteIntermediateField_normal
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    ((openSubgroupOfNormalClosureFiniteIntermediateField K E :
      Subgroup (Gal(AlgebraicClosure K / K)))).Normal
instance

instNormal

L1141 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfNormalClosureFiniteIntermediateField.instNormal
Documentation

Provides the instance instNormal.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
instance openSubgroupOfNormalClosureFiniteIntermediateField.instNormal
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    (openSubgroupOfNormalClosureFiniteIntermediateField K E).toSubgroup.Normal
def

quotientEquivGalOfNormalIntermediateField

L1150 ↗
RamificationTheory.Field.absoluteGaloisGroup.quotientEquivGalOfNormalIntermediateField
Documentation

For a normal intermediate field E ⊆ K^al, the quotient G_K/G_E is the ordinary Galois group Gal(E/K). The quotient is written with Gal(AlgebraicClosure K / K) so that the normal-subgroup instance for E.fixingSubgroup is available by typeclass search.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
def quotientEquivGalOfNormalIntermediateField
    (E : IntermediateField K (AlgebraicClosure K)) [Normal K E] :
    Gal(AlgebraicClosure K / K) ⧸ E.fixingSubgroup ≃* Gal(E / K)
theorem

quotientEquivGalOfNormalIntermediateField_mk'

L1161 ↗
RamificationTheory.Field.absoluteGaloisGroup.quotientEquivGalOfNormalIntermediateField_mk'
Documentation

States the theorem quotientEquivGalOfNormalIntermediateField_mk'.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem quotientEquivGalOfNormalIntermediateField_mk'
    (E : IntermediateField K (AlgebraicClosure K)) [Normal K E]
    (σ : Gal(AlgebraicClosure K/K)) :
    quotientEquivGalOfNormalIntermediateField K E
        (QuotientGroup.mk' E.fixingSubgroup σ) =
      AlgEquiv.restrictNormalHom E σ
def

quotientNormalClosureOpenSubgroupEquivGal

L1172 ↗
RamificationTheory.Field.absoluteGaloisGroup.quotientNormalClosureOpenSubgroupEquivGal
Documentation

Quotienting G_K by the normal-closure open subgroup attached to a finite intermediate field gives the Galois group of that normal closure.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
def quotientNormalClosureOpenSubgroupEquivGal
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    Gal(AlgebraicClosure K / K) ⧸
        (openSubgroupOfNormalClosureFiniteIntermediateField K E :
          Subgroup (Gal(AlgebraicClosure K / K))) ≃*
      Gal(IntermediateField.normalClosure K E (AlgebraicClosure K) / K)
theorem

quotientNormalClosureOpenSubgroupEquivGal_mk'

L1183 ↗
RamificationTheory.Field.absoluteGaloisGroup.quotientNormalClosureOpenSubgroupEquivGal_mk'
Documentation

States the theorem quotientNormalClosureOpenSubgroupEquivGal_mk'.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem quotientNormalClosureOpenSubgroupEquivGal_mk'
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E]
    (σ : Gal(AlgebraicClosure K/K)) :
    quotientNormalClosureOpenSubgroupEquivGal K E
        (QuotientGroup.mk'
          (openSubgroupOfNormalClosureFiniteIntermediateField K E :
            Subgroup (Gal(AlgebraicClosure K / K))) σ) =
      AlgEquiv.restrictNormalHom
        (IntermediateField.normalClosure K E (AlgebraicClosure K)) σ
theorem

openSubgroupOfNormalClosureFiniteIntermediateField_index_eq_natCard_gal

L1197 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfNormalClosureFiniteIntermediateField_index_eq_natCard_gal
Documentation

The index of the normal-closure open subgroup is the cardinality of the finite automorphism group of the normal closure.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem openSubgroupOfNormalClosureFiniteIntermediateField_index_eq_natCard_gal
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    (openSubgroupOfNormalClosureFiniteIntermediateField K E :
      Subgroup (Gal(AlgebraicClosure K / K))).index =
      Nat.card (Gal(IntermediateField.normalClosure K E (AlgebraicClosure K) / K))
instance

instFiniteIndex

L1206 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfNormalClosureFiniteIntermediateField.instFiniteIndex
Documentation

Provides the instance instFiniteIndex.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
instance openSubgroupOfNormalClosureFiniteIntermediateField.instFiniteIndex
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    ((openSubgroupOfNormalClosureFiniteIntermediateField K E :
      Subgroup (Gal(AlgebraicClosure K / K)))).FiniteIndex
instance

instFiniteIndex

L1215 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteIntermediateField.instFiniteIndex
Documentation

Provides the instance instFiniteIndex.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
instance openSubgroupOfFiniteIntermediateField.instFiniteIndex
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    ((openSubgroupOfFiniteIntermediateField K E :
      Subgroup (Gal(AlgebraicClosure K / K)))).FiniteIndex
theorem

openSubgroupOfFiniteIntermediateField_index_eq_finrank

L1225 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteIntermediateField_index_eq_finrank
Documentation

If the chosen algebraic closure is Galois over K, the index of the finite-intermediate-field open subgroup is [E : K]. This hypothesis is automatic in characteristic zero, but is intentionally explicit in general.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem openSubgroupOfFiniteIntermediateField_index_eq_finrank
    [IsGalois K (AlgebraicClosure K)]
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    (openSubgroupOfFiniteIntermediateField K E :
      Subgroup (Gal(AlgebraicClosure K / K))).index = Module.finrank K E
theorem

range_ofIntermediateField_finiteIndex

L1235 ↗
RamificationTheory.Field.absoluteGaloisGroup.range_ofIntermediateField_finiteIndex
Documentation

The image of Gal(K^al/E) → G_K has finite index for finite E/K.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem range_ofIntermediateField_finiteIndex
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    (MonoidHom.range (ofIntermediateField K E)).FiniteIndex
theorem

range_ofIntermediateField_index_eq_finrank

L1243 ↗
RamificationTheory.Field.absoluteGaloisGroup.range_ofIntermediateField_index_eq_finrank
Documentation

If the chosen algebraic closure is Galois over K, the image of Gal(K^al/E) → G_K has index [E : K].

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem range_ofIntermediateField_index_eq_finrank
    [IsGalois K (AlgebraicClosure K)]
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    (MonoidHom.range (ofIntermediateField K E)).index = Module.finrank K E
def

closedSubgroupOfOpenSubgroup

L1253 ↗
RamificationTheory.Field.absoluteGaloisGroup.closedSubgroupOfOpenSubgroup
Documentation

An open subgroup of G_K, viewed as a closed subgroup. This is the bridge from the topological finite-level API to mathlib's infinite Galois correspondence.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
def closedSubgroupOfOpenSubgroup
    (H : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    ClosedSubgroup (Gal(AlgebraicClosure K / K))
theorem

closedSubgroupOfOpenSubgroup_toSubgroup

L1262 ↗
RamificationTheory.Field.absoluteGaloisGroup.closedSubgroupOfOpenSubgroup_toSubgroup
Documentation

States the theorem closedSubgroupOfOpenSubgroup_toSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem closedSubgroupOfOpenSubgroup_toSubgroup
    (H : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    (closedSubgroupOfOpenSubgroup K H :
      Subgroup (Gal(AlgebraicClosure K / K))) = H.toSubgroup
def

fixedFieldOfOpenSubgroup

L1269 ↗
RamificationTheory.Field.absoluteGaloisGroup.fixedFieldOfOpenSubgroup
Documentation

The finite fixed field attached to an open subgroup of G_K.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
def fixedFieldOfOpenSubgroup
    (H : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    IntermediateField K (AlgebraicClosure K)
theorem

fixedFieldOfOpenSubgroup_def

L1276 ↗
RamificationTheory.Field.absoluteGaloisGroup.fixedFieldOfOpenSubgroup_def
Documentation

States the theorem fixedFieldOfOpenSubgroup_def.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem fixedFieldOfOpenSubgroup_def
    (H : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    fixedFieldOfOpenSubgroup K H =
      IntermediateField.fixedField H.toSubgroup
theorem

fixingSubgroup_fixedFieldOfOpenSubgroup

L1284 ↗
RamificationTheory.Field.absoluteGaloisGroup.fixingSubgroup_fixedFieldOfOpenSubgroup
Documentation

The fixing subgroup of the fixed field of an open subgroup is the original open subgroup, as a subgroup of G_K.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem fixingSubgroup_fixedFieldOfOpenSubgroup
    [IsGalois K (AlgebraicClosure K)]
    (H : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    (fixedFieldOfOpenSubgroup K H).fixingSubgroup = H.toSubgroup
theorem

finiteDimensional_fixedFieldOfOpenSubgroup

L1292 ↗
RamificationTheory.Field.absoluteGaloisGroup.finiteDimensional_fixedFieldOfOpenSubgroup
Documentation

Open subgroups of G_K have finite fixed fields.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem finiteDimensional_fixedFieldOfOpenSubgroup
    [IsGalois K (AlgebraicClosure K)]
    (H : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    FiniteDimensional K (fixedFieldOfOpenSubgroup K H)
instance

instFiniteDimensional

L1302 ↗
RamificationTheory.Field.absoluteGaloisGroup.fixedFieldOfOpenSubgroup.instFiniteDimensional
Documentation

Provides the instance instFiniteDimensional.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
instance fixedFieldOfOpenSubgroup.instFiniteDimensional
    [IsGalois K (AlgebraicClosure K)]
    (H : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    FiniteDimensional K (fixedFieldOfOpenSubgroup K H)
theorem

fixedFieldOfOpenSubgroup_openSubgroupOfFiniteIntermediateField

L1311 ↗
RamificationTheory.Field.absoluteGaloisGroup.fixedFieldOfOpenSubgroup_openSubgroupOfFiniteIntermediateField
Documentation

The reverse construction sends the finite-subextension open subgroup back to the original finite intermediate field.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem fixedFieldOfOpenSubgroup_openSubgroupOfFiniteIntermediateField
    [IsGalois K (AlgebraicClosure K)]
    (E : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K E] :
    fixedFieldOfOpenSubgroup K
        (openSubgroupOfFiniteIntermediateField K E) = E
theorem

openSubgroupOfFiniteIntermediateField_fixedFieldOfOpenSubgroup

L1322 ↗
RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteIntermediateField_fixedFieldOfOpenSubgroup
Documentation

The finite-intermediate-field construction sends the fixed field of an open subgroup back to that open subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem openSubgroupOfFiniteIntermediateField_fixedFieldOfOpenSubgroup
    [IsGalois K (AlgebraicClosure K)]
    (H : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    openSubgroupOfFiniteIntermediateField K
        (fixedFieldOfOpenSubgroup K H) = H
theorem

intermediateField_eq_of_fixingSubgroup_eq

L1330 ↗
RamificationTheory.Field.absoluteGaloisGroup.intermediateField_eq_of_fixingSubgroup_eq
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem intermediateField_eq_of_fixingSubgroup_eq
    [IsGalois K (AlgebraicClosure K)]
    {E F : IntermediateField K (AlgebraicClosure K)}
    (h : E.fixingSubgroup = F.fixingSubgroup) :
    E = F
theorem

fixedFieldOfOpenSubgroup_le_of_le

L1339 ↗
RamificationTheory.Field.absoluteGaloisGroup.fixedFieldOfOpenSubgroup_le_of_le
Documentation

The open-subgroup fixed-field construction is antitone.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem fixedFieldOfOpenSubgroup_le_of_le
    (H J : OpenSubgroup (Gal(AlgebraicClosure K/K))) (hHJ : H ≤ J) :
    fixedFieldOfOpenSubgroup K J ≤ fixedFieldOfOpenSubgroup K H
theorem

fixedFieldOfOpenSubgroup_le_iff

L1345 ↗
RamificationTheory.Field.absoluteGaloisGroup.fixedFieldOfOpenSubgroup_le_iff
Documentation

Order comparison under the open-subgroup fixed-field correspondence.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem fixedFieldOfOpenSubgroup_le_iff
    [IsGalois K (AlgebraicClosure K)]
    (H J : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    fixedFieldOfOpenSubgroup K H ≤ fixedFieldOfOpenSubgroup K J ↔ J ≤ H
theorem

fixedFieldOfOpenSubgroup_inf

L1363 ↗
RamificationTheory.Field.absoluteGaloisGroup.fixedFieldOfOpenSubgroup_inf
Documentation

Intersection of open subgroups corresponds to compositum of finite fixed fields.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem fixedFieldOfOpenSubgroup_inf
    [IsGalois K (AlgebraicClosure K)]
    (H J : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    fixedFieldOfOpenSubgroup K (H ⊓ J) =
      fixedFieldOfOpenSubgroup K H ⊔ fixedFieldOfOpenSubgroup K J
theorem

fixedFieldOfOpenSubgroup_sup

L1377 ↗
RamificationTheory.Field.absoluteGaloisGroup.fixedFieldOfOpenSubgroup_sup
Documentation

The open subgroup generated by two open subgroups corresponds to the intersection of their finite fixed fields.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem fixedFieldOfOpenSubgroup_sup
    (H J : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    fixedFieldOfOpenSubgroup K (H ⊔ J) =
      fixedFieldOfOpenSubgroup K H ⊓ fixedFieldOfOpenSubgroup K J
def

conjugateOpenSubgroupOfOpenSubgroup

L1414 ↗
RamificationTheory.Field.absoluteGaloisGroup.conjugateOpenSubgroupOfOpenSubgroup
Documentation

Conjugate an arbitrary open subgroup of G_K through the finite-level reverse Galois correspondence. Its fixed field is the image of the original finite fixed field under the chosen absolute Galois element.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
def conjugateOpenSubgroupOfOpenSubgroup
    [IsGalois K (AlgebraicClosure K)]
    (σ : Gal(AlgebraicClosure K/K))
    (H : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    OpenSubgroup (Gal(AlgebraicClosure K / K))
theorem

conjugateOpenSubgroupOfOpenSubgroup_toSubgroup

L1431 ↗
RamificationTheory.Field.absoluteGaloisGroup.conjugateOpenSubgroupOfOpenSubgroup_toSubgroup
Documentation

The subgroup underlying the conjugate open subgroup is the pointwise conjugate subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem conjugateOpenSubgroupOfOpenSubgroup_toSubgroup
    [IsGalois K (AlgebraicClosure K)]
    (σ : Gal(AlgebraicClosure K/K))
    (H : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    (conjugateOpenSubgroupOfOpenSubgroup K σ H :
      Subgroup (Gal(AlgebraicClosure K / K))) =
      Subgroup.map (MulAut.conj σ).toMonoidHom H.toSubgroup
theorem

mem_conjugateOpenSubgroupOfOpenSubgroup_iff

L1456 ↗
RamificationTheory.Field.absoluteGaloisGroup.mem_conjugateOpenSubgroupOfOpenSubgroup_iff
Documentation

Membership in a conjugate arbitrary open subgroup can be tested by conjugating the element back into the original open subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem mem_conjugateOpenSubgroupOfOpenSubgroup_iff
    [IsGalois K (AlgebraicClosure K)]
    (σ τ : Gal(AlgebraicClosure K/K))
    (H : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    τ ∈ conjugateOpenSubgroupOfOpenSubgroup K σ H ↔
      σ⁻¹ * τ * σ ∈ H
theorem

fixedFieldOfConjugateOpenSubgroupOfOpenSubgroup

L1476 ↗
RamificationTheory.Field.absoluteGaloisGroup.fixedFieldOfConjugateOpenSubgroupOfOpenSubgroup
Documentation

The fixed field of the conjugate open subgroup is the conjugate of the finite fixed field.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · full declaration
theorem fixedFieldOfConjugateOpenSubgroupOfOpenSubgroup
    [IsGalois K (AlgebraicClosure K)]
    (σ : Gal(AlgebraicClosure K/K))
    (H : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    fixedFieldOfOpenSubgroup K
        (conjugateOpenSubgroupOfOpenSubgroup K σ H) =
      (fixedFieldOfOpenSubgroup K H).map
        (show Gal(AlgebraicClosure K / K) from σ).toAlgHom := by
  let E : IntermediateField K (AlgebraicClosure K) :=
    fixedFieldOfOpenSubgroup K H
  change fixedFieldOfOpenSubgroup K
      (openSubgroupOfFiniteIntermediateField K
        (E.map (show Gal(AlgebraicClosure K / K) from σ).toAlgHom)) =
    E.map (show Gal(AlgebraicClosure K / K) from σ).toAlgHom
  exact fixedFieldOfOpenSubgroup_openSubgroupOfFiniteIntermediateField K
    (E.map (show Gal(AlgebraicClosure K / K) from σ).toAlgHom)
theorem

fixedFieldOfConjugateOpenSubgroupOfOpenSubgroup_inf

L1496 ↗
RamificationTheory.Field.absoluteGaloisGroup.fixedFieldOfConjugateOpenSubgroupOfOpenSubgroup_inf
Documentation

Conjugation carries the fixed field of an intersection of open subgroups to the conjugate of the compositum of their fixed fields.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · full declaration
theorem fixedFieldOfConjugateOpenSubgroupOfOpenSubgroup_inf
    [IsGalois K (AlgebraicClosure K)]
    (σ : Gal(AlgebraicClosure K/K))
    (H J : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    fixedFieldOfOpenSubgroup K
        (conjugateOpenSubgroupOfOpenSubgroup K σ (H ⊓ J)) =
      (fixedFieldOfOpenSubgroup K H ⊔ fixedFieldOfOpenSubgroup K J).map
        (show Gal(AlgebraicClosure K / K) from σ).toAlgHom := by
  rw [fixedFieldOfConjugateOpenSubgroupOfOpenSubgroup,
    fixedFieldOfOpenSubgroup_inf]
theorem

fixedFieldOfConjugateOpenSubgroupOfOpenSubgroup_sup

L1510 ↗
RamificationTheory.Field.absoluteGaloisGroup.fixedFieldOfConjugateOpenSubgroupOfOpenSubgroup_sup
Documentation

Conjugation carries the fixed field of the generated open subgroup to the conjugate of the intersection of the fixed fields.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · full declaration
theorem fixedFieldOfConjugateOpenSubgroupOfOpenSubgroup_sup
    [IsGalois K (AlgebraicClosure K)]
    (σ : Gal(AlgebraicClosure K/K))
    (H J : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    fixedFieldOfOpenSubgroup K
        (conjugateOpenSubgroupOfOpenSubgroup K σ (H ⊔ J)) =
      (fixedFieldOfOpenSubgroup K H ⊓ fixedFieldOfOpenSubgroup K J).map
        (show Gal(AlgebraicClosure K / K) from σ).toAlgHom := by
  rw [fixedFieldOfConjugateOpenSubgroupOfOpenSubgroup,
    fixedFieldOfOpenSubgroup_sup]
theorem

conjugateOpenSubgroupOfOpenSubgroup_one

L1523 ↗
RamificationTheory.Field.absoluteGaloisGroup.conjugateOpenSubgroupOfOpenSubgroup_one
Documentation

States the theorem conjugateOpenSubgroupOfOpenSubgroup_one.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem conjugateOpenSubgroupOfOpenSubgroup_one
    [IsGalois K (AlgebraicClosure K)]
    (H : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    conjugateOpenSubgroupOfOpenSubgroup K 1 H = H
theorem

conjugateOpenSubgroupOfOpenSubgroup_inf

L1534 ↗
RamificationTheory.Field.absoluteGaloisGroup.conjugateOpenSubgroupOfOpenSubgroup_inf
Documentation

States the theorem conjugateOpenSubgroupOfOpenSubgroup_inf.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem conjugateOpenSubgroupOfOpenSubgroup_inf
    [IsGalois K (AlgebraicClosure K)]
    (σ : Gal(AlgebraicClosure K/K))
    (H J : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    conjugateOpenSubgroupOfOpenSubgroup K σ (H ⊓ J) =
      conjugateOpenSubgroupOfOpenSubgroup K σ H ⊓
        conjugateOpenSubgroupOfOpenSubgroup K σ J
theorem

conjugateOpenSubgroupOfOpenSubgroup_sup

L1551 ↗
RamificationTheory.Field.absoluteGaloisGroup.conjugateOpenSubgroupOfOpenSubgroup_sup
Documentation

States the theorem conjugateOpenSubgroupOfOpenSubgroup_sup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem conjugateOpenSubgroupOfOpenSubgroup_sup
    [IsGalois K (AlgebraicClosure K)]
    (σ : Gal(AlgebraicClosure K/K))
    (H J : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    conjugateOpenSubgroupOfOpenSubgroup K σ (H ⊔ J) =
      conjugateOpenSubgroupOfOpenSubgroup K σ H ⊔
        conjugateOpenSubgroupOfOpenSubgroup K σ J
def

openNormalCoreOfOpenSubgroup

L1568 ↗
RamificationTheory.Field.absoluteGaloisGroup.openNormalCoreOfOpenSubgroup
Documentation

The normal core of an open subgroup of G_K, as an open normal subgroup. This is the canonical finite Galois quotient lying below an arbitrary finite level.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · full declaration
def openNormalCoreOfOpenSubgroup
    [IsGalois K (AlgebraicClosure K)]
    (H : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    OpenNormalSubgroup (Gal(AlgebraicClosure K / K)) where
  toOpenSubgroup :=
    ⟨H.toSubgroup.normalCore, by
      have : Finite (Gal(AlgebraicClosure K / K) ⧸ H.toSubgroup) :=
        Subgroup.quotient_finite_of_isOpen H.toSubgroup H.isOpen
      have : H.toSubgroup.normalCore.FiniteIndex :=
        normalCore_finiteIndex_of_finite_quotient H.toSubgroup
      exact Subgroup.isOpen_of_isClosed_of_finiteIndex H.toSubgroup.normalCore
        (Subgroup.normalCore_isClosed H.toSubgroup (by simpa using H.isClosed))⟩
  isNormal' := Subgroup.normalCore_normal H.toSubgroup
theorem

openNormalCoreOfOpenSubgroup_toSubgroup

L1584 ↗
RamificationTheory.Field.absoluteGaloisGroup.openNormalCoreOfOpenSubgroup_toSubgroup
Documentation

States the theorem openNormalCoreOfOpenSubgroup_toSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem openNormalCoreOfOpenSubgroup_toSubgroup
    [IsGalois K (AlgebraicClosure K)]
    (H : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    (openNormalCoreOfOpenSubgroup K H :
      Subgroup (Gal(AlgebraicClosure K / K))) = H.toSubgroup.normalCore
theorem

openNormalCoreOfOpenSubgroup_le

L1592 ↗
RamificationTheory.Field.absoluteGaloisGroup.openNormalCoreOfOpenSubgroup_le
Documentation

The normal core is contained in the original open subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem openNormalCoreOfOpenSubgroup_le
    [IsGalois K (AlgebraicClosure K)]
    (H : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    (openNormalCoreOfOpenSubgroup K H :
      Subgroup (Gal(AlgebraicClosure K / K))) ≤ H.toSubgroup
def

fixedFieldOfOpenNormalSubgroup

L1602 ↗
RamificationTheory.Field.absoluteGaloisGroup.fixedFieldOfOpenNormalSubgroup
Documentation

The fixed field of an open normal subgroup is a finite Galois intermediate field.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
def fixedFieldOfOpenNormalSubgroup
    (H : OpenNormalSubgroup (Gal(AlgebraicClosure K/K))) :
    IntermediateField K (AlgebraicClosure K)
theorem

fixedFieldOfOpenNormalSubgroup_def

L1609 ↗
RamificationTheory.Field.absoluteGaloisGroup.fixedFieldOfOpenNormalSubgroup_def
Documentation

States the theorem fixedFieldOfOpenNormalSubgroup_def.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem fixedFieldOfOpenNormalSubgroup_def
    (H : OpenNormalSubgroup (Gal(AlgebraicClosure K/K))) :
    fixedFieldOfOpenNormalSubgroup K H =
      IntermediateField.fixedField H.toSubgroup
instance

instFiniteDimensional

L1616 ↗
RamificationTheory.Field.absoluteGaloisGroup.fixedFieldOfOpenNormalSubgroup.instFiniteDimensional
Documentation

Provides the instance instFiniteDimensional.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
instance fixedFieldOfOpenNormalSubgroup.instFiniteDimensional
    [IsGalois K (AlgebraicClosure K)]
    (H : OpenNormalSubgroup (Gal(AlgebraicClosure K/K))) :
    FiniteDimensional K (fixedFieldOfOpenNormalSubgroup K H)
theorem

isGalois_fixedFieldOfOpenNormalSubgroup

L1623 ↗
RamificationTheory.Field.absoluteGaloisGroup.isGalois_fixedFieldOfOpenNormalSubgroup
Documentation

States the theorem isGalois_fixedFieldOfOpenNormalSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem isGalois_fixedFieldOfOpenNormalSubgroup
    [IsGalois K (AlgebraicClosure K)]
    (H : OpenNormalSubgroup (Gal(AlgebraicClosure K/K))) :
    IsGalois K (fixedFieldOfOpenNormalSubgroup K H)
instance

instNormal

L1634 ↗
RamificationTheory.Field.absoluteGaloisGroup.fixedFieldOfOpenNormalSubgroup.instNormal
Documentation

Provides the instance instNormal.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
instance fixedFieldOfOpenNormalSubgroup.instNormal
    [IsGalois K (AlgebraicClosure K)]
    (H : OpenNormalSubgroup (Gal(AlgebraicClosure K/K))) :
    Normal K (fixedFieldOfOpenNormalSubgroup K H)
def

quotientOpenNormalSubgroupEquivGalFixedField

L1644 ↗
RamificationTheory.Field.absoluteGaloisGroup.quotientOpenNormalSubgroupEquivGalFixedField
Documentation

The finite Galois quotient attached to an arbitrary open normal subgroup of G_K.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
def quotientOpenNormalSubgroupEquivGalFixedField
    [IsGalois K (AlgebraicClosure K)]
    (H : OpenNormalSubgroup (Gal(AlgebraicClosure K/K))) :
    Gal(AlgebraicClosure K / K) ⧸ H.toSubgroup ≃*
      Gal(fixedFieldOfOpenNormalSubgroup K H / K)
theorem

quotientOpenNormalSubgroupEquivGalFixedField_mk'

L1658 ↗
RamificationTheory.Field.absoluteGaloisGroup.quotientOpenNormalSubgroupEquivGalFixedField_mk'
Documentation

States the theorem quotientOpenNormalSubgroupEquivGalFixedField_mk'.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem quotientOpenNormalSubgroupEquivGalFixedField_mk'
    [IsGalois K (AlgebraicClosure K)]
    (H : OpenNormalSubgroup (Gal(AlgebraicClosure K/K)))
    (σ : Gal(AlgebraicClosure K/K)) :
    quotientOpenNormalSubgroupEquivGalFixedField K H
        (QuotientGroup.mk' H.toSubgroup σ) =
      AlgEquiv.restrictNormalHom
        (fixedFieldOfOpenNormalSubgroup K H) σ
theorem

fixedFieldOfOpenNormalCoreOfOpenSubgroup

L1678 ↗
RamificationTheory.Field.absoluteGaloisGroup.fixedFieldOfOpenNormalCoreOfOpenSubgroup
Documentation

Passing from an open subgroup to its normal core corresponds on fixed fields to taking the normal closure.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem fixedFieldOfOpenNormalCoreOfOpenSubgroup
    [IsGalois K (AlgebraicClosure K)]
    (H : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    fixedFieldOfOpenNormalSubgroup K
        (openNormalCoreOfOpenSubgroup K H) =
      IntermediateField.normalClosure K (fixedFieldOfOpenSubgroup K H)
        (AlgebraicClosure K)
theorem

fixedFieldOfOpenNormalCoreOfConjugateOpenSubgroupOfOpenSubgroup

L1741 ↗
RamificationTheory.Field.absoluteGaloisGroup.fixedFieldOfOpenNormalCoreOfConjugateOpenSubgroupOfOpenSubgroup
Documentation

Normal core is invariant under conjugating the original open subgroup, expressed on fixed fields.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace Field
namespace absoluteGaloisGroup
open scoped Topology Pointwise
open CategoryTheory
variable (K : Type u) [Field K]
Lean source · statement
theorem fixedFieldOfOpenNormalCoreOfConjugateOpenSubgroupOfOpenSubgroup
    [IsGalois K (AlgebraicClosure K)]
    (σ : Gal(AlgebraicClosure K/K))
    (H : OpenSubgroup (Gal(AlgebraicClosure K/K))) :
    fixedFieldOfOpenNormalSubgroup K
        (openNormalCoreOfOpenSubgroup K
          (conjugateOpenSubgroupOfOpenSubgroup K σ H)) =
      fixedFieldOfOpenNormalSubgroup K
        (openNormalCoreOfOpenSubgroup K H)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.