This file connects mathlib's Algebra.norm with the unit-group and valued-norm APIs used by local CFT.
The norm subgroup of Kˣ attached to L/K.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]def fieldNormSubgroup : Subgroup KˣThe norm subgroup from the top field of a tower lies in the norm subgroup from the intermediate field.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormSubgroup_le_of_tower
(E : Type w) [Field E] [Algebra K E] [Algebra E L] [IsScalarTower K E L]
[Module.Free E L] :
fieldNormSubgroup K L ≤ fieldNormSubgroup K ECharacterizes fieldNormSubgroup K L = ⊤ by the equivalent condition Function.Surjective (normUnits K L).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormSubgroup_eq_top_iff :
fieldNormSubgroup K L = ⊤ ↔ Function.Surjective (normUnits K L)Characterizes z ∈ MonoidHom.ker (normUnits K L) by the equivalent condition Algebra.norm K (z : L) = 1.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem mem_fieldNormUnits_ker_iff_norm_eq_one (z : Lˣ) :
z ∈ MonoidHom.ker (normUnits K L) ↔
Algebra.norm K (z : L) = 1First-isomorphism-theorem form for the field norm on unit groups: Lˣ / ker(N) is the norm subgroup of Kˣ.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]def fieldNormUnitsQuotientKerEquivFieldNormSubgroup :
Lˣ ⧸ MonoidHom.ker (normUnits K L) ≃*
fieldNormSubgroup K LEstablishes the identity fieldNormUnitsQuotientKerEquivFieldNormSubgroup K L (QuotientGroup.mk' (MonoidHom.ker (normUnits K L)) z) = (normUnits K L).rangeRestrict z.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormUnitsQuotientKerEquivFieldNormSubgroup_mk
(z : Lˣ) :
fieldNormUnitsQuotientKerEquivFieldNormSubgroup K L
(QuotientGroup.mk'
(MonoidHom.ker (normUnits K L)) z) =
(normUnits K L).rangeRestrict zEstablishes the identity ((fieldNormUnitsQuotientKerEquivFieldNormSubgroup K L (QuotientGroup.mk' (MonoidHom.ker (normUnits K L)) z) : fieldNormSubgroup K L) : Kˣ) = normUnits K L z.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem coe_fieldNormUnitsQuotientKerEquivFieldNormSubgroup_mk
(z : Lˣ) :
((fieldNormUnitsQuotientKerEquivFieldNormSubgroup K L
(QuotientGroup.mk'
(MonoidHom.ker (normUnits K L)) z) :
fieldNormSubgroup K L) : Kˣ) =
normUnits K L zThe quotient map Kˣ → Kˣ / N_{L/K}(Lˣ) attached to the field norm.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]def fieldNormQuotientMap :
Kˣ →* Kˣ ⧸ fieldNormSubgroup K LThe defining evaluation formula for fieldNormQuotientMap is fieldNormQuotientMap K L x = QuotientGroup.mk' (fieldNormSubgroup K L) x.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotientMap_apply (x : Kˣ) :
fieldNormQuotientMap K L x =
QuotientGroup.mk' (fieldNormSubgroup K L) xThe kernel of the norm quotient map is exactly the field-norm subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotientMap_ker :
MonoidHom.ker (fieldNormQuotientMap K L) = fieldNormSubgroup K LCharacterizes fieldNormQuotientMap K L x = 1 by the equivalent condition x ∈ fieldNormSubgroup K L.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotientMap_eq_one_iff (x : Kˣ) :
fieldNormQuotientMap K L x = 1 ↔
x ∈ fieldNormSubgroup K LCharacterizes fieldNormQuotientMap K L x = 1 by the equivalent condition ∃ z : Lˣ, normUnits K L z = x.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotientMap_eq_one_iff_exists_norm_eq (x : Kˣ) :
fieldNormQuotientMap K L x = 1 ↔
∃ z : Lˣ, normUnits K L z = xCharacterizes fieldNormQuotientMap K L x = fieldNormQuotientMap K L y by the equivalent condition x / y ∈ fieldNormSubgroup K L.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotientMap_eq_iff_div_mem (x y : Kˣ) :
fieldNormQuotientMap K L x = fieldNormQuotientMap K L y ↔
x / y ∈ fieldNormSubgroup K LCharacterizes x / y ∈ fieldNormSubgroup K L by the equivalent condition y⁻¹ * x ∈ fieldNormSubgroup K L.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormSubgroup_div_mem_iff_inv_mul_mem (x y : Kˣ) :
x / y ∈ fieldNormSubgroup K L ↔
y⁻¹ * x ∈ fieldNormSubgroup K LCharacterizes y⁻¹ * x ∈ fieldNormSubgroup K L by the equivalent condition x / y ∈ fieldNormSubgroup K L.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormSubgroup_inv_mul_mem_iff_div_mem (x y : Kˣ) :
y⁻¹ * x ∈ fieldNormSubgroup K L ↔
x / y ∈ fieldNormSubgroup K LCharacterizes x / y ∈ fieldNormSubgroup K L by the equivalent condition ∃ z : Lˣ, normUnits K L z * y = x.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormSubgroup_div_mem_iff_exists_norm_mul_eq
(x y : Kˣ) :
x / y ∈ fieldNormSubgroup K L ↔
∃ z : Lˣ, normUnits K L z * y = xCharacterizes y⁻¹ * x ∈ fieldNormSubgroup K L by the equivalent condition ∃ z : Lˣ, y * normUnits K L z = x.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormSubgroup_inv_mul_mem_iff_exists_mul_norm_eq
(x y : Kˣ) :
y⁻¹ * x ∈ fieldNormSubgroup K L ↔
∃ z : Lˣ, y * normUnits K L z = xCharacterizes QuotientGroup.mk' (fieldNormSubgroup K L) x = 1 by the equivalent condition x ∈ fieldNormSubgroup K L.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_eq_one_iff (x : Kˣ) :
QuotientGroup.mk' (fieldNormSubgroup K L) x = 1 ↔
x ∈ fieldNormSubgroup K LCharacterizes QuotientGroup.mk' (fieldNormSubgroup K L) x = 1 by the equivalent condition ∃ z : Lˣ, normUnits K L z = x.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_eq_one_iff_exists_norm_eq (x : Kˣ) :
QuotientGroup.mk' (fieldNormSubgroup K L) x = 1 ↔
∃ z : Lˣ, normUnits K L z = xEstablishes the identity QuotientGroup.mk' (fieldNormSubgroup K L) (normUnits K L z) = 1.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_norm_mk_eq_one (z : Lˣ) :
QuotientGroup.mk' (fieldNormSubgroup K L)
(normUnits K L z) = 1Characterizes (QuotientGroup.mk' (fieldNormSubgroup K L) x) ^ n = 1 by the equivalent condition x ^ n ∈ fieldNormSubgroup K L.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_pow_eq_one_iff_pow_mem
(x : Kˣ) (n : ℕ) :
(QuotientGroup.mk' (fieldNormSubgroup K L) x) ^ n = 1 ↔
x ^ n ∈ fieldNormSubgroup K LCharacterizes (QuotientGroup.mk' (fieldNormSubgroup K L) x) ^ n = 1 by the equivalent condition ∃ z : Lˣ, normUnits K L z = x ^ n.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_pow_eq_one_iff_exists_norm_eq_pow
(x : Kˣ) (n : ℕ) :
(QuotientGroup.mk' (fieldNormSubgroup K L) x) ^ n = 1 ↔
∃ z : Lˣ, normUnits K L z = x ^ nCharacterizes q ^ n = 1 by the equivalent condition ∃ x : Kˣ, QuotientGroup.mk' (fieldNormSubgroup K L) x = q ∧ x ^ n ∈ fieldNormSubgroup K L.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_pow_eq_one_iff_exists_pow_mem
(q : Kˣ ⧸ fieldNormSubgroup K L) (n : ℕ) :
q ^ n = 1 ↔
∃ x : Kˣ, QuotientGroup.mk' (fieldNormSubgroup K L) x = q ∧
x ^ n ∈ fieldNormSubgroup K LCharacterizes q ^ n = 1 by the equivalent condition ∃ x : Kˣ, QuotientGroup.mk' (fieldNormSubgroup K L) x = q ∧ ∃ z : Lˣ, normUnits K L z = x ^ n.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_pow_eq_one_iff_exists_norm_eq_pow
(q : Kˣ ⧸ fieldNormSubgroup K L) (n : ℕ) :
q ^ n = 1 ↔
∃ x : Kˣ, QuotientGroup.mk' (fieldNormSubgroup K L) x = q ∧
∃ z : Lˣ, normUnits K L z = x ^ nCharacterizes (QuotientGroup.mk' (fieldNormSubgroup K L) x) ^ n = 1 by the equivalent condition x ^ n ∈ fieldNormSubgroup K L.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_zpow_eq_one_iff_zpow_mem
(x : Kˣ) (n : ℤ) :
(QuotientGroup.mk' (fieldNormSubgroup K L) x) ^ n = 1 ↔
x ^ n ∈ fieldNormSubgroup K LCharacterizes (QuotientGroup.mk' (fieldNormSubgroup K L) x) ^ n = 1 by the equivalent condition ∃ z : Lˣ, normUnits K L z = x ^ n.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_zpow_eq_one_iff_exists_norm_eq_zpow
(x : Kˣ) (n : ℤ) :
(QuotientGroup.mk' (fieldNormSubgroup K L) x) ^ n = 1 ↔
∃ z : Lˣ, normUnits K L z = x ^ nCharacterizes q ^ n = 1 by the equivalent condition ∃ x : Kˣ, QuotientGroup.mk' (fieldNormSubgroup K L) x = q ∧ x ^ n ∈ fieldNormSubgroup K L.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_zpow_eq_one_iff_exists_zpow_mem
(q : Kˣ ⧸ fieldNormSubgroup K L) (n : ℤ) :
q ^ n = 1 ↔
∃ x : Kˣ, QuotientGroup.mk' (fieldNormSubgroup K L) x = q ∧
x ^ n ∈ fieldNormSubgroup K LCharacterizes q ^ n = 1 by the equivalent condition ∃ x : Kˣ, QuotientGroup.mk' (fieldNormSubgroup K L) x = q ∧ ∃ z : Lˣ, normUnits K L z = x ^ n.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_zpow_eq_one_iff_exists_norm_eq_zpow
(q : Kˣ ⧸ fieldNormSubgroup K L) (n : ℤ) :
q ^ n = 1 ↔
∃ x : Kˣ, QuotientGroup.mk' (fieldNormSubgroup K L) x = q ∧
∃ z : Lˣ, normUnits K L z = x ^ nCharacterizes QuotientGroup.mk' (fieldNormSubgroup K L) x = QuotientGroup.mk' (fieldNormSubgroup K L) y by the equivalent condition x / y ∈ fieldNormSubgroup K L.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_eq_iff_div_mem (x y : Kˣ) :
QuotientGroup.mk' (fieldNormSubgroup K L) x =
QuotientGroup.mk' (fieldNormSubgroup K L) y ↔
x / y ∈ fieldNormSubgroup K LCharacterizes QuotientGroup.mk' (fieldNormSubgroup K L) x = QuotientGroup.mk' (fieldNormSubgroup K L) y by the equivalent condition y⁻¹ * x ∈ fieldNormSubgroup K L.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_eq_iff_inv_mul_mem (x y : Kˣ) :
QuotientGroup.mk' (fieldNormSubgroup K L) x =
QuotientGroup.mk' (fieldNormSubgroup K L) y ↔
y⁻¹ * x ∈ fieldNormSubgroup K LCharacterizes QuotientGroup.mk' (fieldNormSubgroup K L) x = QuotientGroup.mk' (fieldNormSubgroup K L) y by the equivalent condition ∃ z : Lˣ, normUnits K L z = x / y.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_eq_iff_exists_norm_eq_div
(x y : Kˣ) :
QuotientGroup.mk' (fieldNormSubgroup K L) x =
QuotientGroup.mk' (fieldNormSubgroup K L) y ↔
∃ z : Lˣ, normUnits K L z = x / yCharacterizes QuotientGroup.mk' (fieldNormSubgroup K L) x = QuotientGroup.mk' (fieldNormSubgroup K L) y by the equivalent condition ∃ z : Lˣ, normUnits K L z = y⁻¹ * x.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_eq_iff_exists_norm_eq_inv_mul
(x y : Kˣ) :
QuotientGroup.mk' (fieldNormSubgroup K L) x =
QuotientGroup.mk' (fieldNormSubgroup K L) y ↔
∃ z : Lˣ, normUnits K L z = y⁻¹ * xCharacterizes QuotientGroup.mk' (fieldNormSubgroup K L) x = QuotientGroup.mk' (fieldNormSubgroup K L) y by the equivalent condition ∃ z : Lˣ, normUnits K L z * y = x.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_eq_iff_exists_norm_mul_eq (x y : Kˣ) :
QuotientGroup.mk' (fieldNormSubgroup K L) x =
QuotientGroup.mk' (fieldNormSubgroup K L) y ↔
∃ z : Lˣ, normUnits K L z * y = xCharacterizes QuotientGroup.mk' (fieldNormSubgroup K L) x = QuotientGroup.mk' (fieldNormSubgroup K L) y by the equivalent condition ∃ z : Lˣ, y * normUnits K L z = x.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_eq_iff_exists_mul_norm_eq (x y : Kˣ) :
QuotientGroup.mk' (fieldNormSubgroup K L) x =
QuotientGroup.mk' (fieldNormSubgroup K L) y ↔
∃ z : Lˣ, y * normUnits K L z = xEstablishes the identity QuotientGroup.mk' (fieldNormSubgroup K L) (normUnits K L z * x) = QuotientGroup.mk' (fieldNormSubgroup K L) x.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_norm_mul_mk_eq (z : Lˣ) (x : Kˣ) :
QuotientGroup.mk' (fieldNormSubgroup K L)
(normUnits K L z * x) =
QuotientGroup.mk' (fieldNormSubgroup K L) xEstablishes the identity QuotientGroup.mk' (fieldNormSubgroup K L) (x * normUnits K L z) = QuotientGroup.mk' (fieldNormSubgroup K L) x.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mul_norm_mk_eq (x : Kˣ) (z : Lˣ) :
QuotientGroup.mk' (fieldNormSubgroup K L)
(x * normUnits K L z) =
QuotientGroup.mk' (fieldNormSubgroup K L) xEstablishes the identity QuotientGroup.mk' (fieldNormSubgroup K L) x * QuotientGroup.mk' (fieldNormSubgroup K L) (normUnits K L z) = QuotientGroup.mk' (fieldNormSubgroup K L) x.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_mul_norm_eq (x : Kˣ) (z : Lˣ) :
QuotientGroup.mk' (fieldNormSubgroup K L) x *
QuotientGroup.mk' (fieldNormSubgroup K L) (normUnits K L z) =
QuotientGroup.mk' (fieldNormSubgroup K L) xEstablishes the identity QuotientGroup.mk' (fieldNormSubgroup K L) (normUnits K L z) * QuotientGroup.mk' (fieldNormSubgroup K L) x = QuotientGroup.mk' (fieldNormSubgroup K L) x.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_norm_mul_mk_eq_mk (z : Lˣ) (x : Kˣ) :
QuotientGroup.mk' (fieldNormSubgroup K L) (normUnits K L z) *
QuotientGroup.mk' (fieldNormSubgroup K L) x =
QuotientGroup.mk' (fieldNormSubgroup K L) xNorm of an element coming from the base field.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormUnits_algebraMap (u : Kˣ) :
normUnits K L (Units.map (algebraMap K L).toMonoidHom u) =
u ^ Module.finrank K LEstablishes the identity normUnits K L (Units.map (algebraMap K L).toMonoidHom u) = u.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormUnits_algebraMap_of_finrank_eq_one
(hfin : Module.finrank K L = 1) (u : Kˣ) :
normUnits K L (Units.map (algebraMap K L).toMonoidHom u) = uEstablishes the membership statement u ^ Module.finrank K L ∈ fieldNormSubgroup K L.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormSubgroup_pow_finrank_mem (u : Kˣ) :
u ^ Module.finrank K L ∈ fieldNormSubgroup K LEstablishes the identity fieldNormSubgroup K L = ⊤.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormSubgroup_eq_top_of_finrank_eq_one
(hfin : Module.finrank K L = 1) :
fieldNormSubgroup K L = ⊤Establishes the identity (QuotientGroup.mk' (fieldNormSubgroup K L) u) ^ Module.finrank K L = 1.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_pow_finrank_eq_one (u : Kˣ) :
(QuotientGroup.mk' (fieldNormSubgroup K L) u) ^
Module.finrank K L = 1Establishes the identity q ^ Module.finrank K L = 1.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_pow_finrank_eq_one
(q : Kˣ ⧸ fieldNormSubgroup K L) :
q ^ Module.finrank K L = 1Establishes the identity (QuotientGroup.mk' (fieldNormSubgroup K L) u) ^ n = 1.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_pow_eq_one_of_finrank_dvd
{n : ℕ} (hn : Module.finrank K L ∣ n) (u : Kˣ) :
(QuotientGroup.mk' (fieldNormSubgroup K L) u) ^ n = 1Establishes the identity q ^ n = 1.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_pow_eq_one_of_finrank_dvd
{n : ℕ} (hn : Module.finrank K L ∣ n)
(q : Kˣ ⧸ fieldNormSubgroup K L) :
q ^ n = 1Establishes the identity q = 1.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_eq_one_of_finrank_eq_one
(hfin : Module.finrank K L = 1)
(q : Kˣ ⧸ fieldNormSubgroup K L) :
q = 1Establishes the identity q = r.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_eq_of_finrank_eq_one
(hfin : Module.finrank K L = 1)
(q r : Kˣ ⧸ fieldNormSubgroup K L) :
q = rPackage a field norm as a ValuedNorm once the valuation formula has been proved for the concrete extension. The natural-number argument is not a second source of extension-invariant data: hformula certifies it as the valuation multiplier (and a source uniformizer makes that multiplier unique).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]def valuedFieldNorm
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x) :
ValuedNorm vK vL where
toHom := normUnits K L
residueDegree := residueDegree
valuation_formula := hformulaEstablishes the identity (valuedFieldNorm K L vK vL residueDegree hformula).toHom = normUnits K L.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem valuedFieldNorm_toHom
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x) :
(valuedFieldNorm K L vK vL residueDegree hformula).toHom =
normUnits K LEstablishes the identity (valuedFieldNorm K L vK vL residueDegree hformula).normSubgroup = fieldNormSubgroup K L.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem valuedFieldNorm_normSubgroup_eq_fieldNormSubgroup
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x) :
(valuedFieldNorm K L vK vL residueDegree hformula).normSubgroup =
fieldNormSubgroup K LConcrete cyclic description of the field-norm quotient. The assumptions are the valuation formula for the field norm and the assertion that every target valuation-zero element is already a field norm.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]def fieldNormQuotientEquivZMod
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖK : Kˣ} (hϖK : vK.IsUniformizer ϖK)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L) :
Kˣ ⧸ fieldNormSubgroup K L ≃* Multiplicative (ZMod residueDegree)Establishes the identity fieldNormQuotientEquivZMod K L vK vL residueDegree hformula hϖK hϖL hzero (QuotientGroup.mk' (fieldNormSubgroup K L) x) = Multiplicative.ofAdd ((vK.val x : ℤ) : ZMod residueDegree).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotientEquivZMod_mk
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖK : Kˣ} (hϖK : vK.IsUniformizer ϖK)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(x : Kˣ) :
fieldNormQuotientEquivZMod K L vK vL residueDegree
hformula hϖK hϖL hzero
(QuotientGroup.mk' (fieldNormSubgroup K L) x) =
Multiplicative.ofAdd ((vK.val x : ℤ) : ZMod residueDegree)fieldNormQuotientEquivZMod_uniformizer satisfies the integer-power formula fieldNormQuotientEquivZMod K L vK vL residueDegree hformula hϖK hϖL hzero (QuotientGroup.mk' (fieldNormSubgroup K L) (ϖK ^ n)) = Multiplicative.ofAdd ((n : ℤ) : ZMod residueDegree).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotientEquivZMod_uniformizer_zpow
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖK : Kˣ} (hϖK : vK.IsUniformizer ϖK)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(n : ℤ) :
fieldNormQuotientEquivZMod K L vK vL residueDegree
hformula hϖK hϖL hzero
(QuotientGroup.mk' (fieldNormSubgroup K L) (ϖK ^ n)) =
Multiplicative.ofAdd ((n : ℤ) : ZMod residueDegree)fieldNormQuotientEquivZMod_uniformizerClass satisfies the integer-power formula fieldNormQuotientEquivZMod K L vK vL residueDegree hformula hϖK hϖL hzero ((QuotientGroup.mk' (fieldNormSubgroup K L) ϖK) ^ n) = Multiplicative.ofAdd ((n : ℤ) : ZMod residueDegree).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotientEquivZMod_uniformizerClass_zpow
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖK : Kˣ} (hϖK : vK.IsUniformizer ϖK)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(n : ℤ) :
fieldNormQuotientEquivZMod K L vK vL residueDegree
hformula hϖK hϖL hzero
((QuotientGroup.mk' (fieldNormSubgroup K L) ϖK) ^ n) =
Multiplicative.ofAdd ((n : ℤ) : ZMod residueDegree)Establishes the identity (fieldNormQuotientEquivZMod K L vK vL residueDegree hformula hϖK hϖL hzero).symm (Multiplicative.ofAdd ((n : ℤ) : ZMod residueDegree)) = QuotientGroup.mk' (fieldNormSubgroup K L) (ϖK ^ n).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotientEquivZMod_symm_mk_ofAdd
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖK : Kˣ} (hϖK : vK.IsUniformizer ϖK)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(n : ℤ) :
(fieldNormQuotientEquivZMod K L vK vL residueDegree
hformula hϖK hϖL hzero).symm
(Multiplicative.ofAdd ((n : ℤ) : ZMod residueDegree)) =
QuotientGroup.mk' (fieldNormSubgroup K L) (ϖK ^ n)Cardinality form of the concrete field-norm quotient computation.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem cardinalMk_fieldNormQuotient_eq_residueDegree
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖK : Kˣ} (hϖK : vK.IsUniformizer ϖK)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
[NeZero residueDegree] :
Cardinal.mk (Kˣ ⧸ fieldNormSubgroup K L) = residueDegreeField-norm value-image criterion: an integer is attained as the valuation of a field norm exactly when it is divisible by the residue degree.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem exists_mem_fieldNormSubgroup_val_eq_iff_residueDegree_dvd
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL) (n : ℤ) :
(∃ x : Kˣ, x ∈ fieldNormSubgroup K L ∧ vK.val x = n) ↔
(residueDegree : ℤ) ∣ nThe value image of the field-norm subgroup is exactly fℤ.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormSubgroup_valueImage_eq_residueDegree
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL) :
vK.subgroupValueSubgroup (fieldNormSubgroup K L) =
integerMultipleSubgroup (residueDegree : ℤ)Characterizes x ∈ fieldNormSubgroup K L by the equivalent condition (residueDegree : ℤ) ∣ vK.val x.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem mem_fieldNormSubgroup_iff_residueDegree_dvd_val_of_zeroSubgroup_le
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L) (x : Kˣ) :
x ∈ fieldNormSubgroup K L ↔ (residueDegree : ℤ) ∣ vK.val xEstablishes the divisibility statement (residueDegree : ℤ) ∣ vK.val x.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormSubgroup_residueDegree_dvd_val_of_mem
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{x : Kˣ} (hx : x ∈ fieldNormSubgroup K L) :
(residueDegree : ℤ) ∣ vK.val xEstablishes the membership statement x ∈ fieldNormSubgroup K L.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormSubgroup_mem_of_residueDegree_dvd_val_of_zeroSubgroup_le
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
{x : Kˣ} (hx : (residueDegree : ℤ) ∣ vK.val x) :
x ∈ fieldNormSubgroup K LCharacterizes x / y ∈ fieldNormSubgroup K L by the equivalent condition (residueDegree : ℤ) ∣ vK.val x - vK.val y.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormSubgroup_div_mem_iff_residueDegree_dvd_valuation_difference
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(x y : Kˣ) :
x / y ∈ fieldNormSubgroup K L ↔
(residueDegree : ℤ) ∣ vK.val x - vK.val yCharacterizes y⁻¹ * x ∈ fieldNormSubgroup K L by the equivalent condition (residueDegree : ℤ) ∣ vK.val x - vK.val y.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormSubgroup_inv_mul_mem_iff_residueDegree_dvd_valuation_difference
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(x y : Kˣ) :
y⁻¹ * x ∈ fieldNormSubgroup K L ↔
(residueDegree : ℤ) ∣ vK.val x - vK.val yUnder the standard valuation formula and valuation-zero norm-surjectivity, the norm equation N z = x is solvable exactly when f divides v(x).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem exists_fieldNormUnits_eq_iff_residueDegree_dvd_val
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L) (x : Kˣ) :
(∃ z : Lˣ, normUnits K L z = x) ↔
(residueDegree : ℤ) ∣ vK.val xEstablishes the identity ∃ z : Lˣ, normUnits K L z = x.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem exists_fieldNormUnits_eq_of_residueDegree_dvd_val
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
{x : Kˣ} (hx : (residueDegree : ℤ) ∣ vK.val x) :
∃ z : Lˣ, normUnits K L z = xDifference form of the concrete norm equation criterion.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem exists_fieldNormUnits_eq_div_iff_residueDegree_dvd_valuation_difference
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(x y : Kˣ) :
(∃ z : Lˣ, normUnits K L z = x / y) ↔
(residueDegree : ℤ) ∣ vK.val x - vK.val yMultiplicative equation form of the concrete norm-lift criterion.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem exists_fieldNormUnits_mul_eq_iff_residueDegree_dvd_valuation_difference
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(x y : Kˣ) :
(∃ z : Lˣ, normUnits K L z * y = x) ↔
(residueDegree : ℤ) ∣ vK.val x - vK.val yLeft-multiplicative equation form of the concrete norm-lift criterion.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem exists_mul_fieldNormUnits_eq_iff_residueDegree_dvd_valuation_difference
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(x y : Kˣ) :
(∃ z : Lˣ, y * normUnits K L z = x) ↔
(residueDegree : ℤ) ∣ vK.val x - vK.val yCharacterizes QuotientGroup.mk' (fieldNormSubgroup K L) x = 1 by the equivalent condition (residueDegree : ℤ) ∣ vK.val x.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_eq_one_iff_residueDegree_dvd_val
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(x : Kˣ) :
QuotientGroup.mk' (fieldNormSubgroup K L) x = 1 ↔
(residueDegree : ℤ) ∣ vK.val xCharacterizes QuotientGroup.mk' (fieldNormSubgroup K L) x = QuotientGroup.mk' (fieldNormSubgroup K L) y by the equivalent condition (residueDegree : ℤ) ∣ vK.val x - vK.val y.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_eq_iff_residueDegree_dvd_valuation_difference
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(x y : Kˣ) :
QuotientGroup.mk' (fieldNormSubgroup K L) x =
QuotientGroup.mk' (fieldNormSubgroup K L) y ↔
(residueDegree : ℤ) ∣ vK.val x - vK.val yCharacterizes ϖK ^ n ∈ fieldNormSubgroup K L by the equivalent condition (residueDegree : ℤ) ∣ n.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormSubgroup_uniformizer_zpow_mem_iff
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖK : Kˣ} (hϖK : vK.IsUniformizer ϖK)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(n : ℤ) :
ϖK ^ n ∈ fieldNormSubgroup K L ↔
(residueDegree : ℤ) ∣ nCharacterizes ϖK ^ m / ϖK ^ n ∈ fieldNormSubgroup K L by the equivalent condition (residueDegree : ℤ) ∣ m - n.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormSubgroup_uniformizer_zpow_div_mem_iff
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖK : Kˣ} (hϖK : vK.IsUniformizer ϖK)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(m n : ℤ) :
ϖK ^ m / ϖK ^ n ∈ fieldNormSubgroup K L ↔
(residueDegree : ℤ) ∣ m - nEstablishes the identity QuotientGroup.mk' (fieldNormSubgroup K L) x = QuotientGroup.mk' (fieldNormSubgroup K L) (ϖK ^ vK.val x).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_eq_uniformizer_zpow_val
(vK : MultiplicativeIntegerValuation Kˣ)
{ϖK : Kˣ} (hϖK : vK.IsUniformizer ϖK)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L) (x : Kˣ) :
QuotientGroup.mk' (fieldNormSubgroup K L) x =
QuotientGroup.mk' (fieldNormSubgroup K L) (ϖK ^ vK.val x)Establishes the identity QuotientGroup.mk' (fieldNormSubgroup K L) x = (QuotientGroup.mk' (fieldNormSubgroup K L) ϖK) ^ vK.val x.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_eq_uniformizerClass_zpow_val
(vK : MultiplicativeIntegerValuation Kˣ)
{ϖK : Kˣ} (hϖK : vK.IsUniformizer ϖK)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L) (x : Kˣ) :
QuotientGroup.mk' (fieldNormSubgroup K L) x =
(QuotientGroup.mk' (fieldNormSubgroup K L) ϖK) ^ vK.val xCharacterizes QuotientGroup.mk' (fieldNormSubgroup K L) x = QuotientGroup.mk' (fieldNormSubgroup K L) (ϖK ^ n) by the equivalent condition (residueDegree : ℤ) ∣ vK.val x - n.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_eq_uniformizer_zpow_iff
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖK : Kˣ} (hϖK : vK.IsUniformizer ϖK)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(x : Kˣ) (n : ℤ) :
QuotientGroup.mk' (fieldNormSubgroup K L) x =
QuotientGroup.mk' (fieldNormSubgroup K L) (ϖK ^ n) ↔
(residueDegree : ℤ) ∣ vK.val x - nCharacterizes QuotientGroup.mk' (fieldNormSubgroup K L) x = (QuotientGroup.mk' (fieldNormSubgroup K L) ϖK) ^ n by the equivalent condition (residueDegree : ℤ) ∣ vK.val x - n.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_mk_eq_uniformizerClass_zpow_iff
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖK : Kˣ} (hϖK : vK.IsUniformizer ϖK)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(x : Kˣ) (n : ℤ) :
QuotientGroup.mk' (fieldNormSubgroup K L) x =
(QuotientGroup.mk' (fieldNormSubgroup K L) ϖK) ^ n ↔
(residueDegree : ℤ) ∣ vK.val x - nCharacterizes (QuotientGroup.mk' (fieldNormSubgroup K L) ϖK) ^ m = (QuotientGroup.mk' (fieldNormSubgroup K L) ϖK) ^ n by the equivalent condition (residueDegree : ℤ) ∣ m - n.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_uniformizerClass_zpow_eq_iff
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖK : Kˣ} (hϖK : vK.IsUniformizer ϖK)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(m n : ℤ) :
(QuotientGroup.mk' (fieldNormSubgroup K L) ϖK) ^ m =
(QuotientGroup.mk' (fieldNormSubgroup K L) ϖK) ^ n ↔
(residueDegree : ℤ) ∣ m - nCharacterizes (QuotientGroup.mk' (fieldNormSubgroup K L) ϖK) ^ n = 1 by the equivalent condition (residueDegree : ℤ) ∣ n.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_uniformizerClass_zpow_eq_one_iff
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖK : Kˣ} (hϖK : vK.IsUniformizer ϖK)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(n : ℤ) :
(QuotientGroup.mk' (fieldNormSubgroup K L) ϖK) ^ n = 1 ↔
(residueDegree : ℤ) ∣ nEstablishes the identity (QuotientGroup.mk' (fieldNormSubgroup K L) ϖK) ^ (residueDegree : ℤ) = 1.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_uniformizerClass_zpow_residueDegree_eq_one
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖK : Kˣ} (hϖK : vK.IsUniformizer ϖK)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L) :
(QuotientGroup.mk' (fieldNormSubgroup K L) ϖK) ^
(residueDegree : ℤ) = 1The concrete field-norm quotient is generated by the class of any target uniformizer under the standard valuation-zero norm-surjectivity hypothesis.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_generated_by_uniformizerClass
(vK : MultiplicativeIntegerValuation Kˣ)
{ϖK : Kˣ} (hϖK : vK.IsUniformizer ϖK)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(q : Kˣ ⧸ fieldNormSubgroup K L) :
∃ n : ℤ,
q = (QuotientGroup.mk' (fieldNormSubgroup K L) ϖK) ^ nEstablishes the identity Subgroup.closure ({QuotientGroup.mk' (fieldNormSubgroup K L) ϖK} : Set (Kˣ ⧸ fieldNormSubgroup K L)) = ⊤.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_closure_uniformizerClass_eq_top
(vK : MultiplicativeIntegerValuation Kˣ)
{ϖK : Kˣ} (hϖK : vK.IsUniformizer ϖK)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L) :
Subgroup.closure
({QuotientGroup.mk' (fieldNormSubgroup K L) ϖK} :
Set (Kˣ ⧸ fieldNormSubgroup K L)) =
⊤Establishes the identity fieldNormSubgroup K L = ⊤.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormSubgroup_eq_top_of_residueDegree_eq_one
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(hres : residueDegree = 1) :
fieldNormSubgroup K L = ⊤The specified map is surjective: Function.Surjective (normUnits K L).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormUnits_surjective_of_residueDegree_eq_one
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(hres : residueDegree = 1) :
Function.Surjective (normUnits K L)Under the standard valuation formula and valuation-zero norm-surjectivity, the field norm on units is surjective exactly in residue degree one.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormUnits_surjective_iff_residueDegree_eq_one
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖK : Kˣ} (hϖK : vK.IsUniformizer ϖK)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L) :
Function.Surjective (normUnits K L) ↔ residueDegree = 1Subgroup form of the residue-degree-one norm-surjectivity criterion.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormSubgroup_eq_top_iff_residueDegree_eq_one
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖK : Kˣ} (hϖK : vK.IsUniformizer ϖK)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L) :
fieldNormSubgroup K L = ⊤ ↔ residueDegree = 1Establishes the identity q = 1.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_eq_one_of_residueDegree_eq_one
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(hres : residueDegree = 1)
(q : Kˣ ⧸ fieldNormSubgroup K L) :
q = 1Establishes the identity q = r.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_eq_of_residueDegree_eq_one
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L)
(hres : residueDegree = 1)
(q r : Kˣ ⧸ fieldNormSubgroup K L) :
q = rQuotient form of the residue-degree-one norm-surjectivity criterion.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormQuotient_forall_eq_one_iff_residueDegree_eq_one
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
{ϖK : Kˣ} (hϖK : vK.IsUniformizer ϖK)
{ϖL : Lˣ} (hϖL : vL.IsUniformizer ϖL)
(hzero : vK.zeroSubgroup ≤ fieldNormSubgroup K L) :
(∀ q : Kˣ ⧸ fieldNormSubgroup K L, q = 1) ↔ residueDegree = 1Concrete compatibility condition saying that the field norm maps the n-th source principal-unit subgroup into the requested target level.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]abbrev fieldNormMapsFiltrationLevels
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ) : PropCharacterizes ValuedNorm.MapsFiltrationLevels (valuedFieldNorm K L vK vL residueDegree hformula) UK UL targetLevel by the equivalent condition fieldNormMapsFiltrationLevels K L UK UL targetLevel.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem valuedFieldNorm_mapsFiltrationLevels_iff
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(residueDegree : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ) :
ValuedNorm.MapsFiltrationLevels
(valuedFieldNorm K L vK vL residueDegree hformula)
UK UL targetLevel ↔
fieldNormMapsFiltrationLevels K L UK UL targetLevelFiltration compatibility can be weakened by replacing the target level by a coarser one.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormMapsFiltrationLevels_of_le
{UK : AntitoneSubgroupFiltration Kˣ} {UL : AntitoneSubgroupFiltration Lˣ}
{targetLevel targetLevel' : ℕ → ℕ}
(hN : fieldNormMapsFiltrationLevels K L UK UL targetLevel)
(hle : ∀ n, targetLevel' n ≤ targetLevel n) :
fieldNormMapsFiltrationLevels K L UK UL targetLevel'The field norm restricted to a principal-unit filtration level.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]def fieldNormMapLevelOfMapsFiltrationLevels
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ)
(hN : fieldNormMapsFiltrationLevels K L UK UL targetLevel) (n : ℕ) :
UL.principalUnitSubgroup n →*
UK.principalUnitSubgroup (targetLevel n) where
toFun x := ⟨normUnits K L x.1, hN n x.2⟩
map_one' := by
apply Subtype.ext
exact (normUnits K L).map_one
map_mul' x y := by
apply Subtype.ext
exact (normUnits K L).map_mul x.1 y.1The defining evaluation formula for fieldNormMapLevelOfMapsFiltrationLevels is (fieldNormMapLevelOfMapsFiltrationLevels K L UK UL targetLevel hN n x : Kˣ) = normUnits K L x.1.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormMapLevelOfMapsFiltrationLevels_apply
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ)
(hN : fieldNormMapsFiltrationLevels K L UK UL targetLevel) (n : ℕ)
(x : UL.principalUnitSubgroup n) :
(fieldNormMapLevelOfMapsFiltrationLevels K L UK UL targetLevel hN n x :
Kˣ) =
normUnits K L x.1The field norm descended to quotients by compatible principal-unit filtration levels.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]def fieldNormFiltrationQuotientMap
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ)
(hN : fieldNormMapsFiltrationLevels K L UK UL targetLevel) (n : ℕ)
[(UL.principalUnitSubgroup n).Normal]
[(UK.principalUnitSubgroup (targetLevel n)).Normal] :
Lˣ ⧸ UL.principalUnitSubgroup n →*
Kˣ ⧸ UK.principalUnitSubgroup (targetLevel n)The defining evaluation formula for fieldNormFiltrationQuotientMap is fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n (QuotientGroup.mk x) = QuotientGroup.mk (normUnits K L x).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormFiltrationQuotientMap_apply_mk
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ)
(hN : fieldNormMapsFiltrationLevels K L UK UL targetLevel) (n : ℕ)
[(UL.principalUnitSubgroup n).Normal]
[(UK.principalUnitSubgroup (targetLevel n)).Normal] (x : Lˣ) :
fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n
(QuotientGroup.mk x) =
QuotientGroup.mk (normUnits K L x)Establishes the identity fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n (QuotientGroup.mk' (UL.principalUnitSubgroup n) x) = QuotientGroup.mk' (UK.principalUnitSubgroup (targetLevel n)) (normUnits K L x).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormFiltrationQuotientMap_apply_mk'
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ)
(hN : fieldNormMapsFiltrationLevels K L UK UL targetLevel) (n : ℕ)
[(UL.principalUnitSubgroup n).Normal]
[(UK.principalUnitSubgroup (targetLevel n)).Normal] (x : Lˣ) :
fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n
(QuotientGroup.mk' (UL.principalUnitSubgroup n) x) =
QuotientGroup.mk' (UK.principalUnitSubgroup (targetLevel n))
(normUnits K L x)Characterizes fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n (QuotientGroup.mk' (UL.principalUnitSubgroup n) x) = 1 by the equivalent condition normUnits K L x ∈ UK.principalUnitSubgroup (targetLevel n).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormFiltrationQuotientMap_mk_eq_one_iff
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ)
(hN : fieldNormMapsFiltrationLevels K L UK UL targetLevel) (n : ℕ)
[(UL.principalUnitSubgroup n).Normal]
[(UK.principalUnitSubgroup (targetLevel n)).Normal] (x : Lˣ) :
fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n
(QuotientGroup.mk' (UL.principalUnitSubgroup n) x) = 1 ↔
normUnits K L x ∈
UK.principalUnitSubgroup (targetLevel n)Characterizes fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n (QuotientGroup.mk' (UL.principalUnitSubgroup n) x) = fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n (QuotientGroup.mk' (UL.principalUnitSubgroup n) y) by the equivalent condition normUnits K L (x / y) ∈ UK.principalUnitSubgroup (targetLevel n).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormFiltrationQuotientMap_mk_eq_iff_div_mem
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ)
(hN : fieldNormMapsFiltrationLevels K L UK UL targetLevel) (n : ℕ)
[(UL.principalUnitSubgroup n).Normal]
[(UK.principalUnitSubgroup (targetLevel n)).Normal] (x y : Lˣ) :
fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n
(QuotientGroup.mk' (UL.principalUnitSubgroup n) x) =
fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n
(QuotientGroup.mk' (UL.principalUnitSubgroup n) y) ↔
normUnits K L (x / y) ∈
UK.principalUnitSubgroup (targetLevel n)Characterizes fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n (QuotientGroup.mk' (UL.principalUnitSubgroup n) x) = fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n (QuotientGroup.mk' (UL.principalUnitSubgroup n) y) by the equivalent condition normUnits K L (y⁻¹ * x) ∈ UK.principalUnitSubgroup (targetLevel n).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormFiltrationQuotientMap_mk_eq_iff_inv_mul_mem
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ)
(hN : fieldNormMapsFiltrationLevels K L UK UL targetLevel) (n : ℕ)
[(UL.principalUnitSubgroup n).Normal]
[(UK.principalUnitSubgroup (targetLevel n)).Normal] (x y : Lˣ) :
fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n
(QuotientGroup.mk' (UL.principalUnitSubgroup n) x) =
fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n
(QuotientGroup.mk' (UL.principalUnitSubgroup n) y) ↔
normUnits K L (y⁻¹ * x) ∈
UK.principalUnitSubgroup (targetLevel n)Characterizes Function.Surjective (fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n) by the equivalent condition ∀ y : Kˣ, ∃ x : Lˣ, normUnits K L x / y ∈ UK.principalUnitSubgroup (targetLevel n).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormFiltrationQuotientMap_surjective_iff_exists_div_mem
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ)
(hN : fieldNormMapsFiltrationLevels K L UK UL targetLevel) (n : ℕ)
[(UL.principalUnitSubgroup n).Normal]
[(UK.principalUnitSubgroup (targetLevel n)).Normal] :
Function.Surjective
(fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n) ↔
∀ y : Kˣ, ∃ x : Lˣ,
normUnits K L x / y ∈
UK.principalUnitSubgroup (targetLevel n)The specified map is surjective: Function.Surjective (fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormFiltrationQuotientMap_surjective_of_exists_div_mem
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ)
(hN : fieldNormMapsFiltrationLevels K L UK UL targetLevel) (n : ℕ)
[(UL.principalUnitSubgroup n).Normal]
[(UK.principalUnitSubgroup (targetLevel n)).Normal]
(hLift : ∀ y : Kˣ, ∃ x : Lˣ,
normUnits K L x / y ∈
UK.principalUnitSubgroup (targetLevel n)) :
Function.Surjective
(fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n)The preimage of a target principal-unit filtration subgroup under the field norm.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]def fieldNormFiltrationPreimageSubgroup
(UK : AntitoneSubgroupFiltration Kˣ) (targetLevel : ℕ → ℕ) (n : ℕ) :
Subgroup LˣCharacterizes x ∈ fieldNormFiltrationPreimageSubgroup K L UK targetLevel n by the equivalent condition normUnits K L x ∈ UK.principalUnitSubgroup (targetLevel n).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem mem_fieldNormFiltrationPreimageSubgroup_iff
(UK : AntitoneSubgroupFiltration Kˣ) (targetLevel : ℕ → ℕ) (n : ℕ)
(x : Lˣ) :
x ∈ fieldNormFiltrationPreimageSubgroup K L UK targetLevel n ↔
normUnits K L x ∈
UK.principalUnitSubgroup (targetLevel n)Proves the bound UL.principalUnitSubgroup n ≤ fieldNormFiltrationPreimageSubgroup K L UK targetLevel n.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem principalUnitSubgroup_le_fieldNormFiltrationPreimageSubgroup
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ)
(hN : fieldNormMapsFiltrationLevels K L UK UL targetLevel) (n : ℕ) :
UL.principalUnitSubgroup n ≤
fieldNormFiltrationPreimageSubgroup K L UK targetLevel nThe subgroup appearing in (fieldNormFiltrationPreimageSubgroup K L UK targetLevel n).Normal is normal.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]instance fieldNormFiltrationPreimageSubgroup_normal
(UK : AntitoneSubgroupFiltration Kˣ) (targetLevel : ℕ → ℕ) (n : ℕ)
[(UK.principalUnitSubgroup (targetLevel n)).Normal] :
(fieldNormFiltrationPreimageSubgroup K L UK targetLevel n).NormalThe class of the field-norm preimage of the target filtration subgroup inside the source filtration quotient.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]def fieldNormFiltrationPreimageClassInQuotient
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ) (n : ℕ)
[(UL.principalUnitSubgroup n).Normal] :
Subgroup (Lˣ ⧸ UL.principalUnitSubgroup n)The subgroup appearing in (fieldNormFiltrationPreimageClassInQuotient K L UK UL targetLevel n).Normal is normal.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]instance fieldNormFiltrationPreimageClassInQuotient_normal
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ) (n : ℕ)
[(UL.principalUnitSubgroup n).Normal]
[(UK.principalUnitSubgroup (targetLevel n)).Normal] :
(fieldNormFiltrationPreimageClassInQuotient
K L UK UL targetLevel n).NormalCharacterizes q ∈ fieldNormFiltrationPreimageClassInQuotient K L UK UL targetLevel n by the equivalent condition ∃ x : Lˣ, x ∈ fieldNormFiltrationPreimageSubgroup K L UK targetLevel n ∧ QuotientGroup.mk' (UL.principalUnitSubgroup n) x = q.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem mem_fieldNormFiltrationPreimageClassInQuotient_iff
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ) (n : ℕ)
[(UL.principalUnitSubgroup n).Normal]
(q : Lˣ ⧸ UL.principalUnitSubgroup n) :
q ∈ fieldNormFiltrationPreimageClassInQuotient
K L UK UL targetLevel n ↔
∃ x : Lˣ,
x ∈ fieldNormFiltrationPreimageSubgroup K L UK targetLevel n ∧
QuotientGroup.mk' (UL.principalUnitSubgroup n) x = qCharacterizes q ∈ fieldNormFiltrationPreimageClassInQuotient K L UK UL targetLevel n by the equivalent condition ∃ x : Lˣ, normUnits K L x ∈ UK.principalUnitSubgroup (targetLevel n) ∧ QuotientGroup.mk' (UL.principalUnitSubgroup n) x = q.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem mem_fieldNormFiltrationPreimageClassInQuotient_iff_exists_norm_mem
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ) (n : ℕ)
[(UL.principalUnitSubgroup n).Normal]
(q : Lˣ ⧸ UL.principalUnitSubgroup n) :
q ∈ fieldNormFiltrationPreimageClassInQuotient
K L UK UL targetLevel n ↔
∃ x : Lˣ,
normUnits K L x ∈
UK.principalUnitSubgroup (targetLevel n) ∧
QuotientGroup.mk' (UL.principalUnitSubgroup n) x = qEstablishes the membership statement QuotientGroup.mk' (UL.principalUnitSubgroup n) x ∈ fieldNormFiltrationPreimageClassInQuotient K L UK UL targetLevel n.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormFiltrationPreimageClassInQuotient_mk_mem
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ) {n : ℕ}
[(UL.principalUnitSubgroup n).Normal] {x : Lˣ}
(hx : x ∈ fieldNormFiltrationPreimageSubgroup K L UK targetLevel n) :
QuotientGroup.mk' (UL.principalUnitSubgroup n) x ∈
fieldNormFiltrationPreimageClassInQuotient K L UK UL targetLevel nThe kernel of the concrete field-norm filtration quotient map is the class of the norm-preimage of the target filtration subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormFiltrationQuotientMap_ker_eq_preimageClass
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ)
(hN : fieldNormMapsFiltrationLevels K L UK UL targetLevel) (n : ℕ)
[(UL.principalUnitSubgroup n).Normal]
[(UK.principalUnitSubgroup (targetLevel n)).Normal] :
(fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n).ker =
fieldNormFiltrationPreimageClassInQuotient
K L UK UL targetLevel nCharacterizes fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n q = 1 by the equivalent condition q ∈ fieldNormFiltrationPreimageClassInQuotient K L UK UL targetLevel n.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormFiltrationQuotientMap_eq_one_iff_mem_preimageClass
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ)
(hN : fieldNormMapsFiltrationLevels K L UK UL targetLevel) (n : ℕ)
[(UL.principalUnitSubgroup n).Normal]
[(UK.principalUnitSubgroup (targetLevel n)).Normal]
(q : Lˣ ⧸ UL.principalUnitSubgroup n) :
fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n q = 1 ↔
q ∈ fieldNormFiltrationPreimageClassInQuotient
K L UK UL targetLevel nFirst-isomorphism form of the concrete field-norm filtration quotient map, with codomain the actual range when no surjectivity hypothesis is available.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]def fieldNormFiltrationQuotientModuloPreimageClassEquivRange
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ)
(hN : fieldNormMapsFiltrationLevels K L UK UL targetLevel) (n : ℕ)
[(UL.principalUnitSubgroup n).Normal]
[(UK.principalUnitSubgroup (targetLevel n)).Normal] :
(Lˣ ⧸ UL.principalUnitSubgroup n) ⧸
fieldNormFiltrationPreimageClassInQuotient
K L UK UL targetLevel n ≃*
(fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n).rangeEstablishes the identity fieldNormFiltrationQuotientModuloPreimageClassEquivRange K L UK UL targetLevel hN n (QuotientGroup.mk' (fieldNormFiltrationPreimageClassInQuotient K L UK UL targetLevel n) q) = (fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n).rangeRestrict q.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormFiltrationQuotientModuloPreimageClassEquivRange_mk
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ)
(hN : fieldNormMapsFiltrationLevels K L UK UL targetLevel) (n : ℕ)
[(UL.principalUnitSubgroup n).Normal]
[(UK.principalUnitSubgroup (targetLevel n)).Normal]
(q : Lˣ ⧸ UL.principalUnitSubgroup n) :
fieldNormFiltrationQuotientModuloPreimageClassEquivRange
K L UK UL targetLevel hN n
(QuotientGroup.mk'
(fieldNormFiltrationPreimageClassInQuotient
K L UK UL targetLevel n) q) =
(fieldNormFiltrationQuotientMap
K L UK UL targetLevel hN n).rangeRestrict qEstablishes the identity ((fieldNormFiltrationQuotientModuloPreimageClassEquivRange K L UK UL targetLevel hN n (QuotientGroup.mk' (fieldNormFiltrationPreimageClassInQuotient K L UK UL targetLevel n) q) : (fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n).range) : Kˣ ⧸ UK.principalUnitSubgroup (targetLevel n)) = fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n q.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem coe_fieldNormFiltrationQuotientModuloPreimageClassEquivRange_mk
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ)
(hN : fieldNormMapsFiltrationLevels K L UK UL targetLevel) (n : ℕ)
[(UL.principalUnitSubgroup n).Normal]
[(UK.principalUnitSubgroup (targetLevel n)).Normal]
(q : Lˣ ⧸ UL.principalUnitSubgroup n) :
((fieldNormFiltrationQuotientModuloPreimageClassEquivRange
K L UK UL targetLevel hN n
(QuotientGroup.mk'
(fieldNormFiltrationPreimageClassInQuotient
K L UK UL targetLevel n) q) :
(fieldNormFiltrationQuotientMap
K L UK UL targetLevel hN n).range) :
Kˣ ⧸ UK.principalUnitSubgroup (targetLevel n)) =
fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n qFirst-isomorphism form of a surjective concrete field-norm filtration quotient map.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]def fieldNormFiltrationQuotientModuloPreimageClassEquivTarget
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ)
(hN : fieldNormMapsFiltrationLevels K L UK UL targetLevel) (n : ℕ)
[(UL.principalUnitSubgroup n).Normal]
[(UK.principalUnitSubgroup (targetLevel n)).Normal]
(hSurj : Function.Surjective
(fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n)) :
(Lˣ ⧸ UL.principalUnitSubgroup n) ⧸
fieldNormFiltrationPreimageClassInQuotient
K L UK UL targetLevel n ≃*
Kˣ ⧸ UK.principalUnitSubgroup (targetLevel n)Establishes the identity fieldNormFiltrationQuotientModuloPreimageClassEquivTarget K L UK UL targetLevel hN n hSurj (QuotientGroup.mk' (fieldNormFiltrationPreimageClassInQuotient K L UK UL targetLevel n) q) = fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n q.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem fieldNormFiltrationQuotientModuloPreimageClassEquivTarget_mk
(UK : AntitoneSubgroupFiltration Kˣ) (UL : AntitoneSubgroupFiltration Lˣ)
(targetLevel : ℕ → ℕ)
(hN : fieldNormMapsFiltrationLevels K L UK UL targetLevel) (n : ℕ)
[(UL.principalUnitSubgroup n).Normal]
[(UK.principalUnitSubgroup (targetLevel n)).Normal]
(hSurj : Function.Surjective
(fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n))
(q : Lˣ ⧸ UL.principalUnitSubgroup n) :
fieldNormFiltrationQuotientModuloPreimageClassEquivTarget
K L UK UL targetLevel hN n hSurj
(QuotientGroup.mk'
(fieldNormFiltrationPreimageClassInQuotient
K L UK UL targetLevel n) q) =
fieldNormFiltrationQuotientMap K L UK UL targetLevel hN n q