Module

FiniteExtensionCorrespondence.lean

Nyll.ValuedFieldTheory.Ramification.GaloisValuation.AbsoluteGalois.FiniteExtensionCorrespondence

115 declarations indexed from sourceView source ↗

Module documentation

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

Imports2

Mathlib.SetTheory.Cardinal.Finite
Nyll.ValuedFieldTheory.Ramification.GaloisValuation.AbsoluteGalois.InfiniteGaloisCorrespondence

Imported by8

instance

fixingSubgroupOfExtension_eq_fieldRange_fixingSubgroup

L81 ↗

RamificationTheory.Field.absoluteGaloisGroup.fixingSubgroupOfExtension_eq_fieldRange_fixingSubgroup

Documentation

The concrete pointwise-fixing subgroup is the usual fixing subgroup of the field range i(L).

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem fixingSubgroupOfExtension_eq_fieldRange_fixingSubgroup
    (i : L →ₐ[K] AlgebraicClosure K) :
    fixingSubgroupOfExtension K i =
      (AlgHom.fieldRange i).fixingSubgroup

theorem

fixingSubgroupOfExtension_le_of_fieldRange_le

L106 ↗

RamificationTheory.Field.absoluteGaloisGroup.fixingSubgroupOfExtension_le_of_fieldRange_le

Documentation

If the embedded copy of L is contained in the embedded copy of M, then the subgroup fixing i(M) is contained in the subgroup fixing i(L).

Source context 14 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
section TwoFiniteExtensions
variable {M : Type w} [Field M] [Algebra K M]

Lean source · statement

theorem fixingSubgroupOfExtension_le_of_fieldRange_le
    (iL : L →ₐ[K] AlgebraicClosure K)
    (iM : M →ₐ[K] AlgebraicClosure K)
    (h : AlgHom.fieldRange iL ≤ AlgHom.fieldRange iM) :
    fixingSubgroupOfExtension K iM ≤ fixingSubgroupOfExtension K iL

theorem

fixingSubgroupOfExtension_comp_le

L120 ↗

RamificationTheory.Field.absoluteGaloisGroup.fixingSubgroupOfExtension_comp_le

Documentation

For a tower embedding L -> M -> K^al, the subgroup fixing M is contained in the subgroup fixing L.

Source context 14 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
section TwoFiniteExtensions
variable {M : Type w} [Field M] [Algebra K M]

Lean source · statement

theorem fixingSubgroupOfExtension_comp_le
    (i : M →ₐ[K] AlgebraicClosure K) (j : L →ₐ[K] M) :
    fixingSubgroupOfExtension K i ≤
      fixingSubgroupOfExtension K (i.comp j)

def

openSubgroupOfFiniteExtension_toSubgroup

L140 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteExtension_toSubgroup

Documentation

States the theorem openSubgroupOfFiniteExtension_toSubgroup.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem openSubgroupOfFiniteExtension_toSubgroup [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    (openSubgroupOfFiniteExtension K i :
      Subgroup (Field.absoluteGaloisGroup K)) =
      (AlgHom.fieldRange i).fixingSubgroup

theorem

mem_openSubgroupOfFiniteExtension

L150 ↗

RamificationTheory.Field.absoluteGaloisGroup.mem_openSubgroupOfFiniteExtension

Documentation

States the theorem mem_openSubgroupOfFiniteExtension.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · full declaration

theorem mem_openSubgroupOfFiniteExtension [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) (σ : Field.absoluteGaloisGroup K) :
    σ ∈ openSubgroupOfFiniteExtension K i ↔
      ∀ x ∈ AlgHom.fieldRange i,
        (show Gal(AlgebraicClosure K / K) from σ) x = x := by
  let := finiteDimensional_fieldRange (K := K) i
  exact mem_openSubgroupOfFiniteIntermediateField K (AlgHom.fieldRange i) σ

theorem

mem_openSubgroupOfFiniteExtension_iff_forall_apply_eq

L161 ↗

RamificationTheory.Field.absoluteGaloisGroup.mem_openSubgroupOfFiniteExtension_iff_forall_apply_eq

Documentation

Concrete membership in the finite-extension open subgroup: an element of G_K lies in the copy of G_L exactly when it fixes every embedded element i x.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · full declaration

theorem mem_openSubgroupOfFiniteExtension_iff_forall_apply_eq
    [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) (σ : Field.absoluteGaloisGroup K) :
    σ ∈ openSubgroupOfFiniteExtension K i ↔
      ∀ x : L, (show Gal(AlgebraicClosure K / K) from σ) (i x) = i x := by
  rw [mem_openSubgroupOfFiniteExtension]
  constructor
  · intro hσ x
    exact hσ (i x) ⟨x, rfl⟩
  · intro hσ y hy
    rcases (AlgHom.mem_fieldRange (f := i)).mp hy with ⟨x, rfl⟩
    exact hσ x

theorem

openSubgroupOfFiniteExtension_toSubgroup_eq_fixingSubgroupOfExtension

L176 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteExtension_toSubgroup_eq_fixingSubgroupOfExtension

Documentation

The finite-extension open subgroup is exactly the concrete subgroup fixing the embedded copy i(L) pointwise.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem openSubgroupOfFiniteExtension_toSubgroup_eq_fixingSubgroupOfExtension
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K) :
    (openSubgroupOfFiniteExtension K i :
      Subgroup (Field.absoluteGaloisGroup K)) =
      fixingSubgroupOfExtension K i

theorem

isOpen_fixingSubgroupOfExtension

L185 ↗

RamificationTheory.Field.absoluteGaloisGroup.isOpen_fixingSubgroupOfExtension

Documentation

