ModuleFiniteUnramifiedTower.lean
Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.FiniteUnramifiedTower
5 declarations indexed from sourceView source ↗ Module documentation
Finite-prime unramifiedness in towers of number fields
This file records the tower properties of being unramified at every finite prime. The transitivity and intermediate-field arguments are proved from multiplicativity of ramification indices.
Declarations
DocumentationA number-field extension is unramified at finite places when every height-one prime of the top ring of integers is unramified over the base ring of integers.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
attribute [local instance] Ideal.Quotient.field
universe u v w
IsUnramifiedAtFinitePlaces.refl
DocumentationThe identity extension is unramified at every finite place.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
attribute [local instance] Ideal.Quotient.field
universe u v w
namespace IsUnramifiedAtFinitePlaces
IsUnramifiedAtFinitePlaces.trans
DocumentationFinite-prime unramifiedness is transitive in a tower of number fields.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
attribute [local instance] Ideal.Quotient.field
universe u v w
namespace IsUnramifiedAtFinitePlaces
variable
{k : Type u} {K : Type v} {F : Type w}
[Field k] [NumberField k]
[Field K] [NumberField K]
[Field F] [NumberField F]
[Algebra k K] [Algebra k F] [Algebra K F]
[IsScalarTower k K F]
IsUnramifiedAtFinitePlaces.top
DocumentationIf the top of a number-field tower is unramified over the bottom, then it is unramified over the intermediate field.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
attribute [local instance] Ideal.Quotient.field
universe u v w
namespace IsUnramifiedAtFinitePlaces
variable
{k : Type u} {K : Type v} {F : Type w}
[Field k] [NumberField k]
[Field K] [NumberField K]
[Field F] [NumberField F]
[Algebra k K] [Algebra k F] [Algebra K F]
[IsScalarTower k K F]
IsUnramifiedAtFinitePlaces.bot
DocumentationIf the top of a number-field tower is unramified over the bottom, then the intermediate field is unramified over the bottom.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
attribute [local instance] Ideal.Quotient.field
universe u v w
namespace IsUnramifiedAtFinitePlaces
variable
{k : Type u} {K : Type v} {F : Type w}
[Field k] [NumberField k]
[Field K] [NumberField K]
[Field F] [NumberField F]
[Algebra k K] [Algebra k F] [Algebra K F]
[IsScalarTower k K F]