ModuleFixedSubgroupConjugation.lean
Nyll.GaloisCohomology.Kummer.Concrete.FixedSubgroupConjugation
5 declarations indexed from sourceView source ↗ Module documentation
Conjugation on a normal intermediate field's fixing subgroup
Restriction supplies the base map of an ambient automorphism. The fixing subgroup equivalence intertwines its actual subgroup conjugation with that semilinear conjugation, and therefore intertwines their abelianized actions.
Declarations
KummerTheory.fixingSubgroup_normal
DocumentationThe fixing subgroup of a normal intermediate field is the normal kernel of restriction, even without normality of the ambient extension.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open ProCGroups.Abelian
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
(L : IntermediateField K Ω) [Normal K L]
KummerTheory.fixingSubgroupNormal
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open ProCGroups.Abelian
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
(L : IntermediateField K Ω) [Normal K L]
KummerTheory.galois_restrictNormal_algebraMap
DocumentationAn ambient Galois automorphism is a semilinear lift of its restriction.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open ProCGroups.Abelian
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
(L : IntermediateField K Ω) [Normal K L]
local instance fixingSubgroupNormal : L.fixingSubgroup.Normal := fixingSubgroup_normal L
KummerTheory.fixingSubgroupEquiv_conjNormal
DocumentationThe relative Galois identification intertwines subgroup conjugation with semilinear conjugation by the actual ambient representative.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open ProCGroups.Abelian
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
(L : IntermediateField K Ω) [Normal K L]
local instance fixingSubgroupNormal : L.fixingSubgroup.Normal := fixingSubgroup_normal L
KummerTheory.fixingSubgroupAbelianization_conjugation
DocumentationOn topological abelianizations, the actual quotient conjugation agrees with semilinear conjugation under the continuous fixing subgroup equivalence.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open ProCGroups.Abelian
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
(L : IntermediateField K Ω) [Normal K L]
local instance fixingSubgroupNormal : L.fixingSubgroup.Normal := fixingSubgroup_normal L
variable [FiniteDimensional K L] [Algebra.IsAlgebraic L Ω]