ModuleFiniteIntermediateAbsoluteClosure.lean
Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.FiniteIntermediateAbsoluteClosure
2 declarations indexed from sourceView source ↗ Module documentation
The closure equivalence underlying finite-extension absolute restriction
For an actual finite intermediate field, the canonical algebraic-closure equivalence is exactly the choice used by the existing absolute Galois inclusion. This evaluation identity lets finite base changes use the same closure without an additional comparison hypothesis.
Declarations
ClassFieldTower.Martinet.Shafarevich.finiteIntermediateAbsoluteClosureEquiv
DocumentationThe algebraic-closure equivalence used in the actual finite-extension absolute Galois inclusion. Both added instances are proposition-valued.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RamificationTheory.Field.absoluteGaloisGroup
variable (F : Type) [Field F]
variable (C : IntermediateField F (AlgebraicClosure F)) [FiniteDimensional F C]
ClassFieldTower.Martinet.Shafarevich.finiteIntermediateAbsoluteGaloisInclusion_apply
DocumentationActual absolute restriction acts by conjugation with this same closure equivalence; the compatibility is definitional.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RamificationTheory.Field.absoluteGaloisGroup
variable (F : Type) [Field F]
variable (C : IntermediateField F (AlgebraicClosure F)) [FiniteDimensional F C]