NYLL
Module

SlimFieldExtensions.lean

Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SlimFieldExtensions
2 declarations indexed from sourceView source ↗

Module documentation

Slimness and centers under finite field extension

Slimness is preserved by continuous group isomorphisms. A finite extension of a field with slim absolute Galois group has center-free absolute Galois group.

Imports2
Imported by2

Declarations

theorem

isSlim_of_continuousMulEquiv

L25 ↗
Yamaguchi26AbfaithfulGalois.isSlim_of_continuousMulEquiv
Documentation

Slimness is preserved by a continuous group isomorphism.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.FiniteStepSolvableQuotients
universe u v
Lean source · statement
theorem isSlim_of_continuousMulEquiv
    {G : Type u} {H : Type v} [Group G] [Group H]
    [TopologicalSpace G] [TopologicalSpace H]
    (e : G ≃ₜ* H) (hG : IsSlim G) : IsSlim H
theorem

center_eq_bot_absoluteGaloisGroup_of_finiteExtension_of_isSlim

L42 ↗
Yamaguchi26AbfaithfulGalois.center_eq_bot_absoluteGaloisGroup_of_finiteExtension_of_isSlim
Documentation

Slimness of the lower absolute Galois group makes the upper absolute Galois group center-free for every finite extension.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.FiniteStepSolvableQuotients
universe u v
Lean source · statement
theorem center_eq_bot_absoluteGaloisGroup_of_finiteExtension_of_isSlim
    {K : Type u} {E : Type v} [Field K] [Field E] [Algebra K E]
    [FiniteDimensional K E]
    (hK : IsSlim Gal(AlgebraicClosure K/K)) :
    Subgroup.center Gal(AlgebraicClosure E/E) = ⊥

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