The subgroup fixing an embedded finite extension is open.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem isOpen_fixingSubgroupOfExtension [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsOpen (fixingSubgroupOfExtension K i :
      Set (Field.absoluteGaloisGroup K))

def

openSubgroupOfNormalClosureFiniteExtension

L193 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfNormalClosureFiniteExtension

Documentation

The normal-closure open subgroup attached to an embedded finite extension.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

def openSubgroupOfNormalClosureFiniteExtension [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    OpenSubgroup (Field.absoluteGaloisGroup K)

theorem

openSubgroupOfNormalClosureFiniteExtension_toSubgroup

L202 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfNormalClosureFiniteExtension_toSubgroup

Documentation

States the theorem openSubgroupOfNormalClosureFiniteExtension_toSubgroup.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem openSubgroupOfNormalClosureFiniteExtension_toSubgroup
    [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    (openSubgroupOfNormalClosureFiniteExtension K i :
      Subgroup (Field.absoluteGaloisGroup K)) =
      (IntermediateField.normalClosure K (AlgHom.fieldRange i)
        (AlgebraicClosure K)).fixingSubgroup

theorem

openSubgroupOfNormalClosureFiniteExtension_le

L214 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfNormalClosureFiniteExtension_le

Documentation

The normal-closure open subgroup lies inside the concrete open subgroup identified with G_L.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem openSubgroupOfNormalClosureFiniteExtension_le
    [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    (openSubgroupOfNormalClosureFiniteExtension K i :
      Subgroup (Field.absoluteGaloisGroup K)) ≤
      openSubgroupOfFiniteExtension K i

theorem

openSubgroupOfNormalClosureFiniteExtension_normal

L226 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfNormalClosureFiniteExtension_normal

Documentation

The normal-closure open subgroup attached to an embedded finite extension is normal in G_K.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem openSubgroupOfNormalClosureFiniteExtension_normal
    [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    ((openSubgroupOfNormalClosureFiniteExtension K i :
      Subgroup (Field.absoluteGaloisGroup K))).Normal

instance

quotientNormalClosureOpenSubgroupEquivGalOfFiniteExtension

L245 ↗

RamificationTheory.Field.absoluteGaloisGroup.quotientNormalClosureOpenSubgroupEquivGalOfFiniteExtension

Documentation

Quotienting by the normal-closure open subgroup attached to an embedded finite extension gives the finite Galois group of the normal closure of i(L).

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

def quotientNormalClosureOpenSubgroupEquivGalOfFiniteExtension
    [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    Field.absoluteGaloisGroup K ⧸
        (openSubgroupOfNormalClosureFiniteExtension K i :
          Subgroup (Field.absoluteGaloisGroup K)) ≃*
      Gal(IntermediateField.normalClosure K (AlgHom.fieldRange i)
        (AlgebraicClosure K) / K)

theorem

quotientNormalClosureOpenSubgroupEquivGalOfFiniteExtension_mk'

L258 ↗

RamificationTheory.Field.absoluteGaloisGroup.quotientNormalClosureOpenSubgroupEquivGalOfFiniteExtension_mk'

Documentation

States the theorem quotientNormalClosureOpenSubgroupEquivGalOfFiniteExtension_mk'.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem quotientNormalClosureOpenSubgroupEquivGalOfFiniteExtension_mk'
    [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup K) :
    quotientNormalClosureOpenSubgroupEquivGalOfFiniteExtension K i
        (QuotientGroup.mk'
          (openSubgroupOfNormalClosureFiniteExtension K i :
            Subgroup (Field.absoluteGaloisGroup K)) σ) =
      AlgEquiv.restrictNormalHom
        (IntermediateField.normalClosure K (AlgHom.fieldRange i)
          (AlgebraicClosure K)) σ

def

normalClosureFiniteExtensionGaloisCard

L277 ↗

RamificationTheory.Field.absoluteGaloisGroup.normalClosureFiniteExtensionGaloisCard

Documentation

The cardinality of the Galois group of the normal closure of an embedded finite extension. The finite-dimensional structure on the field range is installed inside this definition, so the natural cardinal cannot silently use the infinite-type zero fallback.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

def normalClosureFiniteExtensionGaloisCard
    [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) : ℕ

theorem

openSubgroupOfNormalClosureFiniteExtension_index_eq_galoisCard

L286 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfNormalClosureFiniteExtension_index_eq_galoisCard

Documentation

The index of the normal-closure open subgroup attached to an embedded finite extension is the safely computed cardinality of its Galois group.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem openSubgroupOfNormalClosureFiniteExtension_index_eq_galoisCard
    [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    (openSubgroupOfNormalClosureFiniteExtension K i :
      Subgroup (Field.absoluteGaloisGroup K)).index =
      normalClosureFiniteExtensionGaloisCard K i

instance

instFiniteIndex

L297 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteExtension.instFiniteIndex

Documentation

Provides the instance instFiniteIndex.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

instance openSubgroupOfFiniteExtension.instFiniteIndex [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    ((openSubgroupOfFiniteExtension K i :
      Subgroup (Field.absoluteGaloisGroup K))).FiniteIndex

instance

instFiniteIndex

L307 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfNormalClosureFiniteExtension.instFiniteIndex

Documentation

Provides the instance instFiniteIndex.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

instance openSubgroupOfNormalClosureFiniteExtension.instFiniteIndex
    [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    ((openSubgroupOfNormalClosureFiniteExtension K i :
      Subgroup (Field.absoluteGaloisGroup K))).FiniteIndex

theorem

openSubgroupOfFiniteExtension_index_eq_finrank

L320 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteExtension_index_eq_finrank

Documentation

If the chosen algebraic closure is Galois over K, the index of the open subgroup fixing an embedded finite extension is [L : K].

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem openSubgroupOfFiniteExtension_index_eq_finrank
    [FiniteDimensional K L] [IsGalois K (AlgebraicClosure K)]
    (i : L →ₐ[K] AlgebraicClosure K) :
    (openSubgroupOfFiniteExtension K i :
      Subgroup (Field.absoluteGaloisGroup K)).index = Module.finrank K L

def

conjugateEmbedding

L332 ↗

RamificationTheory.Field.absoluteGaloisGroup.conjugateEmbedding

Documentation

Conjugate an embedding i : L -> K^al by an element of G_K.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

def conjugateEmbedding
    (i : L →ₐ[K] AlgebraicClosure K) (σ : Field.absoluteGaloisGroup K) :
    L →ₐ[K] AlgebraicClosure K

theorem

conjugateEmbedding_apply

L339 ↗

RamificationTheory.Field.absoluteGaloisGroup.conjugateEmbedding_apply

Documentation

States the theorem conjugateEmbedding_apply.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · full declaration

theorem conjugateEmbedding_apply
    (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup K) (x : L) :
    conjugateEmbedding K i σ x =
      (show Gal(AlgebraicClosure K / K) from σ) (i x) :=
  rfl

theorem

fieldRange_conjugateEmbedding

L348 ↗

RamificationTheory.Field.absoluteGaloisGroup.fieldRange_conjugateEmbedding

Documentation

The field range of the conjugated embedding is the image of the original embedded field range.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · full declaration

theorem fieldRange_conjugateEmbedding
    (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup K) :
    AlgHom.fieldRange (conjugateEmbedding K i σ) =
      (AlgHom.fieldRange i).map
        (show Gal(AlgebraicClosure K / K) from σ).toAlgHom :=
  (AlgHom.map_fieldRange i
    (show Gal(AlgebraicClosure K / K) from σ).toAlgHom).symm

theorem

mem_openSubgroupOfFiniteExtension_conjugateEmbedding_iff

L360 ↗

RamificationTheory.Field.absoluteGaloisGroup.mem_openSubgroupOfFiniteExtension_conjugateEmbedding_iff

Documentation

Membership in the open subgroup attached to a conjugated embedding is membership in the original open subgroup after conjugating the automorphism back.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem mem_openSubgroupOfFiniteExtension_conjugateEmbedding_iff
    [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K)
    (σ τ : Field.absoluteGaloisGroup K) :
    τ ∈ openSubgroupOfFiniteExtension K (conjugateEmbedding K i σ) ↔
      σ⁻¹ * τ * σ ∈ openSubgroupOfFiniteExtension K i

theorem

openSubgroupOfFiniteExtension_conjugateEmbedding_eq_map

L394 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteExtension_conjugateEmbedding_eq_map

Documentation

Conjugating the embedding conjugates the associated concrete open subgroup inside G_K.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem openSubgroupOfFiniteExtension_conjugateEmbedding_eq_map
    [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup K) :
    (openSubgroupOfFiniteExtension K (conjugateEmbedding K i σ) :
      Subgroup (Field.absoluteGaloisGroup K)) =
      Subgroup.map (MulAut.conj σ).toMonoidHom
        (openSubgroupOfFiniteExtension K i :
          Subgroup (Field.absoluteGaloisGroup K))

theorem

openSubgroupOfFiniteExtension_le_of_fieldRange_le

L424 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteExtension_le_of_fieldRange_le

Documentation

If the embedded copy of L is contained in the embedded copy of M, then the open subgroup identified with G_M is contained in the one identified with G_L.

Source context 14 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
section TwoFiniteExtensions
variable {M : Type w} [Field M] [Algebra K M]

Lean source · statement

theorem openSubgroupOfFiniteExtension_le_of_fieldRange_le
    [FiniteDimensional K L] [FiniteDimensional K M]
    (iL : L →ₐ[K] AlgebraicClosure K)
    (iM : M →ₐ[K] AlgebraicClosure K)
    (h : AlgHom.fieldRange iL ≤ AlgHom.fieldRange iM) :
    (openSubgroupOfFiniteExtension K iM :
      Subgroup (Field.absoluteGaloisGroup K)) ≤
      openSubgroupOfFiniteExtension K iL

theorem

openSubgroupOfFiniteExtension_comp_le

L438 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteExtension_comp_le

Documentation

For a tower embedding L -> M -> K^al, the open subgroup identified with G_M is contained in the one identified with G_L.

Source context 14 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
section TwoFiniteExtensions
variable {M : Type w} [Field M] [Algebra K M]

Lean source · statement

theorem openSubgroupOfFiniteExtension_comp_le
    [FiniteDimensional K L] [FiniteDimensional K M]
    (i : M →ₐ[K] AlgebraicClosure K) (j : L →ₐ[K] M) :
    (openSubgroupOfFiniteExtension K i :
      Subgroup (Field.absoluteGaloisGroup K)) ≤
      openSubgroupOfFiniteExtension K (i.comp j)

def

openSubgroupOfFiniteExtensionSup

L450 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteExtensionSup

Documentation

The open subgroup corresponding to the compositum of the two embedded finite extensions iL(L) and iM(M) inside K^al.

Source context 14 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
section TwoFiniteExtensions
variable {M : Type w} [Field M] [Algebra K M]

Lean source · statement

def openSubgroupOfFiniteExtensionSup
    [FiniteDimensional K L] [FiniteDimensional K M]
    (iL : L →ₐ[K] AlgebraicClosure K)
    (iM : M →ₐ[K] AlgebraicClosure K) :
    OpenSubgroup (Field.absoluteGaloisGroup K)

theorem

openSubgroupOfFiniteExtensionSup_toSubgroup

L465 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteExtensionSup_toSubgroup

Documentation

States the theorem openSubgroupOfFiniteExtensionSup_toSubgroup.

Source context 14 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
section TwoFiniteExtensions
variable {M : Type w} [Field M] [Algebra K M]

Lean source · statement

theorem openSubgroupOfFiniteExtensionSup_toSubgroup
    [FiniteDimensional K L] [FiniteDimensional K M]
    (iL : L →ₐ[K] AlgebraicClosure K)
    (iM : M →ₐ[K] AlgebraicClosure K) :
    (openSubgroupOfFiniteExtensionSup K iL iM :
      Subgroup (Field.absoluteGaloisGroup K)) =
      (openSubgroupOfFiniteExtension K iL :
        Subgroup (Field.absoluteGaloisGroup K)) ⊓
        openSubgroupOfFiniteExtension K iM

theorem

mem_openSubgroupOfFiniteExtensionSup

L489 ↗

RamificationTheory.Field.absoluteGaloisGroup.mem_openSubgroupOfFiniteExtensionSup

Documentation

States the theorem mem_openSubgroupOfFiniteExtensionSup.

Source context 14 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
section TwoFiniteExtensions
variable {M : Type w} [Field M] [Algebra K M]

Lean source · statement

theorem mem_openSubgroupOfFiniteExtensionSup
    [FiniteDimensional K L] [FiniteDimensional K M]
    (iL : L →ₐ[K] AlgebraicClosure K)
    (iM : M →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup K) :
    σ ∈ openSubgroupOfFiniteExtensionSup K iL iM ↔
      σ ∈ openSubgroupOfFiniteExtension K iL ∧
        σ ∈ openSubgroupOfFiniteExtension K iM

theorem

mem_openSubgroupOfFiniteExtensionSup_iff_forall_apply_eq

L517 ↗

RamificationTheory.Field.absoluteGaloisGroup.mem_openSubgroupOfFiniteExtensionSup_iff_forall_apply_eq

Documentation

Concrete pointwise criterion for the compositum open subgroup attached to two embedded finite extensions.

Source context 14 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
section TwoFiniteExtensions
variable {M : Type w} [Field M] [Algebra K M]

Lean source · full declaration

theorem mem_openSubgroupOfFiniteExtensionSup_iff_forall_apply_eq
    [FiniteDimensional K L] [FiniteDimensional K M]
    (iL : L →ₐ[K] AlgebraicClosure K)
    (iM : M →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup K) :
    σ ∈ openSubgroupOfFiniteExtensionSup K iL iM ↔
      (∀ x : L, (show Gal(AlgebraicClosure K / K) from σ) (iL x) = iL x) ∧
        ∀ y : M, (show Gal(AlgebraicClosure K / K) from σ) (iM y) = iM y := by
  rw [mem_openSubgroupOfFiniteExtensionSup,
    mem_openSubgroupOfFiniteExtension_iff_forall_apply_eq,
    mem_openSubgroupOfFiniteExtension_iff_forall_apply_eq]

def

openSubgroupOfFiniteExtensionContinuousMulEquiv

L533 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteExtensionContinuousMulEquiv

Documentation

The finite-extension open subgroup fixing i(L) is topologically isomorphic to Gal(K^al/i(L)).

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

def openSubgroupOfFiniteExtensionContinuousMulEquiv [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    openSubgroupOfFiniteExtension K i ≃ₜ*
      Gal(AlgebraicClosure K / AlgHom.fieldRange i)

def

ofFiniteExtension

L544 ↗

RamificationTheory.Field.absoluteGaloisGroup.ofFiniteExtension

Documentation

The inclusion Gal(K^al / i(L)) → G_K attached to an embedded finite extension.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

def ofFiniteExtension (i : L →ₐ[K] AlgebraicClosure K) :
    Gal(AlgebraicClosure K / AlgHom.fieldRange i) →*
      Field.absoluteGaloisGroup K

theorem

ofFiniteExtension_apply

L551 ↗

RamificationTheory.Field.absoluteGaloisGroup.ofFiniteExtension_apply

Documentation

States the theorem ofFiniteExtension_apply.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem ofFiniteExtension_apply
    (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Gal(AlgebraicClosure K/AlgHom.fieldRange i)) :
    ofFiniteExtension K i σ = σ.restrictScalars K

theorem

ofFiniteExtension_injective

L558 ↗

RamificationTheory.Field.absoluteGaloisGroup.ofFiniteExtension_injective

Documentation

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

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem ofFiniteExtension_injective
    (i : L →ₐ[K] AlgebraicClosure K) :
    Function.Injective (ofFiniteExtension K i)

theorem

ofFiniteExtension_continuous

L565 ↗

RamificationTheory.Field.absoluteGaloisGroup.ofFiniteExtension_continuous

Documentation

The inclusion Gal(K^al / i(L)) → G_K attached to an embedded finite extension is continuous for finite L/K.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem ofFiniteExtension_continuous [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    Continuous (ofFiniteExtension K i)

theorem

range_ofFiniteExtension

L573 ↗

RamificationTheory.Field.absoluteGaloisGroup.range_ofFiniteExtension

Documentation

The image of Gal(K^al / i(L)) in G_K is the open subgroup attached to the embedded finite extension i : L → K^al.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem range_ofFiniteExtension [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    MonoidHom.range (ofFiniteExtension K i) =
      (openSubgroupOfFiniteExtension K i :
        Subgroup (Field.absoluteGaloisGroup K))

theorem

range_ofFiniteExtension_finiteIndex

L582 ↗

RamificationTheory.Field.absoluteGaloisGroup.range_ofFiniteExtension_finiteIndex

Documentation

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

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem range_ofFiniteExtension_finiteIndex [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    (MonoidHom.range (ofFiniteExtension K i)).FiniteIndex

theorem

range_ofFiniteExtension_index_eq_finrank

L590 ↗

RamificationTheory.Field.absoluteGaloisGroup.range_ofFiniteExtension_index_eq_finrank

Documentation

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

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem range_ofFiniteExtension_index_eq_finrank
    [FiniteDimensional K L] [IsGalois K (AlgebraicClosure K)]
    (i : L →ₐ[K] AlgebraicClosure K) :
    (MonoidHom.range (ofFiniteExtension K i)).index = Module.finrank K L

theorem

isOpen_range_ofFiniteExtension

L599 ↗

RamificationTheory.Field.absoluteGaloisGroup.isOpen_range_ofFiniteExtension

Documentation

Hence the image of Gal(K^al / i(L)) in G_K is open for finite L/K.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem isOpen_range_ofFiniteExtension [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsOpen (MonoidHom.range (ofFiniteExtension K i) :
      Set (Field.absoluteGaloisGroup K))

theorem

mem_range_ofFiniteExtension_iff

L607 ↗

RamificationTheory.Field.absoluteGaloisGroup.mem_range_ofFiniteExtension_iff

Documentation

States the theorem mem_range_ofFiniteExtension_iff.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · full declaration

theorem mem_range_ofFiniteExtension_iff
    (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup K) :
    σ ∈ MonoidHom.range (ofFiniteExtension K i) ↔
      ∀ x ∈ AlgHom.fieldRange i,
        (show Gal(AlgebraicClosure K / K) from σ) x = x := by
  change
    (show Gal(AlgebraicClosure K / K) from σ) ∈
        MonoidHom.range (ofIntermediateField K (AlgHom.fieldRange i)) ↔
      ∀ x ∈ AlgHom.fieldRange i,
        (show Gal(AlgebraicClosure K / K) from σ) x = x
  rw [mem_range_ofIntermediateField_iff]
  exact IntermediateField.mem_fixingSubgroup_iff (AlgHom.fieldRange i) σ

theorem

mem_range_ofFiniteExtension_iff_forall_apply_eq

L622 ↗

RamificationTheory.Field.absoluteGaloisGroup.mem_range_ofFiniteExtension_iff_forall_apply_eq

Documentation

Concrete range criterion for Gal(K^al/i(L)) → G_K.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · full declaration

theorem mem_range_ofFiniteExtension_iff_forall_apply_eq
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup K) :
    σ ∈ MonoidHom.range (ofFiniteExtension K i) ↔
      ∀ x : L, (show Gal(AlgebraicClosure K / K) from σ) (i x) = i x := by
  rw [range_ofFiniteExtension]
  exact mem_openSubgroupOfFiniteExtension_iff_forall_apply_eq K i σ

instance

normal_fieldRangeOfExtension

L631 ↗

RamificationTheory.Field.absoluteGaloisGroup.normal_fieldRangeOfExtension

Documentation

Normality of L/K transports to the embedded field range i(L).

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

instance normal_fieldRangeOfExtension
    (i : L →ₐ[K] AlgebraicClosure K) [Normal K L] :
    Normal K (AlgHom.fieldRange i)

theorem

openSubgroupOfFiniteExtension_normal

L638 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteExtension_normal

Documentation

The open subgroup attached to an embedded finite extension is normal when the embedded image is normal over K.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem openSubgroupOfFiniteExtension_normal [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) [Normal K (AlgHom.fieldRange i)] :
    ((openSubgroupOfFiniteExtension K i :
      Subgroup (Field.absoluteGaloisGroup K))).Normal

theorem

openSubgroupOfFiniteExtension_normal_of_normal

L647 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteExtension_normal_of_normal

Documentation

For a finite normal extension, the concrete copy of G_L inside G_K is a normal open subgroup.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem openSubgroupOfFiniteExtension_normal_of_normal
    [FiniteDimensional K L] [Normal K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    ((openSubgroupOfFiniteExtension K i :
      Subgroup (Field.absoluteGaloisGroup K))).Normal

instance

instNormal

L655 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteExtension.instNormal

Documentation

Provides the instance instNormal.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

instance openSubgroupOfFiniteExtension.instNormal
    [FiniteDimensional K L] [Normal K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    (openSubgroupOfFiniteExtension K i).toSubgroup.Normal

instance

instNormal_coe

L662 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteExtension.instNormal_coe

Documentation

Provides the instance instNormal_coe.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

instance openSubgroupOfFiniteExtension.instNormal_coe
    [FiniteDimensional K L] [Normal K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    ((openSubgroupOfFiniteExtension K i :
      Subgroup (Field.absoluteGaloisGroup K))).Normal

def

quotientEquivGalFieldRangeOfNormalFiniteExtension

L671 ↗

RamificationTheory.Field.absoluteGaloisGroup.quotientEquivGalFieldRangeOfNormalFiniteExtension

Documentation

For an embedded finite normal extension, G_K/G_L is the automorphism group of the embedded field range.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

def quotientEquivGalFieldRangeOfNormalFiniteExtension [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) [Normal K (AlgHom.fieldRange i)] :
    Gal(AlgebraicClosure K / K) ⧸ (AlgHom.fieldRange i).fixingSubgroup ≃*
      Gal(AlgHom.fieldRange i / K)

theorem

quotientEquivGalFieldRangeOfNormalFiniteExtension_mk'

L679 ↗

RamificationTheory.Field.absoluteGaloisGroup.quotientEquivGalFieldRangeOfNormalFiniteExtension_mk'

Documentation

States the theorem quotientEquivGalFieldRangeOfNormalFiniteExtension_mk'.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem quotientEquivGalFieldRangeOfNormalFiniteExtension_mk'
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K)
    [Normal K (AlgHom.fieldRange i)] (σ : Gal(AlgebraicClosure K/K)) :
    quotientEquivGalFieldRangeOfNormalFiniteExtension K i
        (QuotientGroup.mk' (AlgHom.fieldRange i).fixingSubgroup σ) =
      AlgEquiv.restrictNormalHom (AlgHom.fieldRange i) σ

def

quotientEquivGalOfNormalFiniteExtension

L689 ↗

RamificationTheory.Field.absoluteGaloisGroup.quotientEquivGalOfNormalFiniteExtension

Documentation

For an embedded finite normal extension, G_K/G_L is the original automorphism group Gal(L/K), transported across the chosen embedding.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

def quotientEquivGalOfNormalFiniteExtension [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) [Normal K (AlgHom.fieldRange i)] :
    Gal(AlgebraicClosure K / K) ⧸ (AlgHom.fieldRange i).fixingSubgroup ≃*
      Gal(L / K)

theorem

quotientEquivGalOfNormalFiniteExtension_mk'

L698 ↗

RamificationTheory.Field.absoluteGaloisGroup.quotientEquivGalOfNormalFiniteExtension_mk'

Documentation

States the theorem quotientEquivGalOfNormalFiniteExtension_mk'.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem quotientEquivGalOfNormalFiniteExtension_mk'
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K)
    [Normal K (AlgHom.fieldRange i)] (σ : Gal(AlgebraicClosure K/K)) :
    quotientEquivGalOfNormalFiniteExtension K i
        (QuotientGroup.mk' (AlgHom.fieldRange i).fixingSubgroup σ) =
      (AlgEquiv.autCongr (AlgEquiv.ofInjectiveField i)).symm
        ((@AlgEquiv.restrictNormalHom K _ (AlgebraicClosure K) _ _
          (AlgHom.fieldRange i) _ _ _ (fieldRangeIsScalarTower K i) _) σ)

def

quotientOpenSubgroupEquivGalFieldRangeOfNormalFiniteExtension

L712 ↗

RamificationTheory.Field.absoluteGaloisGroup.quotientOpenSubgroupEquivGalFieldRangeOfNormalFiniteExtension

Documentation

For an embedded finite normal extension, the quotient by the concrete open subgroup attached to L is the automorphism group of the embedded field range. This is the open-subgroup form of quotientEquivGalFieldRangeOfNormalFiniteExtension.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

def quotientOpenSubgroupEquivGalFieldRangeOfNormalFiniteExtension
    [FiniteDimensional K L] [Normal K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    Field.absoluteGaloisGroup K ⧸
        (openSubgroupOfFiniteExtension K i :
          Subgroup (Field.absoluteGaloisGroup K)) ≃*
      Gal(AlgHom.fieldRange i / K)

theorem

quotientOpenSubgroupEquivGalFieldRangeOfNormalFiniteExtension_mk'

L723 ↗

RamificationTheory.Field.absoluteGaloisGroup.quotientOpenSubgroupEquivGalFieldRangeOfNormalFiniteExtension_mk'

Documentation

States the theorem quotientOpenSubgroupEquivGalFieldRangeOfNormalFiniteExtension_mk'.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem quotientOpenSubgroupEquivGalFieldRangeOfNormalFiniteExtension_mk'
    [FiniteDimensional K L] [Normal K L]
    (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup K) :
    quotientOpenSubgroupEquivGalFieldRangeOfNormalFiniteExtension K i
        (QuotientGroup.mk'
          (openSubgroupOfFiniteExtension K i :
            Subgroup (Field.absoluteGaloisGroup K)) σ) =
      AlgEquiv.restrictNormalHom (AlgHom.fieldRange i) σ

def

quotientOpenSubgroupEquivGalOfNormalFiniteExtension

L737 ↗

RamificationTheory.Field.absoluteGaloisGroup.quotientOpenSubgroupEquivGalOfNormalFiniteExtension

Documentation

For an embedded finite normal extension, G_K / G_L is the original automorphism group Gal(L/K) when G_L is written as the concrete open subgroup of G_K.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

def quotientOpenSubgroupEquivGalOfNormalFiniteExtension
    [FiniteDimensional K L] [Normal K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    Field.absoluteGaloisGroup K ⧸
        (openSubgroupOfFiniteExtension K i :
          Subgroup (Field.absoluteGaloisGroup K)) ≃*
      Gal(L / K)

theorem

quotientOpenSubgroupEquivGalOfNormalFiniteExtension_mk'

L749 ↗

RamificationTheory.Field.absoluteGaloisGroup.quotientOpenSubgroupEquivGalOfNormalFiniteExtension_mk'

Documentation

States the theorem quotientOpenSubgroupEquivGalOfNormalFiniteExtension_mk'.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem quotientOpenSubgroupEquivGalOfNormalFiniteExtension_mk'
    [FiniteDimensional K L] [Normal K L]
    (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup K) :
    quotientOpenSubgroupEquivGalOfNormalFiniteExtension K i
        (QuotientGroup.mk'
          (openSubgroupOfFiniteExtension K i :
            Subgroup (Field.absoluteGaloisGroup K)) σ) =
      (AlgEquiv.autCongr (AlgEquiv.ofInjectiveField i)).symm
        ((@AlgEquiv.restrictNormalHom K _ (AlgebraicClosure K) _ _
          (AlgHom.fieldRange i) _ _ _ (fieldRangeIsScalarTower K i) _) σ)

def

automorphismsOverFieldRangeEquiv

L764 ↗

RamificationTheory.Field.absoluteGaloisGroup.automorphismsOverFieldRangeEquiv

Documentation

Rebase automorphisms over an embedded finite extension from L to its field range i(L).

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · full declaration

def automorphismsOverFieldRangeEquiv
    (i : L →ₐ[K] AlgebraicClosure K) [Algebra L (AlgebraicClosure K)]
    (hmap : ∀ x, algebraMap L (AlgebraicClosure K) x = i x) :
    (AlgebraicClosure K ≃ₐ[L] AlgebraicClosure K) ≃*
      Gal(AlgebraicClosure K / AlgHom.fieldRange i) where
  toFun σ :=
    { σ.toRingEquiv with
      commutes' := by
        intro y
        obtain ⟨x, hx⟩ := (AlgHom.mem_fieldRange (f := i)).mp y.2
        change σ y.1 = y.1
        rw [← hx]
        change σ (i x) = i x
        rw [← hmap x]
        exact σ.commutes x }
  invFun σ :=
    { σ.toRingEquiv with
      commutes' := by
        intro x
        rw [hmap x]
        exact σ.commutes ⟨i x, ⟨x, rfl⟩⟩ }
  left_inv σ := by
    ext x
    rfl
  right_inv σ := by
    ext x
    rfl
  map_mul' σ τ := by
    ext x
    rfl

theorem

automorphismsOverFieldRangeEquiv_continuous

L795 ↗

RamificationTheory.Field.absoluteGaloisGroup.automorphismsOverFieldRangeEquiv_continuous

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem automorphismsOverFieldRangeEquiv_continuous
    (i : L →ₐ[K] AlgebraicClosure K) [Algebra L (AlgebraicClosure K)]
    (hmap : ∀ x, algebraMap L (AlgebraicClosure K) x = i x) :
    Continuous (automorphismsOverFieldRangeEquiv K i hmap :
      (AlgebraicClosure K ≃ₐ[L] AlgebraicClosure K) →
        Gal(AlgebraicClosure K / AlgHom.fieldRange i))

theorem

automorphismsOverFieldRangeEquiv_symm_continuous

L878 ↗

RamificationTheory.Field.absoluteGaloisGroup.automorphismsOverFieldRangeEquiv_symm_continuous

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem automorphismsOverFieldRangeEquiv_symm_continuous
    (i : L →ₐ[K] AlgebraicClosure K) [Algebra L (AlgebraicClosure K)]
    (hmap : ∀ x, algebraMap L (AlgebraicClosure K) x = i x) :
    Continuous ((automorphismsOverFieldRangeEquiv K i hmap).symm :
      Gal(AlgebraicClosure K / AlgHom.fieldRange i) →
        (AlgebraicClosure K ≃ₐ[L] AlgebraicClosure K))

def

equivGalFieldRangeOfFiniteExtension

L977 ↗

RamificationTheory.Field.absoluteGaloisGroup.equivGalFieldRangeOfFiniteExtension

Documentation

For a finite extension L/K embedded in K^al, the absolute Galois group G_L is canonically (up to the chosen algebraic-closure equivalence) identified with Gal(K^al / i(L)).

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

def equivGalFieldRangeOfFiniteExtension [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    Field.absoluteGaloisGroup L ≃*
      Gal(AlgebraicClosure K / AlgHom.fieldRange i)

theorem

equivGalFieldRangeOfFiniteExtension_continuous

L996 ↗

RamificationTheory.Field.absoluteGaloisGroup.equivGalFieldRangeOfFiniteExtension_continuous

Documentation

The field-range identification G_L ≃ Gal(K^al/i(L)) is continuous.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem equivGalFieldRangeOfFiniteExtension_continuous
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K) :
    Continuous (equivGalFieldRangeOfFiniteExtension K i :
      Field.absoluteGaloisGroup L →
        Gal(AlgebraicClosure K / AlgHom.fieldRange i))

theorem

equivGalFieldRangeOfFiniteExtension_symm_continuous

L1021 ↗

RamificationTheory.Field.absoluteGaloisGroup.equivGalFieldRangeOfFiniteExtension_symm_continuous

Documentation

The inverse field-range identification Gal(K^al/i(L)) ≃ G_L is continuous.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem equivGalFieldRangeOfFiniteExtension_symm_continuous
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K) :
    Continuous ((equivGalFieldRangeOfFiniteExtension K i).symm :
      Gal(AlgebraicClosure K / AlgHom.fieldRange i) →
        Field.absoluteGaloisGroup L)

def

equivGalFieldRangeOfFiniteExtensionContinuousMulEquiv

L1046 ↗

RamificationTheory.Field.absoluteGaloisGroup.equivGalFieldRangeOfFiniteExtensionContinuousMulEquiv

Documentation

The field-range identification between G_L and Gal(K^al/i(L)) as a topological group isomorphism.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

def equivGalFieldRangeOfFiniteExtensionContinuousMulEquiv
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K) :
    Field.absoluteGaloisGroup L ≃ₜ*
      Gal(AlgebraicClosure K / AlgHom.fieldRange i)

def

equivOpenSubgroupOfFiniteExtension

L1056 ↗

RamificationTheory.Field.absoluteGaloisGroup.equivOpenSubgroupOfFiniteExtension

Documentation

The concrete open subgroup of G_K attached to i : L → K^al is identified with the absolute Galois group G_L.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

def equivOpenSubgroupOfFiniteExtension [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    Field.absoluteGaloisGroup L ≃* openSubgroupOfFiniteExtension K i

def

equivOpenSubgroupOfFiniteExtensionContinuousMulEquiv

L1065 ↗

RamificationTheory.Field.absoluteGaloisGroup.equivOpenSubgroupOfFiniteExtensionContinuousMulEquiv

Documentation

The concrete open subgroup of G_K attached to i : L → K^al is topologically identified with G_L.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

def equivOpenSubgroupOfFiniteExtensionContinuousMulEquiv
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K) :
    Field.absoluteGaloisGroup L ≃ₜ* openSubgroupOfFiniteExtension K i

def

toOpenSubgroupOfFiniteExtension

L1074 ↗

RamificationTheory.Field.absoluteGaloisGroup.toOpenSubgroupOfFiniteExtension

Documentation

The concrete map from G_L to the finite-extension open subgroup of G_K. This is the subgroup-valued form of the identification G_L ≃ openSubgroupOfFiniteExtension K i.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

def toOpenSubgroupOfFiniteExtension [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    Field.absoluteGaloisGroup L →* openSubgroupOfFiniteExtension K i

def

toOpenSubgroupOfFiniteExtensionContinuous

L1081 ↗

RamificationTheory.Field.absoluteGaloisGroup.toOpenSubgroupOfFiniteExtensionContinuous

Documentation

The subgroup-valued inclusion G_L -> openSubgroupOfFiniteExtension K i as a continuous homomorphism.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

def toOpenSubgroupOfFiniteExtensionContinuous [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    Field.absoluteGaloisGroup L →ₜ* openSubgroupOfFiniteExtension K i

theorem

toOpenSubgroupOfFiniteExtension_apply

L1089 ↗

RamificationTheory.Field.absoluteGaloisGroup.toOpenSubgroupOfFiniteExtension_apply

Documentation

States the theorem toOpenSubgroupOfFiniteExtension_apply.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem toOpenSubgroupOfFiniteExtension_apply
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup L) :
    toOpenSubgroupOfFiniteExtension K i σ =
      equivOpenSubgroupOfFiniteExtension K i σ

theorem

toOpenSubgroupOfFiniteExtensionContinuous_apply

L1098 ↗

RamificationTheory.Field.absoluteGaloisGroup.toOpenSubgroupOfFiniteExtensionContinuous_apply

Documentation

States the theorem toOpenSubgroupOfFiniteExtensionContinuous_apply.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem toOpenSubgroupOfFiniteExtensionContinuous_apply
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup L) :
    toOpenSubgroupOfFiniteExtensionContinuous K i σ =
      equivOpenSubgroupOfFiniteExtension K i σ

theorem

coe_equivOpenSubgroupOfFiniteExtension_apply

L1107 ↗

RamificationTheory.Field.absoluteGaloisGroup.coe_equivOpenSubgroupOfFiniteExtension_apply

Documentation

States the theorem coe_equivOpenSubgroupOfFiniteExtension_apply.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem coe_equivOpenSubgroupOfFiniteExtension_apply
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup L) :
    ((equivOpenSubgroupOfFiniteExtension K i σ :
      openSubgroupOfFiniteExtension K i) :
      Field.absoluteGaloisGroup K) =
      ofFiniteExtension K i (equivGalFieldRangeOfFiniteExtension K i σ)

def

ofFiniteExtensionAbsolute

L1121 ↗

RamificationTheory.Field.absoluteGaloisGroup.ofFiniteExtensionAbsolute

Documentation

The inclusion G_L → G_K obtained by identifying G_L with the open subgroup fixing the embedded image i(L) ⊆ K^al.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

def ofFiniteExtensionAbsolute [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    Field.absoluteGaloisGroup L →* Field.absoluteGaloisGroup K

def

ofFiniteExtensionAbsoluteContinuous

L1130 ↗

RamificationTheory.Field.absoluteGaloisGroup.ofFiniteExtensionAbsoluteContinuous

Documentation

The inclusion G_L -> G_K as a continuous homomorphism. Its range is the concrete open subgroup fixing i(L).

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

def ofFiniteExtensionAbsoluteContinuous [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    Field.absoluteGaloisGroup L →ₜ* Field.absoluteGaloisGroup K

theorem

ofFiniteExtensionAbsolute_apply

L1145 ↗

RamificationTheory.Field.absoluteGaloisGroup.ofFiniteExtensionAbsolute_apply

Documentation

States the theorem ofFiniteExtensionAbsolute_apply.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem ofFiniteExtensionAbsolute_apply [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) (σ : Field.absoluteGaloisGroup L) :
    ofFiniteExtensionAbsolute K i σ =
      (equivOpenSubgroupOfFiniteExtension K i σ :
        Field.absoluteGaloisGroup K)

theorem

ofFiniteExtensionAbsoluteContinuous_apply

L1154 ↗

RamificationTheory.Field.absoluteGaloisGroup.ofFiniteExtensionAbsoluteContinuous_apply

Documentation

States the theorem ofFiniteExtensionAbsoluteContinuous_apply.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem ofFiniteExtensionAbsoluteContinuous_apply [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) (σ : Field.absoluteGaloisGroup L) :
    ofFiniteExtensionAbsoluteContinuous K i σ =
      ofFiniteExtensionAbsolute K i σ

theorem

ofFiniteExtensionAbsolute_continuous

L1161 ↗

RamificationTheory.Field.absoluteGaloisGroup.ofFiniteExtensionAbsolute_continuous

Documentation

States the theorem ofFiniteExtensionAbsolute_continuous.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem ofFiniteExtensionAbsolute_continuous [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    Continuous (ofFiniteExtensionAbsolute K i)

theorem

openSubgroupOfFiniteExtension_subtype_isOpenEmbedding

L1167 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteExtension_subtype_isOpenEmbedding

Documentation

States the theorem openSubgroupOfFiniteExtension_subtype_isOpenEmbedding.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · full declaration

theorem openSubgroupOfFiniteExtension_subtype_isOpenEmbedding
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K) :
    Topology.IsOpenEmbedding (fun σ : openSubgroupOfFiniteExtension K i =>
      (σ : Field.absoluteGaloisGroup K)) :=
  (openSubgroupOfFiniteExtension K i :
    TopologicalSpace.Opens (Field.absoluteGaloisGroup K)).isOpenEmbedding'

theorem

ofFiniteExtensionAbsolute_isOpenEmbedding

L1176 ↗

RamificationTheory.Field.absoluteGaloisGroup.ofFiniteExtensionAbsolute_isOpenEmbedding

Documentation

The inclusion G_L -> G_K is an open embedding onto the finite-extension open subgroup fixing i(L).

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem ofFiniteExtensionAbsolute_isOpenEmbedding [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    Topology.IsOpenEmbedding (ofFiniteExtensionAbsolute K i)

theorem

ofFiniteExtensionAbsolute_eq_ofFiniteExtension

L1190 ↗

RamificationTheory.Field.absoluteGaloisGroup.ofFiniteExtensionAbsolute_eq_ofFiniteExtension

Documentation

The concrete map G_L → G_K agrees with the usual scalar-restriction map after identifying G_L with Gal(K^al / i(L)).

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem ofFiniteExtensionAbsolute_eq_ofFiniteExtension
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup L) :
    ofFiniteExtensionAbsolute K i σ =
      ofFiniteExtension K i (equivGalFieldRangeOfFiniteExtension K i σ)

theorem

ofFiniteExtensionAbsolute_mem_openSubgroup

L1200 ↗

RamificationTheory.Field.absoluteGaloisGroup.ofFiniteExtensionAbsolute_mem_openSubgroup

Documentation

Every element of G_L, viewed inside G_K, lies in the finite-extension open subgroup fixing i(L).

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem ofFiniteExtensionAbsolute_mem_openSubgroup
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup L) :
    ofFiniteExtensionAbsolute K i σ ∈ openSubgroupOfFiniteExtension K i

theorem

ofFiniteExtensionAbsolute_injective

L1209 ↗

RamificationTheory.Field.absoluteGaloisGroup.ofFiniteExtensionAbsolute_injective

Documentation

The concrete inclusion G_L → G_K attached to an embedded finite extension is injective.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem ofFiniteExtensionAbsolute_injective [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    Function.Injective (ofFiniteExtensionAbsolute K i)

theorem

range_ofFiniteExtensionAbsolute

L1219 ↗

RamificationTheory.Field.absoluteGaloisGroup.range_ofFiniteExtensionAbsolute

Documentation

The image of G_L → G_K is exactly the finite-extension open subgroup fixing i(L).

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem range_ofFiniteExtensionAbsolute [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    MonoidHom.range (ofFiniteExtensionAbsolute K i) =
      (openSubgroupOfFiniteExtension K i :
        Subgroup (Field.absoluteGaloisGroup K))

theorem

map_top_ofFiniteExtensionAbsolute

L1234 ↗

RamificationTheory.Field.absoluteGaloisGroup.map_top_ofFiniteExtensionAbsolute

Documentation

States the theorem map_top_ofFiniteExtensionAbsolute.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem map_top_ofFiniteExtensionAbsolute [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    Subgroup.map (ofFiniteExtensionAbsolute K i) ⊤ =
      (openSubgroupOfFiniteExtension K i :
        Subgroup (Field.absoluteGaloisGroup K))

theorem

openSubgroupOfNormalClosureFiniteExtension_le_range

L1243 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfNormalClosureFiniteExtension_le_range

Documentation

The normal-closure open subgroup is contained in the actual image of G_L -> G_K.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem openSubgroupOfNormalClosureFiniteExtension_le_range
    [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    (openSubgroupOfNormalClosureFiniteExtension K i :
      Subgroup (Field.absoluteGaloisGroup K)) ≤
      MonoidHom.range (ofFiniteExtensionAbsolute K i)

theorem

range_ofFiniteExtensionAbsolute_finiteIndex

L1253 ↗

RamificationTheory.Field.absoluteGaloisGroup.range_ofFiniteExtensionAbsolute_finiteIndex

Documentation

States the theorem range_ofFiniteExtensionAbsolute_finiteIndex.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem range_ofFiniteExtensionAbsolute_finiteIndex [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    (MonoidHom.range (ofFiniteExtensionAbsolute K i)).FiniteIndex

theorem

range_ofFiniteExtensionAbsolute_index_eq_finrank

L1261 ↗

RamificationTheory.Field.absoluteGaloisGroup.range_ofFiniteExtensionAbsolute_index_eq_finrank

Documentation

If the chosen algebraic closure is Galois over K, the concrete image of G_L → G_K has index [L : K].

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem range_ofFiniteExtensionAbsolute_index_eq_finrank
    [FiniteDimensional K L] [IsGalois K (AlgebraicClosure K)]
    (i : L →ₐ[K] AlgebraicClosure K) :
    (MonoidHom.range (ofFiniteExtensionAbsolute K i)).index =
      Module.finrank K L

theorem

isOpen_range_ofFiniteExtensionAbsolute

L1270 ↗

RamificationTheory.Field.absoluteGaloisGroup.isOpen_range_ofFiniteExtensionAbsolute

Documentation

Hence the concrete image of G_L in G_K is open for finite L/K.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem isOpen_range_ofFiniteExtensionAbsolute [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsOpen (MonoidHom.range (ofFiniteExtensionAbsolute K i) :
      Set (Field.absoluteGaloisGroup K))

theorem

range_ofFiniteExtensionAbsolute_conjugateEmbedding_eq_map

L1278 ↗

RamificationTheory.Field.absoluteGaloisGroup.range_ofFiniteExtensionAbsolute_conjugateEmbedding_eq_map

Documentation

Conjugating the embedding conjugates the actual image of G_L -> G_K.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem range_ofFiniteExtensionAbsolute_conjugateEmbedding_eq_map
    [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup K) :
    MonoidHom.range
        (ofFiniteExtensionAbsolute K (conjugateEmbedding K i σ)) =
      Subgroup.map (MulAut.conj σ).toMonoidHom
        (MonoidHom.range (ofFiniteExtensionAbsolute K i))

theorem

mem_range_ofFiniteExtensionAbsolute_conjugateEmbedding_iff

L1291 ↗

RamificationTheory.Field.absoluteGaloisGroup.mem_range_ofFiniteExtensionAbsolute_conjugateEmbedding_iff

Documentation

Membership in the image attached to a conjugated embedding can be tested by conjugating back into the original image.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem mem_range_ofFiniteExtensionAbsolute_conjugateEmbedding_iff
    [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K)
    (σ τ : Field.absoluteGaloisGroup K) :
    τ ∈ MonoidHom.range
        (ofFiniteExtensionAbsolute K (conjugateEmbedding K i σ)) ↔
      σ⁻¹ * τ * σ ∈ MonoidHom.range (ofFiniteExtensionAbsolute K i)

theorem

mem_range_ofFiniteExtensionAbsolute_iff

L1304 ↗

RamificationTheory.Field.absoluteGaloisGroup.mem_range_ofFiniteExtensionAbsolute_iff

Documentation

States the theorem mem_range_ofFiniteExtensionAbsolute_iff.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · full declaration

theorem mem_range_ofFiniteExtensionAbsolute_iff [FiniteDimensional K L]
    (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup K) :
    σ ∈ MonoidHom.range (ofFiniteExtensionAbsolute K i) ↔
      ∀ x ∈ AlgHom.fieldRange i,
        (show Gal(AlgebraicClosure K / K) from σ) x = x := by
  rw [range_ofFiniteExtensionAbsolute]
  exact mem_openSubgroupOfFiniteExtension K i σ

theorem

range_ofFiniteExtensionAbsolute_eq_fixingSubgroupOfExtension

L1315 ↗

RamificationTheory.Field.absoluteGaloisGroup.range_ofFiniteExtensionAbsolute_eq_fixingSubgroupOfExtension

Documentation

The image of G_L → G_K is the concrete subgroup fixing i(L) pointwise.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem range_ofFiniteExtensionAbsolute_eq_fixingSubgroupOfExtension
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K) :
    MonoidHom.range (ofFiniteExtensionAbsolute K i) =
      fixingSubgroupOfExtension K i

instance

instNormal

L1323 ↗

RamificationTheory.Field.absoluteGaloisGroup.range_ofFiniteExtensionAbsolute.instNormal

Documentation

Provides the instance instNormal.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

instance range_ofFiniteExtensionAbsolute.instNormal
    [FiniteDimensional K L] [Normal K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    (MonoidHom.range (ofFiniteExtensionAbsolute K i)).Normal

def

quotientRangeEquivGalFieldRangeOfNormalFiniteExtension

L1332 ↗

RamificationTheory.Field.absoluteGaloisGroup.quotientRangeEquivGalFieldRangeOfNormalFiniteExtension

Documentation

For a finite normal extension, the quotient by the actual image of G_L -> G_K is the automorphism group of the embedded field range.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

def quotientRangeEquivGalFieldRangeOfNormalFiniteExtension
    [FiniteDimensional K L] [Normal K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    Field.absoluteGaloisGroup K ⧸
        MonoidHom.range (ofFiniteExtensionAbsolute K i) ≃*
      Gal(AlgHom.fieldRange i / K)

theorem

quotientRangeEquivGalFieldRangeOfNormalFiniteExtension_mk'

L1344 ↗

RamificationTheory.Field.absoluteGaloisGroup.quotientRangeEquivGalFieldRangeOfNormalFiniteExtension_mk'

Documentation

States the theorem quotientRangeEquivGalFieldRangeOfNormalFiniteExtension_mk'.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem quotientRangeEquivGalFieldRangeOfNormalFiniteExtension_mk'
    [FiniteDimensional K L] [Normal K L]
    (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup K) :
    quotientRangeEquivGalFieldRangeOfNormalFiniteExtension K i
        (QuotientGroup.mk'
          (MonoidHom.range (ofFiniteExtensionAbsolute K i)) σ) =
      AlgEquiv.restrictNormalHom (AlgHom.fieldRange i) σ

def

quotientRangeEquivGalOfNormalFiniteExtension

L1364 ↗

RamificationTheory.Field.absoluteGaloisGroup.quotientRangeEquivGalOfNormalFiniteExtension

Documentation

For a finite normal extension, G_K/G_L is Gal(L/K) when G_L is written as the actual image of G_L -> G_K.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

def quotientRangeEquivGalOfNormalFiniteExtension
    [FiniteDimensional K L] [Normal K L]
    (i : L →ₐ[K] AlgebraicClosure K) :
    Field.absoluteGaloisGroup K ⧸
        MonoidHom.range (ofFiniteExtensionAbsolute K i) ≃*
      Gal(L / K)

theorem

quotientRangeEquivGalOfNormalFiniteExtension_mk'

L1375 ↗

RamificationTheory.Field.absoluteGaloisGroup.quotientRangeEquivGalOfNormalFiniteExtension_mk'

Documentation

States the theorem quotientRangeEquivGalOfNormalFiniteExtension_mk'.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem quotientRangeEquivGalOfNormalFiniteExtension_mk'
    [FiniteDimensional K L] [Normal K L]
    (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup K) :
    quotientRangeEquivGalOfNormalFiniteExtension K i
        (QuotientGroup.mk'
          (MonoidHom.range (ofFiniteExtensionAbsolute K i)) σ) =
      (AlgEquiv.autCongr (AlgEquiv.ofInjectiveField i)).symm
        ((@AlgEquiv.restrictNormalHom K _ (AlgebraicClosure K) _ _
          (AlgHom.fieldRange i) _ _ _ (fieldRangeIsScalarTower K i) _) σ)

theorem

range_ofFiniteExtensionAbsolute_le_of_fieldRange_le

L1394 ↗

RamificationTheory.Field.absoluteGaloisGroup.range_ofFiniteExtensionAbsolute_le_of_fieldRange_le

Documentation

The images of absolute Galois groups inside G_K are contravariant in embedded finite extensions.

Source context 14 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
section TwoFiniteExtensions
variable {M : Type w} [Field M] [Algebra K M]

Lean source · statement

theorem range_ofFiniteExtensionAbsolute_le_of_fieldRange_le
    [FiniteDimensional K L] [FiniteDimensional K M]
    (iL : L →ₐ[K] AlgebraicClosure K)
    (iM : M →ₐ[K] AlgebraicClosure K)
    (h : AlgHom.fieldRange iL ≤ AlgHom.fieldRange iM) :
    MonoidHom.range (ofFiniteExtensionAbsolute K iM) ≤
      MonoidHom.range (ofFiniteExtensionAbsolute K iL)

theorem

range_ofFiniteExtensionAbsolute_comp_le

L1406 ↗

RamificationTheory.Field.absoluteGaloisGroup.range_ofFiniteExtensionAbsolute_comp_le

Documentation

For a tower embedding L -> M -> K^al, the image of G_M in G_K is contained in the image of G_L in G_K.

Source context 14 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
section TwoFiniteExtensions
variable {M : Type w} [Field M] [Algebra K M]

Lean source · statement

theorem range_ofFiniteExtensionAbsolute_comp_le
    [FiniteDimensional K L] [FiniteDimensional K M]
    (i : M →ₐ[K] AlgebraicClosure K) (j : L →ₐ[K] M) :
    MonoidHom.range (ofFiniteExtensionAbsolute K i) ≤
      MonoidHom.range (ofFiniteExtensionAbsolute K (i.comp j))

theorem

openSubgroupOfFiniteExtensionSup_eq_range_inf

L1415 ↗

RamificationTheory.Field.absoluteGaloisGroup.openSubgroupOfFiniteExtensionSup_eq_range_inf

Documentation

States the theorem openSubgroupOfFiniteExtensionSup_eq_range_inf.

Source context 14 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
section TwoFiniteExtensions
variable {M : Type w} [Field M] [Algebra K M]

Lean source · statement

theorem openSubgroupOfFiniteExtensionSup_eq_range_inf
    [FiniteDimensional K L] [FiniteDimensional K M]
    (iL : L →ₐ[K] AlgebraicClosure K)
    (iM : M →ₐ[K] AlgebraicClosure K) :
    (openSubgroupOfFiniteExtensionSup K iL iM :
      Subgroup (Field.absoluteGaloisGroup K)) =
      MonoidHom.range (ofFiniteExtensionAbsolute K iL) ⊓
        MonoidHom.range (ofFiniteExtensionAbsolute K iM)

theorem

mem_range_ofFiniteExtensionAbsolute_inf_iff

L1427 ↗

RamificationTheory.Field.absoluteGaloisGroup.mem_range_ofFiniteExtensionAbsolute_inf_iff

Documentation

States the theorem mem_range_ofFiniteExtensionAbsolute_inf_iff.

Source context 14 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
section TwoFiniteExtensions
variable {M : Type w} [Field M] [Algebra K M]

Lean source · full declaration

theorem mem_range_ofFiniteExtensionAbsolute_inf_iff
    [FiniteDimensional K L] [FiniteDimensional K M]
    (iL : L →ₐ[K] AlgebraicClosure K)
    (iM : M →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup K) :
    σ ∈ MonoidHom.range (ofFiniteExtensionAbsolute K iL) ⊓
        MonoidHom.range (ofFiniteExtensionAbsolute K iM) ↔
      (∀ x : L, (show Gal(AlgebraicClosure K / K) from σ) (iL x) = iL x) ∧
        ∀ y : M, (show Gal(AlgebraicClosure K / K) from σ) (iM y) = iM y := by
  rw [← openSubgroupOfFiniteExtensionSup_eq_range_inf]
  change
    σ ∈ openSubgroupOfFiniteExtensionSup K iL iM ↔
      (∀ x : L, (show Gal(AlgebraicClosure K / K) from σ) (iL x) = iL x) ∧
        ∀ y : M, (show Gal(AlgebraicClosure K / K) from σ) (iM y) = iM y
  exact mem_openSubgroupOfFiniteExtensionSup_iff_forall_apply_eq K iL iM σ

theorem

mem_range_ofFiniteExtensionAbsolute_iff_forall_apply_eq

L1446 ↗

RamificationTheory.Field.absoluteGaloisGroup.mem_range_ofFiniteExtensionAbsolute_iff_forall_apply_eq

Documentation

Concrete range criterion for the identified inclusion G_L → G_K.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · full declaration

theorem mem_range_ofFiniteExtensionAbsolute_iff_forall_apply_eq
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup K) :
    σ ∈ MonoidHom.range (ofFiniteExtensionAbsolute K i) ↔
      ∀ x : L, (show Gal(AlgebraicClosure K / K) from σ) (i x) = i x := by
  rw [range_ofFiniteExtensionAbsolute_eq_fixingSubgroupOfExtension]
  rfl

theorem

ofFiniteExtensionAbsolute_apply_embedding

L1456 ↗

RamificationTheory.Field.absoluteGaloisGroup.ofFiniteExtensionAbsolute_apply_embedding

Documentation

States the theorem ofFiniteExtensionAbsolute_apply_embedding.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · full declaration

theorem ofFiniteExtensionAbsolute_apply_embedding
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup L) (x : L) :
    (show Gal(AlgebraicClosure K / K) from
      ofFiniteExtensionAbsolute K i σ) (i x) = i x := by
  exact (mem_openSubgroupOfFiniteExtension_iff_forall_apply_eq K i
    (ofFiniteExtensionAbsolute K i σ)).1
      (ofFiniteExtensionAbsolute_mem_openSubgroup K i σ) x

theorem

coe_toOpenSubgroupOfFiniteExtension_apply_embedding

L1467 ↗

RamificationTheory.Field.absoluteGaloisGroup.coe_toOpenSubgroupOfFiniteExtension_apply_embedding

Documentation

States the theorem coe_toOpenSubgroupOfFiniteExtension_apply_embedding.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · full declaration

theorem coe_toOpenSubgroupOfFiniteExtension_apply_embedding
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup L) (x : L) :
    (show Gal(AlgebraicClosure K / K) from
      ((toOpenSubgroupOfFiniteExtension K i σ :
        openSubgroupOfFiniteExtension K i) :
        Field.absoluteGaloisGroup K)) (i x) = i x := by
  simpa [ofFiniteExtensionAbsolute_apply]
    using ofFiniteExtensionAbsolute_apply_embedding K i σ x

theorem

exists_ofFiniteExtensionAbsolute_eq_iff_mem_openSubgroup

L1478 ↗

RamificationTheory.Field.absoluteGaloisGroup.exists_ofFiniteExtensionAbsolute_eq_iff_mem_openSubgroup

Documentation

States the theorem exists_ofFiniteExtensionAbsolute_eq_iff_mem_openSubgroup.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem exists_ofFiniteExtensionAbsolute_eq_iff_mem_openSubgroup
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup K) :
    (∃ τ : Field.absoluteGaloisGroup L,
      ofFiniteExtensionAbsolute K i τ = σ) ↔
      σ ∈ openSubgroupOfFiniteExtension K i

theorem

ofFiniteExtensionAbsolute_equivOpenSubgroupOfFiniteExtension_symm

L1489 ↗

RamificationTheory.Field.absoluteGaloisGroup.ofFiniteExtensionAbsolute_equivOpenSubgroupOfFiniteExtension_symm

Documentation

States the theorem ofFiniteExtensionAbsolute_equivOpenSubgroupOfFiniteExtension_symm.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem ofFiniteExtensionAbsolute_equivOpenSubgroupOfFiniteExtension_symm
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K)
    (σ : openSubgroupOfFiniteExtension K i) :
    ofFiniteExtensionAbsolute K i
        ((equivOpenSubgroupOfFiniteExtension K i).symm σ) =
      (σ : Field.absoluteGaloisGroup K)

def

ofFiniteExtensionAbsoluteTower

L1505 ↗

RamificationTheory.Field.absoluteGaloisGroup.ofFiniteExtensionAbsoluteTower

Documentation

The tower restriction map G_M -> G_L induced by embeddings L -> M -> K^al, constructed through the concrete open-subgroup identifications inside G_K.

Source context 14 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
section TwoFiniteExtensionsTower
variable {M : Type w} [Field M] [Algebra K M]

Lean source · statement

def ofFiniteExtensionAbsoluteTower
    [FiniteDimensional K L] [FiniteDimensional K M]
    (i : M →ₐ[K] AlgebraicClosure K) (j : L →ₐ[K] M) :
    Field.absoluteGaloisGroup M →* Field.absoluteGaloisGroup L

theorem

ofFiniteExtensionAbsoluteTower_naturality

L1532 ↗

RamificationTheory.Field.absoluteGaloisGroup.ofFiniteExtensionAbsoluteTower_naturality

Documentation

The tower map is natural with respect to the concrete inclusions into G_K: the inclusion G_L -> G_K after G_M -> G_L is the inclusion G_M -> G_K.

Source context 14 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
section TwoFiniteExtensionsTower
variable {M : Type w} [Field M] [Algebra K M]

Lean source · statement

theorem ofFiniteExtensionAbsoluteTower_naturality
    [FiniteDimensional K L] [FiniteDimensional K M]
    (i : M →ₐ[K] AlgebraicClosure K) (j : L →ₐ[K] M)
    (σ : Field.absoluteGaloisGroup M) :
    ofFiniteExtensionAbsolute K (i.comp j)
        (ofFiniteExtensionAbsoluteTower K i j σ) =
      ofFiniteExtensionAbsolute K i σ

theorem

ofFiniteExtensionAbsoluteTower_injective

L1556 ↗

RamificationTheory.Field.absoluteGaloisGroup.ofFiniteExtensionAbsoluteTower_injective

Documentation

The tower map G_M -> G_L is injective.

Source context 14 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
section TwoFiniteExtensionsTower
variable {M : Type w} [Field M] [Algebra K M]

Lean source · statement

theorem ofFiniteExtensionAbsoluteTower_injective
    [FiniteDimensional K L] [FiniteDimensional K M]
    (i : M →ₐ[K] AlgebraicClosure K) (j : L →ₐ[K] M) :
    Function.Injective (ofFiniteExtensionAbsoluteTower K i j)

theorem

map_top_ofFiniteExtensionAbsoluteTower_eq_comap_range

L1567 ↗

RamificationTheory.Field.absoluteGaloisGroup.map_top_ofFiniteExtensionAbsoluteTower_eq_comap_range

Documentation

The image of the tower map G_M -> G_L is the pullback, along G_L -> G_K, of the image of G_M -> G_K.

Source context 14 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
section TwoFiniteExtensionsTower
variable {M : Type w} [Field M] [Algebra K M]

Lean source · statement

theorem map_top_ofFiniteExtensionAbsoluteTower_eq_comap_range
    [FiniteDimensional K L] [FiniteDimensional K M]
    (i : M →ₐ[K] AlgebraicClosure K) (j : L →ₐ[K] M) :
    Subgroup.map (ofFiniteExtensionAbsoluteTower K i j) ⊤ =
      Subgroup.comap (ofFiniteExtensionAbsolute K (i.comp j))
        (MonoidHom.range (ofFiniteExtensionAbsolute K i))

theorem

existsUnique_ofFiniteExtensionAbsolute_eq_of_mem_openSubgroup

L1590 ↗

RamificationTheory.Field.absoluteGaloisGroup.existsUnique_ofFiniteExtensionAbsolute_eq_of_mem_openSubgroup

Documentation

Elements of the finite-extension open subgroup of G_K have a unique preimage in the identified absolute Galois group G_L.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · statement

theorem existsUnique_ofFiniteExtensionAbsolute_eq_of_mem_openSubgroup
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup K)
    (hσ : σ ∈ openSubgroupOfFiniteExtension K i) :
    ∃! τ : Field.absoluteGaloisGroup L,
      ofFiniteExtensionAbsolute K i τ = σ

theorem

existsUnique_ofFiniteExtensionAbsolute_eq_iff_forall_apply_eq

L1606 ↗

RamificationTheory.Field.absoluteGaloisGroup.existsUnique_ofFiniteExtensionAbsolute_eq_iff_forall_apply_eq

Documentation

Concrete unique-preimage criterion for the identified inclusion G_L → G_K.

Source context 12 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]
section FiniteExtension
variable {L : Type v} [Field L] [Algebra K L]
local instance fieldRangeIsScalarTower
    (i : L →ₐ[K] AlgebraicClosure K) :
    IsScalarTower K (AlgHom.fieldRange i) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Lean source · full declaration

theorem existsUnique_ofFiniteExtensionAbsolute_eq_iff_forall_apply_eq
    [FiniteDimensional K L] (i : L →ₐ[K] AlgebraicClosure K)
    (σ : Field.absoluteGaloisGroup K) :
    (∃! τ : Field.absoluteGaloisGroup L,
      ofFiniteExtensionAbsolute K i τ = σ) ↔
      ∀ x : L, (show Gal(AlgebraicClosure K / K) from σ) (i x) = i x := by
  constructor
  · rintro ⟨τ, hτ, _⟩ x
    rw [← hτ]
    exact ofFiniteExtensionAbsolute_apply_embedding K i τ x
  · intro hσ
    exact existsUnique_ofFiniteExtensionAbsolute_eq_of_mem_openSubgroup K i σ
      ((mem_openSubgroupOfFiniteExtension_iff_forall_apply_eq K i σ).2 hσ)

theorem

mem_absoluteValuationSubring_iff_apply_mem_of_finite_separable_intermediate

L1634 ↗

RamificationTheory.DiscreteValuationField.HenselianDVF.mem_absoluteValuationSubring_iff_apply_mem_of_finite_separable_intermediate

Documentation

Finite-level membership preservation for the absolute valuation subring, exposed from the Henselian-DVF namespace. The finite-level Henselian-DVF target and unique-extension proof are explicit; this is the non-dummy wrapper used by the absolute power route.

Source context 7 commands

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

namespace RamificationTheory
open ValuationTheory
noncomputable section
universe u v w z
namespace DiscreteValuationField
namespace HenselianDVF
variable {K : Type u} [Field K]

Lean source · full declaration

theorem mem_absoluteValuationSubring_iff_apply_mem_of_finite_separable_intermediate
    (F : ValuationTheory.DiscreteValuationField.HenselianDVF.{u, v} K)
    (A : ValuationSubring (AlgebraicClosure K))
    [_root_.Valuation.HasExtension F.valuation A.valuation]
    (E : IntermediateField K (AlgebraicClosure K))
    [FiniteDimensional K E] [Algebra.IsSeparable K E]
    (target : ValuationTheory.DiscreteValuationField.HenselianDVF.{u, w} E)
    (hA : target.valuation.valuationSubring =
      (RamificationTheory.ValuationSubring.restrictIntermediateField A E))
    (huniq :
      ValuationTheory.DiscreteValuationField.HenselianDVF.HasUniqueValuationExtension.{u, v, u,
        w, u}
        F target)
    (sigma : Field.absoluteGaloisGroup K) (x : E) :
    ((x : AlgebraicClosure K) ∈ A) ↔
      (show Gal(AlgebraicClosure K / K) from sigma) (x : AlgebraicClosure K) ∈ A :=
  (open RamificationTheory.Field.absoluteGaloisGroup in
    valuationSubring_mem_preserved_on_finite_separable_intermediate
      (K := K) F A E target hA huniq sigma x)

Module documentation

Declarations