ModuleUnramifiedCompositumBaseChange.lean
Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.UnramifiedCompositumBaseChange
4 declarations indexed from sourceView source ↗ Module documentation
Unramified composita over a changed base
If the images of A and B generate M over K, restriction embeds Gal(M/B) into Gal(A/K). Inertia restricts into the inertia of A/K. Consequently unramifiedness of A/K gives unramifiedness of M/B; B/K need not be unramified. The same injection preserves the p-group condition, and odd p supplies the infinite-place condition. The generating-range equality is supplied by the concrete compositum construction at the application.
Declarations
ClassFieldTower.Martinet.compositumBaseChange_restriction_injective
DocumentationRestriction is injective when the two field images generate the top.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open NumberField
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet
variable (K A B M : Type) [Field K] [Field A] [Field B] [Field M]
variable [Algebra K A] [Algebra K B] [Algebra K M] [Algebra A M] [Algebra B M]
variable [IsScalarTower K A M] [IsScalarTower K B M] [IsGalois K A]
local notation "RA" => AlgHom.fieldRange (IsScalarTower.toAlgHom K A M)
local notation "RB" => AlgHom.fieldRange (IsScalarTower.toAlgHom K B M)
ClassFieldTower.Martinet.compositumBaseChange_isPGroup
DocumentationA p-group Galois extension remains a p-group extension under base change.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open NumberField
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet
variable (K A B M : Type) [Field K] [Field A] [Field B] [Field M]
variable [Algebra K A] [Algebra K B] [Algebra K M] [Algebra A M] [Algebra B M]
variable [IsScalarTower K A M] [IsScalarTower K B M] [IsGalois K A]
local notation "RA" => AlgHom.fieldRange (IsScalarTower.toAlgHom K A M)
local notation "RB" => AlgHom.fieldRange (IsScalarTower.toAlgHom K B M)
ClassFieldTower.Martinet.compositumBaseChange_finitePlaceUnramifiedness
DocumentationFinite-place unramifiedness survives base change, by restriction of actual ideal inertia. No unramifiedness of the new base is assumed.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open NumberField
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet
variable (K A B M : Type) [Field K] [Field A] [Field B] [Field M]
variable [Algebra K A] [Algebra K B] [Algebra K M] [Algebra A M] [Algebra B M]
variable [IsScalarTower K A M] [IsScalarTower K B M] [IsGalois K A]
local notation "RA" => AlgHom.fieldRange (IsScalarTower.toAlgHom K A M)
local notation "RB" => AlgHom.fieldRange (IsScalarTower.toAlgHom K B M)
variable [NumberField K] [NumberField A] [NumberField B] [NumberField M]
variable [FiniteDimensional K A] [FiniteDimensional B M] [IsGalois B M]
ClassFieldTower.Martinet.compositumBaseChange_everywhereUnramified
DocumentationThe base change of an unramified odd-p Galois extension is everywhere unramified, including at infinity.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open NumberField
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet
variable (K A B M : Type) [Field K] [Field A] [Field B] [Field M]
variable [Algebra K A] [Algebra K B] [Algebra K M] [Algebra A M] [Algebra B M]
variable [IsScalarTower K A M] [IsScalarTower K B M] [IsGalois K A]
local notation "RA" => AlgHom.fieldRange (IsScalarTower.toAlgHom K A M)
local notation "RB" => AlgHom.fieldRange (IsScalarTower.toAlgHom K B M)
variable [NumberField K] [NumberField A] [NumberField B] [NumberField M]
variable [FiniteDimensional K A] [FiniteDimensional B M] [IsGalois B M]