NYLL
Module

MathlibAbsoluteGaloisBaseEquiv.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Galois.MathlibAbsoluteGaloisBaseEquiv
6 declarations indexed from sourceView source ↗

Module documentation

Absolute Galois groups under an equivalence of base fields

A field equivalence extends to an equivalence of the chosen algebraic closures. Conjugation then identifies the absolute Galois groups, including their Krull topologies, and hence their topological abelianizations.

Imports3
Imported by2

Declarations

theorem

semilinear_symm_algebraMap

L29 ↗
ClassFieldTheory.semilinear_symm_algebraMap
Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v w z
variable {K : Type u} {M : Type v} {Ω : Type w} {Ψ : Type z}
  [Field K] [Field M] [Field Ω] [Field Ψ]
  [Algebra K Ω] [Algebra M Ψ]
Lean source · statement
theorem semilinear_symm_algebraMap (e : K ≃+* M) (E : Ω ≃+* Ψ)
    (hE : ∀ x : K, E (algebraMap K Ω x) = algebraMap M Ψ (e x))
    (y : M) :
    E.symm (algebraMap M Ψ y) = algebraMap K Ω (e.symm y)
def

semilinearGaloisConjugate

L36 ↗
ClassFieldTheory.semilinearGaloisConjugate
Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v w z
variable {K : Type u} {M : Type v} {Ω : Type w} {Ψ : Type z}
  [Field K] [Field M] [Field Ω] [Field Ψ]
  [Algebra K Ω] [Algebra M Ψ]
Lean source · full declaration
def semilinearGaloisConjugate (e : K ≃+* M) (E : Ω ≃+* Ψ)
    (hE : ∀ x : K, E (algebraMap K Ω x) = algebraMap M Ψ (e x))
    (σ : Gal(Ω/K)) : Gal(Ψ/M) where
  toRingEquiv := (E.symm.trans σ.toRingEquiv).trans E
  commutes' := by
    intro y
    change E (σ (E.symm (algebraMap M Ψ y))) = algebraMap M Ψ y
    rw [semilinear_symm_algebraMap e E hE y, σ.commutes, hE,
      e.apply_symm_apply]
def

semilinearGaloisEquiv

L46 ↗
ClassFieldTheory.semilinearGaloisEquiv
Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v w z
variable {K : Type u} {M : Type v} {Ω : Type w} {Ψ : Type z}
  [Field K] [Field M] [Field Ω] [Field Ψ]
  [Algebra K Ω] [Algebra M Ψ]
Lean source · full declaration
def semilinearGaloisEquiv (e : K ≃+* M) (E : Ω ≃+* Ψ)
    (hE : ∀ x : K, E (algebraMap K Ω x) = algebraMap M Ψ (e x)) :
    Gal(Ω/K) ≃* Gal(Ψ/M) where
  toFun := semilinearGaloisConjugate e E hE
  invFun := semilinearGaloisConjugate e.symm E.symm
    (semilinear_symm_algebraMap e E hE)
  left_inv σ := by
    apply AlgEquiv.ext
    intro x
    simp [semilinearGaloisConjugate]
  right_inv σ := by
    apply AlgEquiv.ext
    intro x
    simp [semilinearGaloisConjugate]
  map_mul' σ τ := by
    apply AlgEquiv.ext
    intro x
    simp [semilinearGaloisConjugate, AlgEquiv.mul_apply]
def

semilinearGaloisContinuousEquiv

L65 ↗
ClassFieldTheory.semilinearGaloisContinuousEquiv
Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v w z
variable {K : Type u} {M : Type v} {Ω : Type w} {Ψ : Type z}
  [Field K] [Field M] [Field Ω] [Field Ψ]
  [Algebra K Ω] [Algebra M Ψ]
Lean source · full declaration
def semilinearGaloisContinuousEquiv (e : K ≃+* M) (E : Ω ≃+* Ψ)
    (hE : ∀ x : K, E (algebraMap K Ω x) = algebraMap M Ψ (e x)) :
    Gal(Ω/K) ≃ₜ* Gal(Ψ/M) where
  toMulEquiv := semilinearGaloisEquiv e E hE
  continuous_toFun :=
    RamificationTheory.Field.absoluteGaloisGroup.semilinear_conjugation_continuous
      e E hE (semilinearGaloisEquiv e E hE).toMonoidHom (by intro σ; rfl)
  continuous_invFun :=
    RamificationTheory.Field.absoluteGaloisGroup.semilinear_conjugation_continuous
      e.symm E.symm (semilinear_symm_algebraMap e E hE)
      (semilinearGaloisEquiv e.symm E.symm
        (semilinear_symm_algebraMap e E hE)).toMonoidHom (by intro σ; rfl)
def

absoluteGaloisGroupEquivOfRingEquiv

L80 ↗
ClassFieldTheory.absoluteGaloisGroupEquivOfRingEquiv
Documentation

A field equivalence identifies the Krull topological absolute Galois groups of its source and target fields.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v w z
variable {K : Type u} {M : Type v} {Ω : Type w} {Ψ : Type z}
  [Field K] [Field M] [Field Ω] [Field Ψ]
  [Algebra K Ω] [Algebra M Ψ]
Lean source · statement
def absoluteGaloisGroupEquivOfRingEquiv (e : K ≃+* M) :
    Field.absoluteGaloisGroup K ≃ₜ* Field.absoluteGaloisGroup M
def

absoluteGaloisGroupAbelianizationEquivOfRingEquiv

L88 ↗
ClassFieldTheory.absoluteGaloisGroupAbelianizationEquivOfRingEquiv
Documentation

The induced equivalence of Mathlib's topological abelianizations.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v w z
variable {K : Type u} {M : Type v} {Ω : Type w} {Ψ : Type z}
  [Field K] [Field M] [Field Ω] [Field Ψ]
  [Algebra K Ω] [Algebra M Ψ]
Lean source · statement
def absoluteGaloisGroupAbelianizationEquivOfRingEquiv
    (e : K ≃+* M) :
    Field.absoluteGaloisGroupAbelianization K ≃ₜ*
      Field.absoluteGaloisGroupAbelianization M

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