ModuleIdeleClassDirectLimitFiniteTowerNormProof.lean
Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.IdeleClassDirectLimitFiniteTowerNormProof
60 declarations indexed from sourceView source ↗ Declarations
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerRestrictedNormal
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerRestrictedUpper
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerLowerFiniteDimensional
Source context 16 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerUpperFiniteDimensional
Source context 17 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerLowerUpperScalarTower
Source context 18 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerUpperAbsoluteFiniteDimensional
Source context 19 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerRestrictedUpperFiniteDimensional
Source context 20 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerLowerNumberField
Source context 21 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerUpperNumberField
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerUpperSeparableClosureScalarTower
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTower_lower_le_upper
Source context 25 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
omit hKfinite hfinite in
GlobalClassFieldTheory.Reciprocity.rationalFiniteTower_upper_le_normal
Source context 25 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
omit hKfinite hfinite in
GlobalClassFieldTheory.Reciprocity.rationalFiniteTower_lower_le_normal
Source context 25 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
omit hKfinite hfinite in
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerNormalScalarTower
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerNormalFiniteDimensional
Source context 25 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerNormalAbsoluteFiniteDimensional
Source context 26 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerNormalNumberField
Source context 27 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerRestrictedNormalFiniteDimensional
Source context 28 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTower_normal_le_rationalNormalClosure
Source context 29 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
GlobalClassFieldTheory.Reciprocity.rationalFiniteTower_lower_le_rationalNormalClosure
Source context 29 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
GlobalClassFieldTheory.Reciprocity.rationalFiniteTower_upper_le_rationalNormalClosure
Source context 29 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerRationalNormalClosureLowerAlgebra
Source context 29 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerRationalNormalClosureUpperAlgebra
Source context 30 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerRationalNormalClosureNormalAlgebra
Source context 31 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerRationalNormalClosureLowerScalarTower
Source context 32 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerRationalNormalClosureUpperScalarTower
Source context 33 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerRationalNormalClosureNormalScalarTower
Source context 34 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerLowerUpperClosureScalarTower
Source context 35 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerLowerNormalClosureScalarTower
Source context 36 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerClosureSeparableClosureScalarTower
Source context 37 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerClosureOverUpperFiniteDimensional
Source context 38 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerClosureOverLowerFiniteDimensional
Source context 39 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerClosureOverNormalFiniteDimensional
Source context 40 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerLowerSeparableClosureGalois
Source context 41 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerNormalGalois
Source context 42 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerClosureOverLowerGalois
Source context 43 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerClosureOverNormalGalois
Source context 44 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerQuotientFintype
Source context 45 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerCosetEquiv
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerNormalInclusion
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerUpperInclusion
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerRelativeClass
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerRationalRelativeClass
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerEmbeddedClass
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerCoset_comp_normalInclusion
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTower_restrictedEmbedding
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTower_representativeAction
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalRelativeFixedFieldCosetActionPointwise
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTower_product_embeddedClass
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerNormalInclusion_eq_toAlgHom
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTowerLowerInclusion_eq_toAlgHom
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTower_ideleClassExtension_comp_apply
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTower_baseChange_classInclusion
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTower_baseChange_normalInclusion_classInclusion
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTower_directLimit_ideleClassExtension
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTower_relativeClassNorm_eq_ordinaryNorm
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTower_directLimit_extension_eq_norm
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalFiniteTower_product_embeddings_eq_norm
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalAbstractRelativeFixedFieldNormCore
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀
GlobalClassFieldTheory.Reciprocity.rationalAbstractRelativeFixedFieldIdeleClassEquivFixed_relativeNorm_ofFiniteTower
DocumentationThe abstract relative norm agrees with the ordinary idèle-class norm for every finite tower of rational fixed fields.
Source context 46 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
section RationalFiniteTower
variable
(K L : ClosedSubgroup
(SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hKfinite : Finite (rationalFixedFieldAbsoluteQuotient K)]
[hfinite : Finite
(rationalFixedFieldRelativeQuotient K L hLK)]
local notation "F₀" =>
abstractFixedField ℚ (SeparableClosure ℚ) K
local notation "E₀" =>
abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
local notation "N₀" =>
IntermediateField.normalClosure F₀ E₀ (SeparableClosure ℚ)
local notation "EQ₀" =>
rationalFiniteTowerRestrictedUpper K L hLK
local notation "NQ₀" =>
rationalFiniteTowerRestrictedNormal K L hLK
local notation "U₀" => rationalNormalClosure NQ₀
local notation "Q₀" =>
K.toSubgroup ⧸ extensionSubgroup K L hLK
noncomputable local instance rationalFiniteTowerLowerFiniteDimensional :
FiniteDimensional ℚ F₀ :=
abstractFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K hKfinite
noncomputable local instance rationalFiniteTowerUpperFiniteDimensional :
FiniteDimensional F₀ E₀ :=
abstractRelativeFixedField_finiteDimensional
ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
local instance rationalFiniteTowerLowerUpperScalarTower :
IsScalarTower ℚ F₀ E₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerUpperAbsoluteFiniteDimensional :
FiniteDimensional ℚ E₀ :=
FiniteDimensional.trans ℚ F₀ E₀
noncomputable local instance rationalFiniteTowerRestrictedUpperFiniteDimensional :
FiniteDimensional ℚ EQ₀ := by
change FiniteDimensional ℚ E₀
infer_instance
noncomputable local instance rationalFiniteTowerLowerNumberField :
NumberField F₀ :=
NumberField.of_module_finite ℚ F₀
noncomputable local instance rationalFiniteTowerUpperNumberField :
NumberField E₀ :=
NumberField.of_module_finite ℚ E₀
local instance rationalFiniteTowerUpperSeparableClosureScalarTower :
IsScalarTower F₀ E₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerNormalScalarTower :
IsScalarTower ℚ F₀ N₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance rationalFiniteTowerNormalFiniteDimensional :
FiniteDimensional F₀ N₀ :=
normalClosure.is_finiteDimensional F₀ E₀ (SeparableClosure ℚ)
noncomputable local instance rationalFiniteTowerNormalAbsoluteFiniteDimensional :
FiniteDimensional ℚ N₀ :=
FiniteDimensional.trans ℚ F₀ N₀
noncomputable local instance rationalFiniteTowerNormalNumberField :
NumberField N₀ :=
NumberField.of_module_finite ℚ N₀
noncomputable local instance rationalFiniteTowerRestrictedNormalFiniteDimensional :
FiniteDimensional ℚ NQ₀ := by
change FiniteDimensional ℚ N₀
infer_instance
local instance rationalFiniteTowerRationalNormalClosureLowerAlgebra :
Algebra F₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_lower_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureUpperAlgebra :
Algebra E₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_upper_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureNormalAlgebra :
Algebra N₀ U₀ :=
(IntermediateField.inclusion
(rationalFiniteTower_normal_le_rationalNormalClosure K L hLK)).toRingHom.toAlgebra
local instance rationalFiniteTowerRationalNormalClosureLowerScalarTower :
IsScalarTower ℚ F₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureUpperScalarTower :
IsScalarTower ℚ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerRationalNormalClosureNormalScalarTower :
IsScalarTower ℚ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
local instance rationalFiniteTowerLowerUpperClosureScalarTower :
IsScalarTower F₀ E₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerLowerNormalClosureScalarTower :
IsScalarTower F₀ N₀ U₀ :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
local instance rationalFiniteTowerClosureSeparableClosureScalarTower :
IsScalarTower F₀ U₀ (SeparableClosure ℚ) :=
IsScalarTower.of_algebraMap_eq' (by
ext x
rfl)
noncomputable local instance rationalFiniteTowerClosureOverUpperFiniteDimensional :
FiniteDimensional E₀ U₀ :=
FiniteDimensional.right ℚ E₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverLowerFiniteDimensional :
FiniteDimensional F₀ U₀ :=
FiniteDimensional.right ℚ F₀ U₀
noncomputable local instance rationalFiniteTowerClosureOverNormalFiniteDimensional :
FiniteDimensional N₀ U₀ :=
FiniteDimensional.right ℚ N₀ U₀
local instance rationalFiniteTowerLowerSeparableClosureGalois :
IsGalois F₀ (SeparableClosure ℚ) :=
IsGalois.tower_top_of_isGalois ℚ F₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerNormalGalois : IsGalois F₀ N₀ :=
IsGalois.normalClosure F₀ E₀ (SeparableClosure ℚ)
local instance rationalFiniteTowerClosureOverLowerGalois : IsGalois F₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ F₀ U₀
local instance rationalFiniteTowerClosureOverNormalGalois : IsGalois N₀ U₀ :=
IsGalois.tower_top_of_isGalois ℚ N₀ U₀
noncomputable local instance rationalFiniteTowerQuotientFintype : Fintype Q₀ :=
Fintype.ofFinite Q₀