Module

Quotients.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.Norm.Quotients

199 declarations indexed from sourceView source ↗

Module documentation

Develops quotient groups attached to an abstract valued norm, including kernel, image, and representative criteria.

Identifies norm-quotient classes with valuation classes modulo the residue degree and constructs the resulting cyclic equivalences.

Imports2

Mathlib.SetTheory.Cardinal.Finite
Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.Norm.Basic

Imported by3

theorem

valuation_apply_uniformizer_zpow

L55 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.valuation_apply_uniformizer_zpow

Documentation

valuation_apply_uniformizer satisfies the integer-power formula vG.val (N.toHom (ϖH ^ n)) = (N.residueDegree : ℤ) * n.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem valuation_apply_uniformizer_zpow {ϖH : H}
    (hϖH : vH.IsUniformizer ϖH) (n : ℤ) :
    vG.val (N.toHom (ϖH ^ n)) = (N.residueDegree : ℤ) * n

theorem

valuation_apply_uniformizer_pow

L64 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.valuation_apply_uniformizer_pow

Documentation

valuation_apply_uniformizer satisfies the natural-power formula vG.val (N.toHom (ϖH ^ n)) = (N.residueDegree : ℤ) * (n : ℤ).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem valuation_apply_uniformizer_pow {ϖH : H}
    (hϖH : vH.IsUniformizer ϖH) (n : ℕ) :
    vG.val (N.toHom (ϖH ^ n)) = (N.residueDegree : ℤ) * (n : ℤ)

theorem

valuation_apply_zeroSubgroup_mul_uniformizer_zpow

L73 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.valuation_apply_zeroSubgroup_mul_uniformizer_zpow

Documentation

valuation_apply_zeroSubgroup_mul_uniformizer satisfies the integer-power formula vG.val (N.toHom (u * ϖH ^ n)) = (N.residueDegree : ℤ) * n.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem valuation_apply_zeroSubgroup_mul_uniformizer_zpow
    {ϖH u : H} (hϖH : vH.IsUniformizer ϖH)
    (hu : u ∈ vH.zeroSubgroup) (n : ℤ) :
    vG.val (N.toHom (u * ϖH ^ n)) = (N.residueDegree : ℤ) * n

theorem

valuation_apply_zeroSubgroup_mul_uniformizer_pow

L83 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.valuation_apply_zeroSubgroup_mul_uniformizer_pow

Documentation

valuation_apply_zeroSubgroup_mul_uniformizer satisfies the natural-power formula vG.val (N.toHom (u * ϖH ^ n)) = (N.residueDegree : ℤ) * (n : ℤ).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem valuation_apply_zeroSubgroup_mul_uniformizer_pow
    {ϖH u : H} (hϖH : vH.IsUniformizer ϖH)
    (hu : u ∈ vH.zeroSubgroup) (n : ℕ) :
    vG.val (N.toHom (u * ϖH ^ n)) =
      (N.residueDegree : ℤ) * (n : ℤ)

theorem

residueDegree_dvd_valuation_of_mem_normSubgroup

L139 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.residueDegree_dvd_valuation_of_mem_normSubgroup

Documentation

The valuation of any norm is divisible by the residue degree.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem residueDegree_dvd_valuation_of_mem_normSubgroup
    {x : G} (hx : x ∈ N.normSubgroup) :
    (N.residueDegree : ℤ) ∣ vG.val x

theorem

exists_normSubgroup_val_eq_residueDegree_mul_of_uniformizer

L147 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.exists_normSubgroup_val_eq_residueDegree_mul_of_uniformizer

Documentation

If the source valuation has a uniformizer, every residue-degree multiple is realized as the valuation of an element of the norm subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem exists_normSubgroup_val_eq_residueDegree_mul_of_uniformizer
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH) (n : ℤ) :
    ∃ x : G, x ∈ N.normSubgroup ∧
      vG.val x = (N.residueDegree : ℤ) * n

theorem

exists_normSubgroup_val_eq_iff_residueDegree_dvd_of_uniformizer

L156 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.exists_normSubgroup_val_eq_iff_residueDegree_dvd_of_uniformizer

Documentation

Source-uniformizer form of the value image of the norm subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem exists_normSubgroup_val_eq_iff_residueDegree_dvd_of_uniformizer
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH) (m : ℤ) :
    (∃ x : G, x ∈ N.normSubgroup ∧ vG.val x = m) ↔
      (N.residueDegree : ℤ) ∣ m

theorem

valuationHom_mem_integerMultipleSubgroup_of_mem_normSubgroup

L172 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.valuationHom_mem_integerMultipleSubgroup_of_mem_normSubgroup

Documentation

The value of any norm-subgroup element lies in the residue-degree multiple subgroup of the target value group.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem valuationHom_mem_integerMultipleSubgroup_of_mem_normSubgroup
    {x : G} (hx : x ∈ N.normSubgroup) :
    vG.valuationHom x ∈ integerMultipleSubgroup (N.residueDegree : ℤ)

theorem

valuationHom_norm_mem_integerMultipleSubgroup

L184 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.valuationHom_norm_mem_integerMultipleSubgroup

Documentation

Establishes the membership statement vG.valuationHom (N.toHom x) ∈ integerMultipleSubgroup (N.residueDegree : ℤ).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem valuationHom_norm_mem_integerMultipleSubgroup (x : H) :
    vG.valuationHom (N.toHom x) ∈
      integerMultipleSubgroup (N.residueDegree : ℤ)

theorem

coe_quotientZeroSubgroupEquivValueSubgroup_norm_mk

L195 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.coe_quotientZeroSubgroupEquivValueSubgroup_norm_mk

Documentation

Establishes the identity ((vG.quotientZeroSubgroupEquivValueSubgroup (QuotientGroup.mk' vG.zeroSubgroup (N.toHom x)) : vG.valueSubgroup) : Multiplicative ℤ) = vH.valuationHom x ^ (N.residueDegree : ℤ).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem coe_quotientZeroSubgroupEquivValueSubgroup_norm_mk
    (x : H) :
    ((vG.quotientZeroSubgroupEquivValueSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup (N.toHom x)) : vG.valueSubgroup) :
      Multiplicative ℤ) =
      vH.valuationHom x ^ (N.residueDegree : ℤ)

theorem

toAdd_quotientZeroSubgroupEquivValueSubgroup_norm_mk

L209 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.toAdd_quotientZeroSubgroupEquivValueSubgroup_norm_mk

Documentation

Establishes the identity Multiplicative.toAdd (((vG.quotientZeroSubgroupEquivValueSubgroup (QuotientGroup.mk' vG.zeroSubgroup (N.toHom x)) : vG.valueSubgroup) : Multiplicative ℤ)) = (N.residueDegree : ℤ) * vH.val x.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem toAdd_quotientZeroSubgroupEquivValueSubgroup_norm_mk
    (x : H) :
    Multiplicative.toAdd
      (((vG.quotientZeroSubgroupEquivValueSubgroup
          (QuotientGroup.mk' vG.zeroSubgroup (N.toHom x)) : vG.valueSubgroup) :
        Multiplicative ℤ)) =
      (N.residueDegree : ℤ) * vH.val x

theorem

quotientZeroSubgroup_value_mem_integerMultipleSubgroup_of_mem_normSubgroup

L223 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientZeroSubgroup_value_mem_integerMultipleSubgroup_of_mem_normSubgroup

Documentation

If an element is a norm, then its class modulo valuation-zero elements maps to a residue-degree multiple in the value group.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem quotientZeroSubgroup_value_mem_integerMultipleSubgroup_of_mem_normSubgroup
    {x : G} (hx : x ∈ N.normSubgroup) :
    ((vG.quotientZeroSubgroupEquivValueSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup x) : vG.valueSubgroup) :
      Multiplicative ℤ) ∈
      integerMultipleSubgroup (N.residueDegree : ℤ)

theorem

quotientZeroSubgroup_value_norm_mem_integerMultipleSubgroup

L242 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientZeroSubgroup_value_norm_mem_integerMultipleSubgroup

Documentation

Establishes the membership statement ((vG.quotientZeroSubgroupEquivValueSubgroup (QuotientGroup.mk' vG.zeroSubgroup (N.toHom x)) : vG.valueSubgroup) : Multiplicative ℤ) ∈ integerMultipleSubgroup (N.residueDegree : ℤ).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem quotientZeroSubgroup_value_norm_mem_integerMultipleSubgroup
    (x : H) :
    ((vG.quotientZeroSubgroupEquivValueSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup (N.toHom x)) : vG.valueSubgroup) :
      Multiplicative ℤ) ∈
      integerMultipleSubgroup (N.residueDegree : ℤ)

theorem

quotientZeroSubgroup_value_div_mem_integerMultipleSubgroup_of_div_mem_normSubgroup

L256 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientZeroSubgroup_value_div_mem_integerMultipleSubgroup_of_div_mem_normSubgroup

Documentation

Establishes the membership statement ((vG.quotientZeroSubgroupEquivValueSubgroup (QuotientGroup.mk' vG.zeroSubgroup (x / y)) : vG.valueSubgroup) : Multiplicative ℤ) ∈ integerMultipleSubgroup (N.residueDegree : ℤ).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem quotientZeroSubgroup_value_div_mem_integerMultipleSubgroup_of_div_mem_normSubgroup
    {x y : G} (hxy : x / y ∈ N.normSubgroup) :
    ((vG.quotientZeroSubgroupEquivValueSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup (x / y)) : vG.valueSubgroup) :
      Multiplicative ℤ) ∈
      integerMultipleSubgroup (N.residueDegree : ℤ)

theorem

residueDegree_dvd_valuation_difference_of_div_mem_normSubgroup

L267 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.residueDegree_dvd_valuation_difference_of_div_mem_normSubgroup

Documentation

If a quotient is a norm, then the valuation difference is divisible by the residue degree.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem residueDegree_dvd_valuation_difference_of_div_mem_normSubgroup
    {x y : G} (hxy : x / y ∈ N.normSubgroup) :
    (N.residueDegree : ℤ) ∣ vG.val x - vG.val y

theorem

exists_valuation_difference_eq_residueDegree_mul_of_div_mem_normSubgroup

L275 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.exists_valuation_difference_eq_residueDegree_mul_of_div_mem_normSubgroup

Documentation

Explicit multiple form of residueDegree_dvd_valuation_difference_of_div_mem_normSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem exists_valuation_difference_eq_residueDegree_mul_of_div_mem_normSubgroup
    {x y : G} (hxy : x / y ∈ N.normSubgroup) :
    ∃ n : ℤ, vG.val x - vG.val y = (N.residueDegree : ℤ) * n

theorem

exists_valuation_difference_eq_mul_residueDegree_of_div_mem_normSubgroup

L282 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.exists_valuation_difference_eq_mul_residueDegree_of_div_mem_normSubgroup

Documentation

Right-multiple form of the valuation difference forced by norm-subgroup membership of a quotient.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem exists_valuation_difference_eq_mul_residueDegree_of_div_mem_normSubgroup
    {x y : G} (hxy : x / y ∈ N.normSubgroup) :
    ∃ n : ℤ, vG.val x - vG.val y = n * (N.residueDegree : ℤ)

theorem

valuation_difference_eq_residueDegree_mul_of_norm_eq_div

L292 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.valuation_difference_eq_residueDegree_mul_of_norm_eq_div

Documentation

If a quotient is represented by the norm of a specific element, its valuation difference is computed by that element's valuation.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem valuation_difference_eq_residueDegree_mul_of_norm_eq_div
    {x y : G} {z : H} (hz : N.toHom z = x / y) :
    vG.val x - vG.val y = (N.residueDegree : ℤ) * vH.val z

theorem

valuation_difference_eq_mul_residueDegree_of_norm_eq_div

L302 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.valuation_difference_eq_mul_residueDegree_of_norm_eq_div

Documentation

Right-multiple form of valuation_difference_eq_residueDegree_mul_of_norm_eq_div.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem valuation_difference_eq_mul_residueDegree_of_norm_eq_div
    {x y : G} {z : H} (hz : N.toHom z = x / y) :
    vG.val x - vG.val y = vH.val z * (N.residueDegree : ℤ)

theorem

exists_zeroSubgroup_mul_norm_uniformizer_zpow_eq_of_mem_normSubgroup

L311 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.exists_zeroSubgroup_mul_norm_uniformizer_zpow_eq_of_mem_normSubgroup

Documentation

A norm-subgroup element is a valuation-zero factor times the norm of a source-uniformizer power. This is the abstract normal form behind local CFT norm quotient calculations; no surjectivity on units is assumed.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem exists_zeroSubgroup_mul_norm_uniformizer_zpow_eq_of_mem_normSubgroup
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    {x : G} (hx : x ∈ N.normSubgroup) :
    ∃ u : G, u ∈ vG.zeroSubgroup ∧
      ∃ n : ℤ, x = u * N.toHom (ϖH ^ n)

theorem

mem_normSubgroup_of_residueDegree_dvd_val_of_zeroSubgroup_le

L326 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.mem_normSubgroup_of_residueDegree_dvd_val_of_zeroSubgroup_le

Documentation

If all valuation-zero target elements are norms and the source valuation has a uniformizer, valuation divisibility by the residue degree is sufficient for norm-subgroup membership.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem mem_normSubgroup_of_residueDegree_dvd_val_of_zeroSubgroup_le
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup)
    {x : G} (hx : (N.residueDegree : ℤ) ∣ vG.val x) :
    x ∈ N.normSubgroup

theorem

mem_normSubgroup_iff_residueDegree_dvd_val_of_zeroSubgroup_le

L345 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.mem_normSubgroup_iff_residueDegree_dvd_val_of_zeroSubgroup_le

Documentation

With source uniformizer and norm-surjectivity on valuation-zero target elements, the norm subgroup is exactly the elements whose valuation is divisible by the residue degree.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem mem_normSubgroup_iff_residueDegree_dvd_val_of_zeroSubgroup_le
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) :
    x ∈ N.normSubgroup ↔ (N.residueDegree : ℤ) ∣ vG.val x

theorem

div_mem_normSubgroup_iff_residueDegree_dvd_valuation_difference_of_zeroSubgroup_le

L356 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.div_mem_normSubgroup_iff_residueDegree_dvd_valuation_difference_of_zeroSubgroup_le

Documentation

Quotient form of mem_normSubgroup_iff_residueDegree_dvd_val_of_zeroSubgroup_le.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem div_mem_normSubgroup_iff_residueDegree_dvd_valuation_difference_of_zeroSubgroup_le
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x y : G) :
    x / y ∈ N.normSubgroup ↔
      (N.residueDegree : ℤ) ∣ vG.val x - vG.val y

theorem

div_mem_normSubgroup_iff_inv_mul_mem_normSubgroup

L367 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.div_mem_normSubgroup_iff_inv_mul_mem_normSubgroup

Documentation

In a normal norm subgroup, the right quotient x / y and the left quotient y⁻¹ * x give the same membership test.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem div_mem_normSubgroup_iff_inv_mul_mem_normSubgroup
    [(N.normSubgroup).Normal] (x y : G) :
    x / y ∈ N.normSubgroup ↔ y⁻¹ * x ∈ N.normSubgroup

theorem

inv_mul_mem_normSubgroup_iff_div_mem_normSubgroup

L376 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.inv_mul_mem_normSubgroup_iff_div_mem_normSubgroup

Documentation

Left-quotient version of div_mem_normSubgroup_iff_inv_mul_mem_normSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem inv_mul_mem_normSubgroup_iff_div_mem_normSubgroup
    [(N.normSubgroup).Normal] (x y : G) :
    y⁻¹ * x ∈ N.normSubgroup ↔ x / y ∈ N.normSubgroup

theorem

inv_mul_mem_normSubgroup_iff_residueDegree_dvd_valuation_difference_of_zeroSubgroup_le

L383 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.inv_mul_mem_normSubgroup_iff_residueDegree_dvd_valuation_difference_of_zeroSubgroup_le

Documentation

Left-quotient form of residue-degree divisibility for norm-subgroup membership.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem inv_mul_mem_normSubgroup_iff_residueDegree_dvd_valuation_difference_of_zeroSubgroup_le
    [(N.normSubgroup).Normal]
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x y : G) :
    y⁻¹ * x ∈ N.normSubgroup ↔
      (N.residueDegree : ℤ) ∣ vG.val x - vG.val y

def

valueModResidueDegreeHom

L396 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.valueModResidueDegreeHom

Documentation

The valuation map modulo the residue-degree multiple subgroup. This is the canonical value-group map used to compare norm quotients with ℤ / fℤ.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

def valueModResidueDegreeHom :
    G →* Multiplicative ℤ ⧸ integerMultipleSubgroup (N.residueDegree : ℤ)

theorem

valueModResidueDegreeHom_apply

L406 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.valueModResidueDegreeHom_apply

Documentation

The defining evaluation formula for valueModResidueDegreeHom is N.valueModResidueDegreeHom x = QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ)) (vG.valuationHom x).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem valueModResidueDegreeHom_apply (x : G) :
    N.valueModResidueDegreeHom x =
      QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ))
        (vG.valuationHom x)

theorem

valueModResidueDegreeHom_apply_ofAdd

L416 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.valueModResidueDegreeHom_apply_ofAdd

Documentation

Establishes the identity N.valueModResidueDegreeHom x = QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ)) (Multiplicative.ofAdd (vG.val x)).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem valueModResidueDegreeHom_apply_ofAdd (x : G) :
    N.valueModResidueDegreeHom x =
      QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ))
        (Multiplicative.ofAdd (vG.val x))

theorem

valueModResidueDegreeHom_surjective_of_uniformizer

L424 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.valueModResidueDegreeHom_surjective_of_uniformizer

Documentation

The specified map is surjective: Function.Surjective N.valueModResidueDegreeHom.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem valueModResidueDegreeHom_surjective_of_uniformizer
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) :
    Function.Surjective N.valueModResidueDegreeHom

theorem

mem_valueModResidueDegreeHom_ker_iff

L442 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.mem_valueModResidueDegreeHom_ker_iff

Documentation

Characterizes x ∈ N.valueModResidueDegreeHom.ker by the equivalent condition (N.residueDegree : ℤ) ∣ vG.val x.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem mem_valueModResidueDegreeHom_ker_iff (x : G) :
    x ∈ N.valueModResidueDegreeHom.ker ↔
      (N.residueDegree : ℤ) ∣ vG.val x

def

zeroSubgroupQuotientToValueModResidueDegree

L453 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToValueModResidueDegree

Documentation

The map G/G⁰ → ℤ/fℤ induced by valuation modulo the residue-degree multiple subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

def zeroSubgroupQuotientToValueModResidueDegree :
    G ⧸ vG.zeroSubgroup →*
      Multiplicative ℤ ⧸ integerMultipleSubgroup (N.residueDegree : ℤ)

theorem

zeroSubgroupQuotientToValueModResidueDegree_mk

L471 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToValueModResidueDegree_mk

Documentation

Establishes the identity N.zeroSubgroupQuotientToValueModResidueDegree (QuotientGroup.mk' vG.zeroSubgroup x) = QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ)) (vG.valuationHom x).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToValueModResidueDegree_mk (x : G) :
    N.zeroSubgroupQuotientToValueModResidueDegree
        (QuotientGroup.mk' vG.zeroSubgroup x) =
      QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ))
        (vG.valuationHom x)

theorem

zeroSubgroupQuotientToValueModResidueDegree_mk_ofAdd

L483 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToValueModResidueDegree_mk_ofAdd

Documentation

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToValueModResidueDegree_mk_ofAdd (x : G) :
    N.zeroSubgroupQuotientToValueModResidueDegree
        (QuotientGroup.mk' vG.zeroSubgroup x) =
      QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ))
        (Multiplicative.ofAdd (vG.val x))

theorem

zeroSubgroupQuotientToValueModResidueDegree_surjective_of_uniformizer

L495 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToValueModResidueDegree_surjective_of_uniformizer

Documentation

The specified map is surjective: Function.Surjective N.zeroSubgroupQuotientToValueModResidueDegree.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToValueModResidueDegree_surjective_of_uniformizer
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) :
    Function.Surjective N.zeroSubgroupQuotientToValueModResidueDegree

theorem

zeroSubgroupQuotientToValueModResidueDegree_mk_eq_one_iff

L514 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToValueModResidueDegree_mk_eq_one_iff

Documentation

Characterizes N.zeroSubgroupQuotientToValueModResidueDegree (QuotientGroup.mk' vG.zeroSubgroup x) = 1 by the equivalent condition (N.residueDegree : ℤ) ∣ vG.val x.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToValueModResidueDegree_mk_eq_one_iff
    (x : G) :
    N.zeroSubgroupQuotientToValueModResidueDegree
        (QuotientGroup.mk' vG.zeroSubgroup x) = 1 ↔
      (N.residueDegree : ℤ) ∣ vG.val x

theorem

zeroSubgroupQuotientToValueModResidueDegree_mk_eq_iff

L528 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToValueModResidueDegree_mk_eq_iff

Documentation

Characterizes N.zeroSubgroupQuotientToValueModResidueDegree (QuotientGroup.mk' vG.zeroSubgroup x) = N.zeroSubgroupQuotientToValueModResidueDegree (QuotientGroup.mk' vG.zeroSubgroup y) by the equivalent condition (N.residueDegree : ℤ) ∣ vG.val x - vG.val y.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToValueModResidueDegree_mk_eq_iff
    (x y : G) :
    N.zeroSubgroupQuotientToValueModResidueDegree
        (QuotientGroup.mk' vG.zeroSubgroup x) =
      N.zeroSubgroupQuotientToValueModResidueDegree
        (QuotientGroup.mk' vG.zeroSubgroup y) ↔
      (N.residueDegree : ℤ) ∣ vG.val x - vG.val y

theorem

valueModResidueDegreeHom_ker_eq_valuationHom_comap

L550 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.valueModResidueDegreeHom_ker_eq_valuationHom_comap

Documentation

Establishes the identity N.valueModResidueDegreeHom.ker = (integerMultipleSubgroup (N.residueDegree : ℤ)).comap vG.valuationHom.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem valueModResidueDegreeHom_ker_eq_valuationHom_comap :
    N.valueModResidueDegreeHom.ker =
      (integerMultipleSubgroup (N.residueDegree : ℤ)).comap
        vG.valuationHom

def

residueDegreeClassSubgroup

L563 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.residueDegreeClassSubgroup

Documentation

The subgroup of G/G⁰ consisting of classes whose value is divisible by the residue degree. This is the kernel of the value-mod-residue-degree map.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

def residueDegreeClassSubgroup :
    Subgroup (G ⧸ vG.zeroSubgroup)

instance

residueDegreeClassSubgroup_normal

L569 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.residueDegreeClassSubgroup_normal

Documentation

The subgroup appearing in N.residueDegreeClassSubgroup.Normal is normal.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

instance residueDegreeClassSubgroup_normal :
    N.residueDegreeClassSubgroup.Normal

theorem

mem_residueDegreeClassSubgroup_iff

L578 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.mem_residueDegreeClassSubgroup_iff

Documentation

Characterizes q ∈ N.residueDegreeClassSubgroup by the equivalent condition ∃ x : G, x ∈ N.valueModResidueDegreeHom.ker ∧ QuotientGroup.mk' vG.zeroSubgroup x = q.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem mem_residueDegreeClassSubgroup_iff
    (q : G ⧸ vG.zeroSubgroup) :
    q ∈ N.residueDegreeClassSubgroup ↔
      ∃ x : G, x ∈ N.valueModResidueDegreeHom.ker ∧
        QuotientGroup.mk' vG.zeroSubgroup x = q

theorem

residueDegreeClassSubgroup_mk_mem

L589 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.residueDegreeClassSubgroup_mk_mem

Documentation

Establishes the membership statement QuotientGroup.mk' vG.zeroSubgroup x ∈ N.residueDegreeClassSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem residueDegreeClassSubgroup_mk_mem {x : G}
    (hx : (N.residueDegree : ℤ) ∣ vG.val x) :
    QuotientGroup.mk' vG.zeroSubgroup x ∈
      N.residueDegreeClassSubgroup

theorem

zeroSubgroupQuotientToValueModResidueDegree_ker_eq_residueDegreeClassSubgroup

L600 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToValueModResidueDegree_ker_eq_residueDegreeClassSubgroup

Documentation

Establishes the identity N.zeroSubgroupQuotientToValueModResidueDegree.ker = N.residueDegreeClassSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToValueModResidueDegree_ker_eq_residueDegreeClassSubgroup :
    N.zeroSubgroupQuotientToValueModResidueDegree.ker =
      N.residueDegreeClassSubgroup

theorem

mem_zeroSubgroupQuotientToValueModResidueDegree_ker_iff

L611 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.mem_zeroSubgroupQuotientToValueModResidueDegree_ker_iff

Documentation

Characterizes q ∈ N.zeroSubgroupQuotientToValueModResidueDegree.ker by the equivalent condition q ∈ N.residueDegreeClassSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem mem_zeroSubgroupQuotientToValueModResidueDegree_ker_iff
    (q : G ⧸ vG.zeroSubgroup) :
    q ∈ N.zeroSubgroupQuotientToValueModResidueDegree.ker ↔
      q ∈ N.residueDegreeClassSubgroup

theorem

quotientZeroSubgroup_mk_mem_residueDegreeClassSubgroup_iff

L621 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientZeroSubgroup_mk_mem_residueDegreeClassSubgroup_iff

Documentation

Characterizes QuotientGroup.mk' vG.zeroSubgroup x ∈ N.residueDegreeClassSubgroup by the equivalent condition (N.residueDegree : ℤ) ∣ vG.val x.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem quotientZeroSubgroup_mk_mem_residueDegreeClassSubgroup_iff
    (x : G) :
    QuotientGroup.mk' vG.zeroSubgroup x ∈
        N.residueDegreeClassSubgroup ↔
      (N.residueDegree : ℤ) ∣ vG.val x

theorem

zeroSubgroupQuotientToValueModResidueDegree_eq_one_iff_mem_residueDegreeClassSubgroup

L635 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToValueModResidueDegree_eq_one_iff_mem_residueDegreeClassSubgroup

Documentation

Characterizes N.zeroSubgroupQuotientToValueModResidueDegree q = 1 by the equivalent condition q ∈ N.residueDegreeClassSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToValueModResidueDegree_eq_one_iff_mem_residueDegreeClassSubgroup
    (q : G ⧸ vG.zeroSubgroup) :
    N.zeroSubgroupQuotientToValueModResidueDegree q = 1 ↔
      q ∈ N.residueDegreeClassSubgroup

theorem

zeroSubgroupQuotientToValueModResidueDegree_eq_one_iff_exists_residueDegree_repr

L646 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToValueModResidueDegree_eq_one_iff_exists_residueDegree_repr

Documentation

Characterizes N.zeroSubgroupQuotientToValueModResidueDegree q = 1 by the equivalent condition ∃ x : G, (N.residueDegree : ℤ) ∣ vG.val x ∧ QuotientGroup.mk' vG.zeroSubgroup x = q.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToValueModResidueDegree_eq_one_iff_exists_residueDegree_repr
    (q : G ⧸ vG.zeroSubgroup) :
    N.zeroSubgroupQuotientToValueModResidueDegree q = 1 ↔
      ∃ x : G, (N.residueDegree : ℤ) ∣ vG.val x ∧
        QuotientGroup.mk' vG.zeroSubgroup x = q

theorem

zeroSubgroupQuotientToValueModResidueDegree_eq_iff_div_mem_residueDegreeClassSubgroup

L665 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToValueModResidueDegree_eq_iff_div_mem_residueDegreeClassSubgroup

Documentation

Characterizes N.zeroSubgroupQuotientToValueModResidueDegree q = N.zeroSubgroupQuotientToValueModResidueDegree r by the equivalent condition q / r ∈ N.residueDegreeClassSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToValueModResidueDegree_eq_iff_div_mem_residueDegreeClassSubgroup
    (q r : G ⧸ vG.zeroSubgroup) :
    N.zeroSubgroupQuotientToValueModResidueDegree q =
        N.zeroSubgroupQuotientToValueModResidueDegree r ↔
      q / r ∈ N.residueDegreeClassSubgroup

def

zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree

L677 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree

Documentation

First-isomorphism form of the value-mod-residue-degree map. A target uniformizer makes G/G⁰ → ℤ/fℤ surjective.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

def zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) :
    (G ⧸ vG.zeroSubgroup) ⧸ N.residueDegreeClassSubgroup ≃*
      Multiplicative ℤ ⧸ integerMultipleSubgroup (N.residueDegree : ℤ)

theorem

zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_mk

L692 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_mk

Documentation

Establishes the identity N.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree hϖG (QuotientGroup.mk' N.residueDegreeClassSubgroup q) = N.zeroSubgroupQuotientToValueModResidueDegree q.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_mk
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    (q : G ⧸ vG.zeroSubgroup) :
    N.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree hϖG
        (QuotientGroup.mk' N.residueDegreeClassSubgroup q) =
      N.zeroSubgroupQuotientToValueModResidueDegree q

theorem

zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_mk_mk

L711 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_mk_mk

Documentation

Establishes the identity N.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree hϖG (QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup x)) = QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ)) (Multiplicative.ofAdd (vG.val x)).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_mk_mk
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) (x : G) :
    N.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree hϖG
        (QuotientGroup.mk' N.residueDegreeClassSubgroup
          (QuotientGroup.mk' vG.zeroSubgroup x)) =
      QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ))
        (Multiplicative.ofAdd (vG.val x))

theorem

zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_symm_mk_val

L727 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_symm_mk_val

Documentation

Establishes the identity (N.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree hϖG).symm (QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ)) (Multiplicative.ofAdd (vG.val x))) = QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup x).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_symm_mk_val
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) (x : G) :
    (N.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree hϖG).symm
        (QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ))
          (Multiplicative.ofAdd (vG.val x))) =
      QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup x)

theorem

zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_symm_mk_ofAdd

L757 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_symm_mk_ofAdd

Documentation

Establishes the identity (N.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree hϖG).symm (QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ)) (Multiplicative.ofAdd n)) = QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup (ϖG ^ n)).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_symm_mk_ofAdd
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) (n : ℤ) :
    (N.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree hϖG).symm
        (QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ))
          (Multiplicative.ofAdd n)) =
      QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup (ϖG ^ n))

theorem

zeroQuotientModuloResidueDegreeClass_mk_eq_one_iff

L771 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClass_mk_eq_one_iff

Documentation

One criterion in the double quotient by the residue-degree class subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClass_mk_eq_one_iff
    (q : G ⧸ vG.zeroSubgroup) :
    QuotientGroup.mk' N.residueDegreeClassSubgroup q = 1 ↔
      q ∈ N.residueDegreeClassSubgroup

theorem

zeroQuotientModuloResidueDegreeClass_mk_mk_eq_one_iff

L781 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClass_mk_mk_eq_one_iff

Documentation

Characterizes QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup x) = 1 by the equivalent condition (N.residueDegree : ℤ) ∣ vG.val x.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClass_mk_mk_eq_one_iff
    (x : G) :
    QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup x) = 1 ↔
      (N.residueDegree : ℤ) ∣ vG.val x

theorem

zeroQuotientModuloResidueDegreeClass_mk_eq_iff_div_mem

L791 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClass_mk_eq_iff_div_mem

Documentation

Equality criterion in the double quotient by the residue-degree class subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClass_mk_eq_iff_div_mem
    (q r : G ⧸ vG.zeroSubgroup) :
    QuotientGroup.mk' N.residueDegreeClassSubgroup q =
        QuotientGroup.mk' N.residueDegreeClassSubgroup r ↔
      q / r ∈ N.residueDegreeClassSubgroup

theorem

zeroQuotientModuloResidueDegreeClass_mk_mk_eq_iff_residueDegree_dvd

L805 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClass_mk_mk_eq_iff_residueDegree_dvd

Documentation

Characterizes QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup x) = QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup y) by the equivalent condition (N.residueDegree : ℤ) ∣ vG.val x - vG.val y.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClass_mk_mk_eq_iff_residueDegree_dvd
    (x y : G) :
    QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup x) =
      QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup y) ↔
      (N.residueDegree : ℤ) ∣ vG.val x - vG.val y

theorem

zeroQuotientModuloResidueDegreeClass_uniformizer_zpow_mk_eq_iff

L822 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClass_uniformizer_zpow_mk_eq_iff

Documentation

Characterizes QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup (ϖG ^ m)) = QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup (ϖG ^ n)) by the equivalent condition (N.residueDegree : ℤ) ∣ m - n.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClass_uniformizer_zpow_mk_eq_iff
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) (m n : ℤ) :
    QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup (ϖG ^ m)) =
      QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup (ϖG ^ n)) ↔
      (N.residueDegree : ℤ) ∣ m - n

theorem

zeroQuotientModuloResidueDegreeClass_uniformizer_zpow_mk_eq_of_sub_dvd

L837 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClass_uniformizer_zpow_mk_eq_of_sub_dvd

Documentation

Establishes the identity QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup (ϖG ^ m)) = QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup (ϖG ^ n)).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClass_uniformizer_zpow_mk_eq_of_sub_dvd
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) {m n : ℤ}
    (hmn : (N.residueDegree : ℤ) ∣ m - n) :
    QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup (ϖG ^ m)) =
      QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup (ϖG ^ n))

theorem

zeroQuotientModuloResidueDegreeClass_uniformizer_zpow_mk_eq_one_iff

L851 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClass_uniformizer_zpow_mk_eq_one_iff

Documentation

Characterizes QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup (ϖG ^ n)) = 1 by the equivalent condition (N.residueDegree : ℤ) ∣ n.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClass_uniformizer_zpow_mk_eq_one_iff
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) (n : ℤ) :
    QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup (ϖG ^ n)) = 1 ↔
      (N.residueDegree : ℤ) ∣ n

theorem

residueDegree_dvd_add_residueDegree_mul_sub

L863 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.residueDegree_dvd_add_residueDegree_mul_sub

Documentation

Establishes the divisibility statement (N.residueDegree : ℤ) ∣ (n + (N.residueDegree : ℤ) * k) - n.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem residueDegree_dvd_add_residueDegree_mul_sub (n k : ℤ) :
    (N.residueDegree : ℤ) ∣
      (n + (N.residueDegree : ℤ) * k) - n

theorem

valueModResidueDegreeHom_uniformizer_zpow_add_residueDegree_mul_eq

L871 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.valueModResidueDegreeHom_uniformizer_zpow_add_residueDegree_mul_eq

Documentation

The value-mod-residue-degree map is periodic on target-uniformizer powers with period the residue degree.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem valueModResidueDegreeHom_uniformizer_zpow_add_residueDegree_mul_eq
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) (n k : ℤ) :
    N.valueModResidueDegreeHom
        (ϖG ^ (n + (N.residueDegree : ℤ) * k)) =
      N.valueModResidueDegreeHom (ϖG ^ n)

theorem

zeroSubgroupQuotientToValueModResidueDegree_uniformizer_zpow_add_residueDegree_mul_mk_eq

L890 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToValueModResidueDegree_uniformizer_zpow_add_residueDegree_mul_mk_eq

Documentation

The map G/G⁰ → ℤ/fℤ induced by valuation is periodic on target-uniformizer powers with period the residue degree.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToValueModResidueDegree_uniformizer_zpow_add_residueDegree_mul_mk_eq
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) (n k : ℤ) :
    N.zeroSubgroupQuotientToValueModResidueDegree
        (QuotientGroup.mk' vG.zeroSubgroup
          (ϖG ^ (n + (N.residueDegree : ℤ) * k))) =
      N.zeroSubgroupQuotientToValueModResidueDegree
        (QuotientGroup.mk' vG.zeroSubgroup (ϖG ^ n))

theorem

zeroQuotientModuloResidueDegreeClass_uniformizer_zpow_add_residueDegree_mul_mk_eq

L904 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClass_uniformizer_zpow_add_residueDegree_mul_mk_eq

Documentation

Uniformizer powers in the residue-degree double quotient are periodic modulo the residue degree.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClass_uniformizer_zpow_add_residueDegree_mul_mk_eq
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) (n k : ℤ) :
    QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup
          (ϖG ^ (n + (N.residueDegree : ℤ) * k))) =
      QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup (ϖG ^ n))

theorem

zeroQuotientModuloResidueDegreeClass_mk_eq_uniformizer_zpow_val

L916 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClass_mk_eq_uniformizer_zpow_val

Documentation

Every residue-degree double-quotient class has the same representative as a target-uniformizer power with exponent given by the valuation.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClass_mk_eq_uniformizer_zpow_val
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) (x : G) :
    QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup x) =
      QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup (ϖG ^ vG.val x))

theorem

zeroQuotientModuloResidueDegreeClass_mk_eq_uniformizerClass_zpow_val

L928 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClass_mk_eq_uniformizerClass_zpow_val

Documentation

Generator-power form of zeroQuotientModuloResidueDegreeClass_mk_eq_uniformizer_zpow_val.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClass_mk_eq_uniformizerClass_zpow_val
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) (x : G) :
    QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup x) =
      (QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ vG.val x

theorem

zeroQuotientModuloResidueDegreeClass_mk_eq_uniformizerClass_zpow_iff

L942 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClass_mk_eq_uniformizerClass_zpow_iff

Documentation

Criterion for a residue-degree double-quotient class to be a prescribed power of the target uniformizer class.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClass_mk_eq_uniformizerClass_zpow_iff
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) (x : G) (n : ℤ) :
    QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup x) =
      (QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n ↔
      (N.residueDegree : ℤ) ∣ vG.val x - n

theorem

zeroQuotientModuloResidueDegreeClass_uniformizerClass_zpow_eq_iff

L957 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClass_uniformizerClass_zpow_eq_iff

Documentation

Equality of two powers of the target uniformizer class in the residue-degree double quotient is residue-degree divisibility of the exponent difference.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClass_uniformizerClass_zpow_eq_iff
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) (m n : ℤ) :
    (QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ m =
      (QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n ↔
      (N.residueDegree : ℤ) ∣ m - n

theorem

zeroQuotientModuloResidueDegreeClass_uniformizerClass_zpow_eq_of_sub_dvd

L978 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClass_uniformizerClass_zpow_eq_of_sub_dvd

Documentation

Establishes the identity (QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ m = (QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClass_uniformizerClass_zpow_eq_of_sub_dvd
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) {m n : ℤ}
    (hmn : (N.residueDegree : ℤ) ∣ m - n) :
    (QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ m =
      (QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n

theorem

zeroQuotientModuloResidueDegreeClass_uniformizerClass_zpow_add_residueDegree_mul_eq

L993 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClass_uniformizerClass_zpow_add_residueDegree_mul_eq

Documentation

Establishes the identity (QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ (n + (N.residueDegree : ℤ) * k) = (QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClass_uniformizerClass_zpow_add_residueDegree_mul_eq
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) (n k : ℤ) :
    (QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^
        (n + (N.residueDegree : ℤ) * k) =
      (QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n

theorem

zeroQuotientModuloResidueDegreeClass_uniformizerClass_zpow_residueDegree_eq_one

L1007 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClass_uniformizerClass_zpow_residueDegree_eq_one

Documentation

Establishes the identity (QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ (N.residueDegree : ℤ) = 1.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClass_uniformizerClass_zpow_residueDegree_eq_one
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) :
    (QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ (N.residueDegree : ℤ) = 1

theorem

zeroQuotientModuloResidueDegreeClass_uniformizerClass_zpow_eq_one_iff

L1022 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClass_uniformizerClass_zpow_eq_one_iff

Documentation

Characterizes (QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n = 1 by the equivalent condition (N.residueDegree : ℤ) ∣ n.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClass_uniformizerClass_zpow_eq_one_iff
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) (n : ℤ) :
    (QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n = 1 ↔
      (N.residueDegree : ℤ) ∣ n

theorem

zeroQuotientModuloResidueDegreeClass_generated_by_uniformizerClass

L1035 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClass_generated_by_uniformizerClass

Documentation

The residue-degree double quotient is generated by the class of any target uniformizer.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClass_generated_by_uniformizerClass
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    (q : (G ⧸ vG.zeroSubgroup) ⧸ N.residueDegreeClassSubgroup) :
    ∃ n : ℤ, q =
      (QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n

theorem

zeroQuotientModuloResidueDegreeClass_closure_uniformizerClass_eq_top

L1051 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClass_closure_uniformizerClass_eq_top

Documentation

The residue-degree double quotient is cyclic, generated by the class of any target uniformizer.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClass_closure_uniformizerClass_eq_top
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) :
    Subgroup.closure
        (Set.singleton (QuotientGroup.mk' N.residueDegreeClassSubgroup
          (QuotientGroup.mk' vG.zeroSubgroup ϖG)) :
          Set ((G ⧸ vG.zeroSubgroup) ⧸ N.residueDegreeClassSubgroup)) =
      ⊤

theorem

zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_uniformizerClass_zpow

L1077 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_uniformizerClass_zpow

Documentation

zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_uniformizerClass satisfies the integer-power formula N.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree hϖG ((QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n) = QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ)) (Multiplicative.ofAdd n).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_uniformizerClass_zpow
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) (n : ℤ) :
    N.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree hϖG
        ((QuotientGroup.mk' N.residueDegreeClassSubgroup
          (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n) =
      QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ))
        (Multiplicative.ofAdd n)

theorem

zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_symm_mk_ofAdd_uniformizerClass_zpow

L1099 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_symm_mk_ofAdd_uniformizerClass_zpow

Documentation

zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_symm_mk_ofAdd_uniformizerClass satisfies the integer-power formula (N.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree hϖG).symm (QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ)) (Multiplicative.ofAdd n)) = (QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem
zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_symm_mk_ofAdd_uniformizerClass_zpow
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG) (n : ℤ) :
    (N.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree hϖG).symm
        (QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ))
          (Multiplicative.ofAdd n)) =
      (QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n

theorem

valueModResidueDegreeHom_ker_eq_normSubgroup_of_zeroSubgroup_le

L1114 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.valueModResidueDegreeHom_ker_eq_normSubgroup_of_zeroSubgroup_le

Documentation

Establishes the identity N.valueModResidueDegreeHom.ker = N.normSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem valueModResidueDegreeHom_ker_eq_normSubgroup_of_zeroSubgroup_le
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) :
    N.valueModResidueDegreeHom.ker = N.normSubgroup

def

normSubgroupClassInZeroQuotient

L1125 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normSubgroupClassInZeroQuotient

Documentation

The subgroup N/G⁰ inside the zero-valuation quotient G/G⁰, where N is the norm subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

def normSubgroupClassInZeroQuotient : Subgroup (G ⧸ vG.zeroSubgroup)

instance

normSubgroupClassInZeroQuotient_normal

L1129 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normSubgroupClassInZeroQuotient_normal

Documentation

The subgroup appearing in N.normSubgroupClassInZeroQuotient.Normal is normal.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

instance normSubgroupClassInZeroQuotient_normal
    [(N.normSubgroup).Normal] :
    N.normSubgroupClassInZeroQuotient.Normal

theorem

mem_normSubgroupClassInZeroQuotient_iff

L1139 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.mem_normSubgroupClassInZeroQuotient_iff

Documentation

Characterizes q ∈ N.normSubgroupClassInZeroQuotient by the equivalent condition ∃ x : G, x ∈ N.normSubgroup ∧ QuotientGroup.mk' vG.zeroSubgroup x = q.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem mem_normSubgroupClassInZeroQuotient_iff
    (q : G ⧸ vG.zeroSubgroup) :
    q ∈ N.normSubgroupClassInZeroQuotient ↔
      ∃ x : G, x ∈ N.normSubgroup ∧
        QuotientGroup.mk' vG.zeroSubgroup x = q

theorem

normSubgroupClassInZeroQuotient_mk_mem

L1150 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normSubgroupClassInZeroQuotient_mk_mem

Documentation

Establishes the membership statement QuotientGroup.mk' vG.zeroSubgroup x ∈ N.normSubgroupClassInZeroQuotient.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normSubgroupClassInZeroQuotient_mk_mem {x : G}
    (hx : x ∈ N.normSubgroup) :
    QuotientGroup.mk' vG.zeroSubgroup x ∈
      N.normSubgroupClassInZeroQuotient

theorem

residueDegreeClassSubgroup_eq_normSubgroupClassInZeroQuotient_of_zeroSubgroup_le

L1157 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.residueDegreeClassSubgroup_eq_normSubgroupClassInZeroQuotient_of_zeroSubgroup_le

Documentation

Establishes the identity N.residueDegreeClassSubgroup = N.normSubgroupClassInZeroQuotient.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem residueDegreeClassSubgroup_eq_normSubgroupClassInZeroQuotient_of_zeroSubgroup_le
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) :
    N.residueDegreeClassSubgroup =
      N.normSubgroupClassInZeroQuotient

def

zeroQuotientModuloResidueDegreeClassEquivNormClass

L1169 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivNormClass

Documentation

The quotient by the value-side residue-degree class subgroup is the same as the quotient by the norm-class subgroup when valuation-zero target elements are norms.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

def zeroQuotientModuloResidueDegreeClassEquivNormClass
    [(N.normSubgroup).Normal]
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) :
    (G ⧸ vG.zeroSubgroup) ⧸ N.residueDegreeClassSubgroup ≃*
      (G ⧸ vG.zeroSubgroup) ⧸ N.normSubgroupClassInZeroQuotient

theorem

zeroQuotientModuloResidueDegreeClassEquivNormClass_mk

L1184 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivNormClass_mk

Documentation

Establishes the identity N.zeroQuotientModuloResidueDegreeClassEquivNormClass hϖH hzero (QuotientGroup.mk' N.residueDegreeClassSubgroup q) = QuotientGroup.mk' N.normSubgroupClassInZeroQuotient q.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClassEquivNormClass_mk
    [(N.normSubgroup).Normal]
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup)
    (q : G ⧸ vG.zeroSubgroup) :
    N.zeroQuotientModuloResidueDegreeClassEquivNormClass hϖH hzero
        (QuotientGroup.mk' N.residueDegreeClassSubgroup q) =
      QuotientGroup.mk' N.normSubgroupClassInZeroQuotient q

theorem

zeroQuotientModuloResidueDegreeClassEquivNormClass_mk_mk

L1199 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivNormClass_mk_mk

Documentation

Establishes the identity N.zeroQuotientModuloResidueDegreeClassEquivNormClass hϖH hzero (QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup x)) = QuotientGroup.mk' N.normSubgroupClassInZeroQuotient (QuotientGroup.mk' vG.zeroSubgroup x).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClassEquivNormClass_mk_mk
    [(N.normSubgroup).Normal]
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) :
    N.zeroQuotientModuloResidueDegreeClassEquivNormClass hϖH hzero
        (QuotientGroup.mk' N.residueDegreeClassSubgroup
          (QuotientGroup.mk' vG.zeroSubgroup x)) =
      QuotientGroup.mk' N.normSubgroupClassInZeroQuotient
        (QuotientGroup.mk' vG.zeroSubgroup x)

theorem

zeroQuotientModuloResidueDegreeClassEquivNormClass_symm_mk

L1215 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivNormClass_symm_mk

Documentation

Establishes the identity (N.zeroQuotientModuloResidueDegreeClassEquivNormClass hϖH hzero).symm (QuotientGroup.mk' N.normSubgroupClassInZeroQuotient q) = QuotientGroup.mk' N.residueDegreeClassSubgroup q.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClassEquivNormClass_symm_mk
    [(N.normSubgroup).Normal]
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup)
    (q : G ⧸ vG.zeroSubgroup) :
    (N.zeroQuotientModuloResidueDegreeClassEquivNormClass hϖH hzero).symm
        (QuotientGroup.mk' N.normSubgroupClassInZeroQuotient q) =
      QuotientGroup.mk' N.residueDegreeClassSubgroup q

theorem

zeroQuotientModuloResidueDegreeClassEquivNormClass_symm_mk_mk

L1241 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivNormClass_symm_mk_mk

Documentation

Establishes the identity (N.zeroQuotientModuloResidueDegreeClassEquivNormClass hϖH hzero).symm (QuotientGroup.mk' N.normSubgroupClassInZeroQuotient (QuotientGroup.mk' vG.zeroSubgroup x)) = QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup x).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClassEquivNormClass_symm_mk_mk
    [(N.normSubgroup).Normal]
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) :
    (N.zeroQuotientModuloResidueDegreeClassEquivNormClass hϖH hzero).symm
        (QuotientGroup.mk' N.normSubgroupClassInZeroQuotient
          (QuotientGroup.mk' vG.zeroSubgroup x)) =
      QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup x)

theorem

zeroQuotientModuloResidueDegreeClassEquivNormClass_uniformizerClass_zpow

L1258 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivNormClass_uniformizerClass_zpow

Documentation

zeroQuotientModuloResidueDegreeClassEquivNormClass_uniformizerClass satisfies the integer-power formula N.zeroQuotientModuloResidueDegreeClassEquivNormClass hϖH hzero ((QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n) = (QuotientGroup.mk' N.normSubgroupClassInZeroQuotient (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClassEquivNormClass_uniformizerClass_zpow
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (n : ℤ) :
    N.zeroQuotientModuloResidueDegreeClassEquivNormClass hϖH hzero
        ((QuotientGroup.mk' N.residueDegreeClassSubgroup
          (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n) =
      (QuotientGroup.mk' N.normSubgroupClassInZeroQuotient
        (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n

theorem

zeroQuotientModuloResidueDegreeClassEquivNormClass_symm_uniformizerClass_zpow

L1283 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivNormClass_symm_uniformizerClass_zpow

Documentation

zeroQuotientModuloResidueDegreeClassEquivNormClass_symm_uniformizerClass satisfies the integer-power formula (N.zeroQuotientModuloResidueDegreeClassEquivNormClass hϖH hzero).symm ((QuotientGroup.mk' N.normSubgroupClassInZeroQuotient (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n) = (QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClassEquivNormClass_symm_uniformizerClass_zpow
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (n : ℤ) :
    (N.zeroQuotientModuloResidueDegreeClassEquivNormClass hϖH hzero).symm
        ((QuotientGroup.mk' N.normSubgroupClassInZeroQuotient
          (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n) =
      (QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n

def

zeroSubgroupQuotientToNormQuotient

L1304 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToNormQuotient

Documentation

The natural map G/G⁰ → G/N, where N is a norm subgroup containing the valuation-zero subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

def zeroSubgroupQuotientToNormQuotient [(N.normSubgroup).Normal]
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) :
    G ⧸ vG.zeroSubgroup →* G ⧸ N.normSubgroup

theorem

zeroSubgroupQuotientToNormQuotient_mk

L1315 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToNormQuotient_mk

Documentation

Establishes the identity N.zeroSubgroupQuotientToNormQuotient hzero (QuotientGroup.mk' vG.zeroSubgroup x) = QuotientGroup.mk' N.normSubgroup x.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToNormQuotient_mk
    [(N.normSubgroup).Normal]
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) :
    N.zeroSubgroupQuotientToNormQuotient hzero
        (QuotientGroup.mk' vG.zeroSubgroup x) =
      QuotientGroup.mk' N.normSubgroup x

theorem

zeroSubgroupQuotientToNormQuotient_surjective

L1328 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToNormQuotient_surjective

Documentation

The specified map is surjective: Function.Surjective (N.zeroSubgroupQuotientToNormQuotient hzero).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToNormQuotient_surjective
    [(N.normSubgroup).Normal]
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) :
    Function.Surjective (N.zeroSubgroupQuotientToNormQuotient hzero)

theorem

zeroSubgroupQuotientToNormQuotient_mk_eq_one_iff

L1341 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToNormQuotient_mk_eq_one_iff

Documentation

Characterizes N.zeroSubgroupQuotientToNormQuotient hzero (QuotientGroup.mk' vG.zeroSubgroup x) = 1 by the equivalent condition x ∈ N.normSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToNormQuotient_mk_eq_one_iff
    [(N.normSubgroup).Normal]
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) :
    N.zeroSubgroupQuotientToNormQuotient hzero
        (QuotientGroup.mk' vG.zeroSubgroup x) = 1 ↔
      x ∈ N.normSubgroup

theorem

zeroSubgroupQuotientToNormQuotient_ker_eq_normSubgroupClassInZeroQuotient

L1351 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToNormQuotient_ker_eq_normSubgroupClassInZeroQuotient

Documentation

The kernel of G/G⁰ → G/N is the image of N in G/G⁰.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToNormQuotient_ker_eq_normSubgroupClassInZeroQuotient
    [(N.normSubgroup).Normal]
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) :
    (N.zeroSubgroupQuotientToNormQuotient hzero).ker =
      N.normSubgroupClassInZeroQuotient

theorem

zeroSubgroupQuotientToValueModResidueDegree_ker_eq_normSubgroupClassInZeroQuotient

L1365 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToValueModResidueDegree_ker_eq_normSubgroupClassInZeroQuotient

Documentation

Establishes the identity N.zeroSubgroupQuotientToValueModResidueDegree.ker = N.normSubgroupClassInZeroQuotient.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToValueModResidueDegree_ker_eq_normSubgroupClassInZeroQuotient
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) :
    N.zeroSubgroupQuotientToValueModResidueDegree.ker =
      N.normSubgroupClassInZeroQuotient

theorem

mem_zeroSubgroupQuotientToNormQuotient_ker_iff

L1378 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.mem_zeroSubgroupQuotientToNormQuotient_ker_iff

Documentation

Characterizes q ∈ (N.zeroSubgroupQuotientToNormQuotient hzero).ker by the equivalent condition q ∈ N.normSubgroupClassInZeroQuotient.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem mem_zeroSubgroupQuotientToNormQuotient_ker_iff
    [(N.normSubgroup).Normal]
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup)
    (q : G ⧸ vG.zeroSubgroup) :
    q ∈ (N.zeroSubgroupQuotientToNormQuotient hzero).ker ↔
      q ∈ N.normSubgroupClassInZeroQuotient

theorem

quotientZeroSubgroup_mk_mem_normSubgroupClassInZeroQuotient_iff

L1391 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientZeroSubgroup_mk_mem_normSubgroupClassInZeroQuotient_iff

Documentation

Characterizes QuotientGroup.mk' vG.zeroSubgroup x ∈ N.normSubgroupClassInZeroQuotient by the equivalent condition x ∈ N.normSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem quotientZeroSubgroup_mk_mem_normSubgroupClassInZeroQuotient_iff
    [(N.normSubgroup).Normal]
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) :
    QuotientGroup.mk' vG.zeroSubgroup x ∈
        N.normSubgroupClassInZeroQuotient ↔
      x ∈ N.normSubgroup

theorem

zeroSubgroupQuotientToNormQuotient_eq_one_iff_mem_normSubgroupClassInZeroQuotient

L1407 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToNormQuotient_eq_one_iff_mem_normSubgroupClassInZeroQuotient

Documentation

Characterizes N.zeroSubgroupQuotientToNormQuotient hzero q = 1 by the equivalent condition q ∈ N.normSubgroupClassInZeroQuotient.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToNormQuotient_eq_one_iff_mem_normSubgroupClassInZeroQuotient
    [(N.normSubgroup).Normal]
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup)
    (q : G ⧸ vG.zeroSubgroup) :
    N.zeroSubgroupQuotientToNormQuotient hzero q = 1 ↔
      q ∈ N.normSubgroupClassInZeroQuotient

theorem

zeroSubgroupQuotientToNormQuotient_eq_one_iff_exists_normSubgroup_repr

L1420 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToNormQuotient_eq_one_iff_exists_normSubgroup_repr

Documentation

Characterizes N.zeroSubgroupQuotientToNormQuotient hzero q = 1 by the equivalent condition ∃ x : G, x ∈ N.normSubgroup ∧ QuotientGroup.mk' vG.zeroSubgroup x = q.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToNormQuotient_eq_one_iff_exists_normSubgroup_repr
    [(N.normSubgroup).Normal]
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup)
    (q : G ⧸ vG.zeroSubgroup) :
    N.zeroSubgroupQuotientToNormQuotient hzero q = 1 ↔
      ∃ x : G, x ∈ N.normSubgroup ∧
        QuotientGroup.mk' vG.zeroSubgroup x = q

theorem

zeroSubgroupQuotientToNormQuotient_eq_iff_div_mem_normSubgroupClassInZeroQuotient

L1435 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToNormQuotient_eq_iff_div_mem_normSubgroupClassInZeroQuotient

Documentation

Characterizes N.zeroSubgroupQuotientToNormQuotient hzero q = N.zeroSubgroupQuotientToNormQuotient hzero r by the equivalent condition q / r ∈ N.normSubgroupClassInZeroQuotient.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToNormQuotient_eq_iff_div_mem_normSubgroupClassInZeroQuotient
    [(N.normSubgroup).Normal]
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup)
    (q r : G ⧸ vG.zeroSubgroup) :
    N.zeroSubgroupQuotientToNormQuotient hzero q =
        N.zeroSubgroupQuotientToNormQuotient hzero r ↔
      q / r ∈ N.normSubgroupClassInZeroQuotient

def

zeroQuotientModuloNormClassEquivNormQuotient

L1450 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloNormClassEquivNormQuotient

Documentation

The third-isomorphism equivalence (G/G⁰)/(N/G⁰) ≃ G/N for the norm subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

def zeroQuotientModuloNormClassEquivNormQuotient
    [(N.normSubgroup).Normal]
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) :
    (G ⧸ vG.zeroSubgroup) ⧸ N.normSubgroupClassInZeroQuotient ≃*
      G ⧸ N.normSubgroup

theorem

zeroQuotientModuloNormClassEquivNormQuotient_mk

L1462 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloNormClassEquivNormQuotient_mk

Documentation

Establishes the identity N.zeroQuotientModuloNormClassEquivNormQuotient hzero (QuotientGroup.mk' N.normSubgroupClassInZeroQuotient q) = N.zeroSubgroupQuotientToNormQuotient hzero q.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloNormClassEquivNormQuotient_mk
    [(N.normSubgroup).Normal]
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup)
    (q : G ⧸ vG.zeroSubgroup) :
    N.zeroQuotientModuloNormClassEquivNormQuotient hzero
        (QuotientGroup.mk' N.normSubgroupClassInZeroQuotient q) =
      N.zeroSubgroupQuotientToNormQuotient hzero q

theorem

zeroQuotientModuloNormClassEquivNormQuotient_mk_mk

L1482 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloNormClassEquivNormQuotient_mk_mk

Documentation

Establishes the identity N.zeroQuotientModuloNormClassEquivNormQuotient hzero (QuotientGroup.mk' N.normSubgroupClassInZeroQuotient (QuotientGroup.mk' vG.zeroSubgroup x)) = QuotientGroup.mk' N.normSubgroup x.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloNormClassEquivNormQuotient_mk_mk
    [(N.normSubgroup).Normal]
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) :
    N.zeroQuotientModuloNormClassEquivNormQuotient hzero
        (QuotientGroup.mk' N.normSubgroupClassInZeroQuotient
          (QuotientGroup.mk' vG.zeroSubgroup x)) =
      QuotientGroup.mk' N.normSubgroup x

def

zeroQuotientModuloResidueDegreeClassEquivNormQuotient

L1494 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivNormQuotient

Documentation

Direct form of the quotient comparison from the residue-degree class subgroup to the norm quotient.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

def zeroQuotientModuloResidueDegreeClassEquivNormQuotient
    [(N.normSubgroup).Normal]
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) :
    (G ⧸ vG.zeroSubgroup) ⧸ N.residueDegreeClassSubgroup ≃*
      G ⧸ N.normSubgroup

theorem

zeroQuotientModuloResidueDegreeClassEquivNormQuotient_mk

L1508 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivNormQuotient_mk

Documentation

Establishes the identity N.zeroQuotientModuloResidueDegreeClassEquivNormQuotient hϖH hzero (QuotientGroup.mk' N.residueDegreeClassSubgroup q) = N.zeroSubgroupQuotientToNormQuotient hzero q.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClassEquivNormQuotient_mk
    [(N.normSubgroup).Normal]
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup)
    (q : G ⧸ vG.zeroSubgroup) :
    N.zeroQuotientModuloResidueDegreeClassEquivNormQuotient hϖH hzero
        (QuotientGroup.mk' N.residueDegreeClassSubgroup q) =
      N.zeroSubgroupQuotientToNormQuotient hzero q

theorem

zeroQuotientModuloResidueDegreeClassEquivNormQuotient_mk_mk

L1531 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivNormQuotient_mk_mk

Documentation

Establishes the identity N.zeroQuotientModuloResidueDegreeClassEquivNormQuotient hϖH hzero (QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup x)) = QuotientGroup.mk' N.normSubgroup x.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClassEquivNormQuotient_mk_mk
    [(N.normSubgroup).Normal]
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) :
    N.zeroQuotientModuloResidueDegreeClassEquivNormQuotient hϖH hzero
        (QuotientGroup.mk' N.residueDegreeClassSubgroup
          (QuotientGroup.mk' vG.zeroSubgroup x)) =
      QuotientGroup.mk' N.normSubgroup x

theorem

zeroQuotientModuloResidueDegreeClassEquivNormQuotient_symm_mk

L1547 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivNormQuotient_symm_mk

Documentation

Establishes the identity (N.zeroQuotientModuloResidueDegreeClassEquivNormQuotient hϖH hzero).symm (QuotientGroup.mk' N.normSubgroup x) = QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup x).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClassEquivNormQuotient_symm_mk
    [(N.normSubgroup).Normal]
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) :
    (N.zeroQuotientModuloResidueDegreeClassEquivNormQuotient hϖH hzero).symm
        (QuotientGroup.mk' N.normSubgroup x) =
      QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup x)

theorem

zeroQuotientModuloResidueDegreeClassEquivNormQuotient_uniformizerClass_zpow

L1576 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivNormQuotient_uniformizerClass_zpow

Documentation

zeroQuotientModuloResidueDegreeClassEquivNormQuotient_uniformizerClass satisfies the integer-power formula N.zeroQuotientModuloResidueDegreeClassEquivNormQuotient hϖH hzero ((QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n) = (QuotientGroup.mk' N.normSubgroup ϖG) ^ n.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClassEquivNormQuotient_uniformizerClass_zpow
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (n : ℤ) :
    N.zeroQuotientModuloResidueDegreeClassEquivNormQuotient hϖH hzero
        ((QuotientGroup.mk' N.residueDegreeClassSubgroup
          (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n) =
      (QuotientGroup.mk' N.normSubgroup ϖG) ^ n

theorem

zeroQuotientModuloResidueDegreeClassEquivNormQuotient_symm_uniformizerClass_zpow

L1599 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivNormQuotient_symm_uniformizerClass_zpow

Documentation

zeroQuotientModuloResidueDegreeClassEquivNormQuotient_symm_uniformizerClass satisfies the integer-power formula (N.zeroQuotientModuloResidueDegreeClassEquivNormQuotient hϖH hzero).symm ((QuotientGroup.mk' N.normSubgroup ϖG) ^ n) = (QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClassEquivNormQuotient_symm_uniformizerClass_zpow
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (n : ℤ) :
    (N.zeroQuotientModuloResidueDegreeClassEquivNormQuotient hϖH hzero).symm
        ((QuotientGroup.mk' N.normSubgroup ϖG) ^ n) =
      (QuotientGroup.mk' N.residueDegreeClassSubgroup
        (QuotientGroup.mk' vG.zeroSubgroup ϖG)) ^ n

theorem

zeroSubgroupQuotientToValueModResidueDegree_ker_eq_zeroSubgroupQuotientToNormQuotient_ker

L1620 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToValueModResidueDegree_ker_eq_zeroSubgroupQuotientToNormQuotient_ker

Documentation

Establishes the identity N.zeroSubgroupQuotientToValueModResidueDegree.ker = (N.zeroSubgroupQuotientToNormQuotient hzero).ker.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToValueModResidueDegree_ker_eq_zeroSubgroupQuotientToNormQuotient_ker
    [(N.normSubgroup).Normal]
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) :
    N.zeroSubgroupQuotientToValueModResidueDegree.ker =
      (N.zeroSubgroupQuotientToNormQuotient hzero).ker

theorem

zeroSubgroupQuotientToValueModResidueDegree_eq_one_iff_zeroSubgroupQuotientToNormQuotient_eq_one

L1635 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToValueModResidueDegree_eq_one_iff_zeroSubgroupQuotientToNormQuotient_eq_one

Documentation

Characterizes N.zeroSubgroupQuotientToValueModResidueDegree q = 1 by the equivalent condition N.zeroSubgroupQuotientToNormQuotient hzero q = 1.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem
zeroSubgroupQuotientToValueModResidueDegree_eq_one_iff_zeroSubgroupQuotientToNormQuotient_eq_one
    [(N.normSubgroup).Normal]
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup)
    (q : G ⧸ vG.zeroSubgroup) :
    N.zeroSubgroupQuotientToValueModResidueDegree q = 1 ↔
      N.zeroSubgroupQuotientToNormQuotient hzero q = 1

theorem

zeroSubgroupQuotientToValueModResidueDegree_eq_iff_zeroSubgroupQuotientToNormQuotient_eq

L1655 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToValueModResidueDegree_eq_iff_zeroSubgroupQuotientToNormQuotient_eq

Documentation

Characterizes N.zeroSubgroupQuotientToValueModResidueDegree q = N.zeroSubgroupQuotientToValueModResidueDegree r by the equivalent condition N.zeroSubgroupQuotientToNormQuotient hzero q = N.zeroSubgroupQuotientToNormQuotient hzero r.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToValueModResidueDegree_eq_iff_zeroSubgroupQuotientToNormQuotient_eq
    [(N.normSubgroup).Normal]
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup)
    (q r : G ⧸ vG.zeroSubgroup) :
    N.zeroSubgroupQuotientToValueModResidueDegree q =
        N.zeroSubgroupQuotientToValueModResidueDegree r ↔
      N.zeroSubgroupQuotientToNormQuotient hzero q =
        N.zeroSubgroupQuotientToNormQuotient hzero r

theorem

zeroSubgroupQuotientToNormQuotient_mk_eq_iff

L1676 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToNormQuotient_mk_eq_iff

Documentation

Characterizes N.zeroSubgroupQuotientToNormQuotient hzero (QuotientGroup.mk' vG.zeroSubgroup x) = N.zeroSubgroupQuotientToNormQuotient hzero (QuotientGroup.mk' vG.zeroSubgroup y) by the equivalent condition x / y ∈ N.normSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToNormQuotient_mk_eq_iff
    [(N.normSubgroup).Normal]
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x y : G) :
    N.zeroSubgroupQuotientToNormQuotient hzero
        (QuotientGroup.mk' vG.zeroSubgroup x) =
    N.zeroSubgroupQuotientToNormQuotient hzero
        (QuotientGroup.mk' vG.zeroSubgroup y) ↔
      x / y ∈ N.normSubgroup

theorem

zeroSubgroupQuotientToNormQuotient_mk_eq_iff_inv_mul_mem

L1692 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToNormQuotient_mk_eq_iff_inv_mul_mem

Documentation

Left-quotient version of zeroSubgroupQuotientToNormQuotient_mk_eq_iff.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToNormQuotient_mk_eq_iff_inv_mul_mem
    [(N.normSubgroup).Normal]
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x y : G) :
    N.zeroSubgroupQuotientToNormQuotient hzero
        (QuotientGroup.mk' vG.zeroSubgroup x) =
      N.zeroSubgroupQuotientToNormQuotient hzero
        (QuotientGroup.mk' vG.zeroSubgroup y) ↔
      y⁻¹ * x ∈ N.normSubgroup

theorem

zeroSubgroupQuotientToNormQuotient_mk_eq_one_iff_residueDegree_dvd

L1707 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToNormQuotient_mk_eq_one_iff_residueDegree_dvd

Documentation

Characterizes N.zeroSubgroupQuotientToNormQuotient hzero (QuotientGroup.mk' vG.zeroSubgroup x) = 1 by the equivalent condition (N.residueDegree : ℤ) ∣ vG.val x.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToNormQuotient_mk_eq_one_iff_residueDegree_dvd
    [(N.normSubgroup).Normal]
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) :
    N.zeroSubgroupQuotientToNormQuotient hzero
        (QuotientGroup.mk' vG.zeroSubgroup x) = 1 ↔
      (N.residueDegree : ℤ) ∣ vG.val x

theorem

zeroSubgroupQuotientToNormQuotient_mk_eq_iff_residueDegree_dvd

L1723 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToNormQuotient_mk_eq_iff_residueDegree_dvd

Documentation

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToNormQuotient_mk_eq_iff_residueDegree_dvd
    [(N.normSubgroup).Normal]
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x y : G) :
    N.zeroSubgroupQuotientToNormQuotient hzero
        (QuotientGroup.mk' vG.zeroSubgroup x) =
      N.zeroSubgroupQuotientToNormQuotient hzero
        (QuotientGroup.mk' vG.zeroSubgroup y) ↔
      (N.residueDegree : ℤ) ∣ vG.val x - vG.val y

theorem

zeroSubgroupQuotientToNormQuotient_mk_eq_iff_inv_mul_residueDegree_dvd

L1739 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToNormQuotient_mk_eq_iff_inv_mul_residueDegree_dvd

Documentation

Left-quotient proof route for equality in G ⧸ zeroSubgroup → G ⧸ normSubgroup, expressed by residue-degree divisibility.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToNormQuotient_mk_eq_iff_inv_mul_residueDegree_dvd
    [(N.normSubgroup).Normal]
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x y : G) :
    N.zeroSubgroupQuotientToNormQuotient hzero
        (QuotientGroup.mk' vG.zeroSubgroup x) =
      N.zeroSubgroupQuotientToNormQuotient hzero
        (QuotientGroup.mk' vG.zeroSubgroup y) ↔
      (N.residueDegree : ℤ) ∣ vG.val x - vG.val y

def

normQuotientEquivValueModResidueDegree

L1755 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotientEquivValueModResidueDegree

Documentation

The actual norm quotient is the value-group quotient ℤ / fℤ when valuation-zero target elements are norms and the target valuation has a uniformizer.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

def normQuotientEquivValueModResidueDegree
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) :
    G ⧸ N.normSubgroup ≃*
      Multiplicative ℤ ⧸ integerMultipleSubgroup (N.residueDegree : ℤ)

theorem

normQuotientEquivValueModResidueDegree_mk

L1774 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotientEquivValueModResidueDegree_mk

Documentation

Establishes the identity N.normQuotientEquivValueModResidueDegree hϖG hϖH hzero (QuotientGroup.mk' N.normSubgroup x) = QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ)) (vG.valuationHom x).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotientEquivValueModResidueDegree_mk
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) :
    N.normQuotientEquivValueModResidueDegree hϖG hϖH hzero
        (QuotientGroup.mk' N.normSubgroup x) =
      QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ))
        (vG.valuationHom x)

theorem

normQuotientEquivValueModResidueDegree_mk_ofAdd

L1795 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotientEquivValueModResidueDegree_mk_ofAdd

Documentation

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotientEquivValueModResidueDegree_mk_ofAdd
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) :
    N.normQuotientEquivValueModResidueDegree hϖG hϖH hzero
        (QuotientGroup.mk' N.normSubgroup x) =
      QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ))
        (Multiplicative.ofAdd (vG.val x))

theorem

normQuotientEquivValueModResidueDegree_uniformizer_zpow

L1812 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotientEquivValueModResidueDegree_uniformizer_zpow

Documentation

normQuotientEquivValueModResidueDegree_uniformizer satisfies the integer-power formula N.normQuotientEquivValueModResidueDegree hϖG hϖH hzero (QuotientGroup.mk' N.normSubgroup (ϖG ^ n)) = QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ)) (Multiplicative.ofAdd n).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotientEquivValueModResidueDegree_uniformizer_zpow
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (n : ℤ) :
    N.normQuotientEquivValueModResidueDegree hϖG hϖH hzero
        (QuotientGroup.mk' N.normSubgroup (ϖG ^ n)) =
      QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ))
        (Multiplicative.ofAdd n)

theorem

normQuotientEquivValueModResidueDegree_symm_mk_val

L1830 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotientEquivValueModResidueDegree_symm_mk_val

Documentation

Establishes the identity (N.normQuotientEquivValueModResidueDegree hϖG hϖH hzero).symm (QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ)) (Multiplicative.ofAdd (vG.val x))) = QuotientGroup.mk' N.normSubgroup x.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotientEquivValueModResidueDegree_symm_mk_val
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) :
    (N.normQuotientEquivValueModResidueDegree hϖG hϖH hzero).symm
        (QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ))
          (Multiplicative.ofAdd (vG.val x))) =
      QuotientGroup.mk' N.normSubgroup x

theorem

normQuotientEquivValueModResidueDegree_symm_mk_ofAdd

L1860 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotientEquivValueModResidueDegree_symm_mk_ofAdd

Documentation

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotientEquivValueModResidueDegree_symm_mk_ofAdd
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (n : ℤ) :
    (N.normQuotientEquivValueModResidueDegree hϖG hϖH hzero).symm
        (QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ))
          (Multiplicative.ofAdd n)) =
      QuotientGroup.mk' N.normSubgroup (ϖG ^ n)

theorem

normQuotientEquivValueModResidueDegree_zeroSubgroupQuotientToNormQuotient_mk

L1876 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotientEquivValueModResidueDegree_zeroSubgroupQuotientToNormQuotient_mk

Documentation

Compatibility of the natural map G/G⁰ → G/N with the value-modulo residue-degree map.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotientEquivValueModResidueDegree_zeroSubgroupQuotientToNormQuotient_mk
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) :
    N.normQuotientEquivValueModResidueDegree hϖG hϖH hzero
        (N.zeroSubgroupQuotientToNormQuotient hzero
          (QuotientGroup.mk' vG.zeroSubgroup x)) =
      N.zeroSubgroupQuotientToValueModResidueDegree
        (QuotientGroup.mk' vG.zeroSubgroup x)

theorem

normQuotientEquivValueModResidueDegree_zeroQuotientModuloResidueDegreeClassEquivNormQuotient_mk

L1894 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotientEquivValueModResidueDegree_zeroQuotientModuloResidueDegreeClassEquivNormQuotient_mk

Documentation

The direct residue-degree-class quotient to the norm quotient, followed by the norm-quotient/value-group equivalence, agrees with the direct value-mod-residue-degree quotient map on representatives.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem
normQuotientEquivValueModResidueDegree_zeroQuotientModuloResidueDegreeClassEquivNormQuotient_mk
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup)
    (q : G ⧸ vG.zeroSubgroup) :
    N.normQuotientEquivValueModResidueDegree hϖG hϖH hzero
        (N.zeroQuotientModuloResidueDegreeClassEquivNormQuotient hϖH hzero
          (QuotientGroup.mk' N.residueDegreeClassSubgroup q)) =
      N.zeroSubgroupQuotientToValueModResidueDegree q

theorem

normQuotientEquivValueModResidueDegree_zeroQuotientModuloResidueDegreeClassEquivNormQuotient_mk_mk

L1927 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotientEquivValueModResidueDegree_zeroQuotientModuloResidueDegreeClassEquivNormQuotient_mk_mk

Documentation

Establishes the identity N.normQuotientEquivValueModResidueDegree hϖG hϖH hzero (N.zeroQuotientModuloResidueDegreeClassEquivNormQuotient hϖH hzero (QuotientGroup.mk' N.residueDegreeClassSubgroup (QuotientGroup.mk' vG.zeroSubgroup x))) = QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ)) (Multiplicative.ofAdd (vG.val x)).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem
normQuotientEquivValueModResidueDegree_zeroQuotientModuloResidueDegreeClassEquivNormQuotient_mk_mk
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) :
    N.normQuotientEquivValueModResidueDegree hϖG hϖH hzero
        (N.zeroQuotientModuloResidueDegreeClassEquivNormQuotient hϖH hzero
          (QuotientGroup.mk' N.residueDegreeClassSubgroup
            (QuotientGroup.mk' vG.zeroSubgroup x))) =
      QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ))
        (Multiplicative.ofAdd (vG.val x))

theorem

zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_apply_eq_norm_composite

L1946 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_apply_eq_norm_composite

Documentation

Pointwise compatibility of the two quotient routes from (G/G⁰)/residueDegreeClassSubgroup to the value group modulo the residue-degree subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree_apply_eq_norm_composite
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup)
    (z : (G ⧸ vG.zeroSubgroup) ⧸ N.residueDegreeClassSubgroup) :
    N.zeroQuotientModuloResidueDegreeClassEquivValueModResidueDegree hϖG z =
      N.normQuotientEquivValueModResidueDegree hϖG hϖH hzero
        (N.zeroQuotientModuloResidueDegreeClassEquivNormQuotient hϖH hzero z)

theorem

normQuotient_mk_eq_one_iff_mem

L1997 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_mk_eq_one_iff_mem

Documentation

Kernel criterion for the actual quotient by the norm subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_mk_eq_one_iff_mem [(N.normSubgroup).Normal] (x : G) :
    QuotientGroup.mk' N.normSubgroup x = 1 ↔ x ∈ N.normSubgroup

theorem

normQuotient_mk_eq_iff_div_mem

L2003 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_mk_eq_iff_div_mem

Documentation

Equality in the actual quotient by the norm subgroup is equality modulo the norm subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_mk_eq_iff_div_mem [(N.normSubgroup).Normal] (x y : G) :
    QuotientGroup.mk' N.normSubgroup x =
        QuotientGroup.mk' N.normSubgroup y ↔
      x / y ∈ N.normSubgroup

theorem

normQuotient_mk_eq_iff_inv_mul_mem

L2013 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_mk_eq_iff_inv_mul_mem

Documentation

Equality in the actual quotient by the norm subgroup, in left-quotient form.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_mk_eq_iff_inv_mul_mem [(N.normSubgroup).Normal]
    (x y : G) :
    QuotientGroup.mk' N.normSubgroup x =
        QuotientGroup.mk' N.normSubgroup y ↔
      y⁻¹ * x ∈ N.normSubgroup

theorem

normQuotient_mk_eq_iff_residueDegree_dvd_valuation_difference

L2023 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_mk_eq_iff_residueDegree_dvd_valuation_difference

Documentation

Equality in the norm quotient, expressed by valuation divisibility under the standard hypothesis that valuation-zero target elements are norms.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_mk_eq_iff_residueDegree_dvd_valuation_difference
    [(N.normSubgroup).Normal]
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x y : G) :
    QuotientGroup.mk' N.normSubgroup x =
        QuotientGroup.mk' N.normSubgroup y ↔
      (N.residueDegree : ℤ) ∣ vG.val x - vG.val y

theorem

normQuotient_mk_eq_iff_inv_mul_residueDegree_dvd

L2036 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_mk_eq_iff_inv_mul_residueDegree_dvd

Documentation

Left-quotient proof route for equality in the norm quotient, expressed by residue-degree divisibility.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_mk_eq_iff_inv_mul_residueDegree_dvd
    [(N.normSubgroup).Normal]
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x y : G) :
    QuotientGroup.mk' N.normSubgroup x =
        QuotientGroup.mk' N.normSubgroup y ↔
      (N.residueDegree : ℤ) ∣ vG.val x - vG.val y

theorem

inv_mul_mem_normSubgroup_of_normQuotient_mk_eq

L2048 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.inv_mul_mem_normSubgroup_of_normQuotient_mk_eq

Documentation

Establishes the membership statement y⁻¹ * x ∈ N.normSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem inv_mul_mem_normSubgroup_of_normQuotient_mk_eq
    [(N.normSubgroup).Normal] {x y : G}
    (hxy : QuotientGroup.mk' N.normSubgroup x =
        QuotientGroup.mk' N.normSubgroup y) :
    y⁻¹ * x ∈ N.normSubgroup

theorem

normQuotient_mk_eq_of_inv_mul_mem

L2059 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_mk_eq_of_inv_mul_mem

Documentation

Establishes the identity QuotientGroup.mk' N.normSubgroup x = QuotientGroup.mk' N.normSubgroup y.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_mk_eq_of_inv_mul_mem
    [(N.normSubgroup).Normal] {x y : G}
    (hxy : y⁻¹ * x ∈ N.normSubgroup) :
    QuotientGroup.mk' N.normSubgroup x =
      QuotientGroup.mk' N.normSubgroup y

theorem

normQuotient_mk_eq_of_val_eq

L2068 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_mk_eq_of_val_eq

Documentation

Elements with the same valuation represent the same norm-quotient class when valuation-zero target elements are norms.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_mk_eq_of_val_eq [(N.normSubgroup).Normal]
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup)
    {x y : G} (hxy : vG.val x = vG.val y) :
    QuotientGroup.mk' N.normSubgroup x =
      QuotientGroup.mk' N.normSubgroup y

theorem

normQuotient_mk_eq_uniformizer_zpow_val

L2078 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_mk_eq_uniformizer_zpow_val

Documentation

Every norm-quotient class has a target-uniformizer-power representative when valuation-zero target elements are norms.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_mk_eq_uniformizer_zpow_val
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) :
    QuotientGroup.mk' N.normSubgroup x =
      QuotientGroup.mk' N.normSubgroup (ϖG ^ vG.val x)

theorem

normQuotient_mk_eq_uniformizer_zpow_iff

L2089 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_mk_eq_uniformizer_zpow_iff

Documentation

Criterion for a norm-quotient class to be represented by a prescribed target-uniformizer power.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_mk_eq_uniformizer_zpow_iff
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) (n : ℤ) :
    QuotientGroup.mk' N.normSubgroup x =
        QuotientGroup.mk' N.normSubgroup (ϖG ^ n) ↔
      (N.residueDegree : ℤ) ∣ vG.val x - n

theorem

normQuotient_uniformizer_zpow_mk_eq_iff

L2103 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_uniformizer_zpow_mk_eq_iff

Documentation

Equality of two target-uniformizer-power classes in the norm quotient is equivalent to residue-degree divisibility of the exponent difference.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_uniformizer_zpow_mk_eq_iff
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (m n : ℤ) :
    QuotientGroup.mk' N.normSubgroup (ϖG ^ m) =
        QuotientGroup.mk' N.normSubgroup (ϖG ^ n) ↔
      (N.residueDegree : ℤ) ∣ m - n

theorem

normQuotient_uniformizer_zpow_residueDegree_eq_one

L2117 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_uniformizer_zpow_residueDegree_eq_one

Documentation

The residue-degree power of a target uniformizer is trivial in the norm quotient under the standard unit-norm-surjectivity hypothesis.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_uniformizer_zpow_residueDegree_eq_one
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) :
    QuotientGroup.mk' N.normSubgroup
        (ϖG ^ (N.residueDegree : ℤ)) = 1

theorem

normQuotient_uniformizer_zpow_add_residueDegree_mul_mk_eq

L2132 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_uniformizer_zpow_add_residueDegree_mul_mk_eq

Documentation

Uniformizer powers in the norm quotient are periodic modulo the residue degree under the standard unit-norm-surjectivity hypothesis.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_uniformizer_zpow_add_residueDegree_mul_mk_eq
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (n k : ℤ) :
    QuotientGroup.mk' N.normSubgroup
        (ϖG ^ (n + (N.residueDegree : ℤ) * k)) =
      QuotientGroup.mk' N.normSubgroup (ϖG ^ n)

theorem

normQuotient_mk_eq_uniformizerClass_zpow_val

L2147 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_mk_eq_uniformizerClass_zpow_val

Documentation

Generator-power form of normQuotient_mk_eq_uniformizer_zpow_val: every element has the same norm quotient class as the valuation power of a target uniformizer class.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_mk_eq_uniformizerClass_zpow_val
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) :
    QuotientGroup.mk' N.normSubgroup x =
      (QuotientGroup.mk' N.normSubgroup ϖG) ^ vG.val x

theorem

normQuotient_mk_eq_uniformizerClass_zpow_iff

L2158 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_mk_eq_uniformizerClass_zpow_iff

Documentation

Criterion for a norm-quotient class to be a prescribed power of the target uniformizer class.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_mk_eq_uniformizerClass_zpow_iff
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) (n : ℤ) :
    QuotientGroup.mk' N.normSubgroup x =
        (QuotientGroup.mk' N.normSubgroup ϖG) ^ n ↔
      (N.residueDegree : ℤ) ∣ vG.val x - n

theorem

normQuotient_uniformizerClass_zpow_eq_iff

L2172 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_uniformizerClass_zpow_eq_iff

Documentation

Equality of two powers of the target uniformizer class is residue-degree divisibility of the exponent difference.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_uniformizerClass_zpow_eq_iff
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (m n : ℤ) :
    (QuotientGroup.mk' N.normSubgroup ϖG) ^ m =
        (QuotientGroup.mk' N.normSubgroup ϖG) ^ n ↔
      (N.residueDegree : ℤ) ∣ m - n

theorem

normQuotient_uniformizerClass_zpow_eq_of_sub_dvd

L2187 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_uniformizerClass_zpow_eq_of_sub_dvd

Documentation

A sufficient form of the exponent-reduction criterion for the target uniformizer class.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_uniformizerClass_zpow_eq_of_sub_dvd
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) {m n : ℤ}
    (hmn : (N.residueDegree : ℤ) ∣ m - n) :
    (QuotientGroup.mk' N.normSubgroup ϖG) ^ m =
      (QuotientGroup.mk' N.normSubgroup ϖG) ^ n

theorem

normQuotient_uniformizerClass_zpow_add_residueDegree_mul_eq

L2200 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_uniformizerClass_zpow_add_residueDegree_mul_eq

Documentation

The target-uniformizer generator in the norm quotient has exponents periodic modulo the residue degree.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_uniformizerClass_zpow_add_residueDegree_mul_eq
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (n k : ℤ) :
    (QuotientGroup.mk' N.normSubgroup ϖG) ^
        (n + (N.residueDegree : ℤ) * k) =
      (QuotientGroup.mk' N.normSubgroup ϖG) ^ n

theorem

normQuotient_uniformizerClass_zpow_residueDegree_eq_one

L2213 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_uniformizerClass_zpow_residueDegree_eq_one

Documentation

The residue-degree power of the target uniformizer class is trivial in the norm quotient.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_uniformizerClass_zpow_residueDegree_eq_one
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) :
    (QuotientGroup.mk' N.normSubgroup ϖG) ^ (N.residueDegree : ℤ) = 1

theorem

normQuotient_uniformizerClass_zpow_eq_one_iff

L2226 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_uniformizerClass_zpow_eq_one_iff

Documentation

A power of the target uniformizer class is trivial exactly when its exponent is divisible by the residue degree.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_uniformizerClass_zpow_eq_one_iff
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (n : ℤ) :
    (QuotientGroup.mk' N.normSubgroup ϖG) ^ n = 1 ↔
      (N.residueDegree : ℤ) ∣ n

theorem

normQuotient_generated_by_uniformizerClass

L2239 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_generated_by_uniformizerClass

Documentation

The norm quotient is generated by the class of any target uniformizer.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_generated_by_uniformizerClass
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup)
    (q : G ⧸ N.normSubgroup) :
    ∃ n : ℤ, q = (QuotientGroup.mk' N.normSubgroup ϖG) ^ n

theorem

normQuotient_closure_uniformizerClass_eq_top

L2253 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_closure_uniformizerClass_eq_top

Documentation

The norm quotient is cyclic, generated by the class of any target uniformizer, under the standard unit-norm-surjectivity hypothesis.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_closure_uniformizerClass_eq_top
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) :
    Subgroup.closure
        ({QuotientGroup.mk' N.normSubgroup ϖG} : Set (G ⧸ N.normSubgroup)) =
      ⊤

theorem

normQuotientEquivValueModResidueDegree_uniformizerClass_zpow

L2273 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotientEquivValueModResidueDegree_uniformizerClass_zpow

Documentation

Under the value-group equivalence, the nth power of the target uniformizer class maps to the class of n modulo the residue-degree subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotientEquivValueModResidueDegree_uniformizerClass_zpow
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (n : ℤ) :
    N.normQuotientEquivValueModResidueDegree hϖG hϖH hzero
        ((QuotientGroup.mk' N.normSubgroup ϖG) ^ n) =
      QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ))
        (Multiplicative.ofAdd n)

theorem

normQuotientEquivValueModResidueDegree_symm_mk_ofAdd_uniformizerClass_zpow

L2292 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotientEquivValueModResidueDegree_symm_mk_ofAdd_uniformizerClass_zpow

Documentation

normQuotientEquivValueModResidueDegree_symm_mk_ofAdd_uniformizerClass satisfies the integer-power formula (N.normQuotientEquivValueModResidueDegree hϖG hϖH hzero).symm (QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ)) (Multiplicative.ofAdd n)) = (QuotientGroup.mk' N.normSubgroup ϖG) ^ n.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotientEquivValueModResidueDegree_symm_mk_ofAdd_uniformizerClass_zpow
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (n : ℤ) :
    (N.normQuotientEquivValueModResidueDegree hϖG hϖH hzero).symm
        (QuotientGroup.mk' (integerMultipleSubgroup (N.residueDegree : ℤ))
          (Multiplicative.ofAdd n)) =
      (QuotientGroup.mk' N.normSubgroup ϖG) ^ n

def

normQuotientEquivZMod

L2308 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotientEquivZMod

Documentation

The actual norm quotient as the standard cyclic group Multiplicative (ZMod f), where f is the residue degree in the valuation formula.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

def normQuotientEquivZMod
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) :
    G ⧸ N.normSubgroup ≃* Multiplicative (ZMod N.residueDegree)

theorem

normQuotientEquivZMod_mk

L2321 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotientEquivZMod_mk

Documentation

Establishes the identity N.normQuotientEquivZMod hϖG hϖH hzero (QuotientGroup.mk' N.normSubgroup x) = Multiplicative.ofAdd ((vG.val x : ℤ) : ZMod N.residueDegree).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotientEquivZMod_mk
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) :
    N.normQuotientEquivZMod hϖG hϖH hzero
        (QuotientGroup.mk' N.normSubgroup x) =
      Multiplicative.ofAdd ((vG.val x : ℤ) : ZMod N.residueDegree)

theorem

normQuotientEquivZMod_uniformizer_zpow

L2338 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotientEquivZMod_uniformizer_zpow

Documentation

normQuotientEquivZMod_uniformizer satisfies the integer-power formula N.normQuotientEquivZMod hϖG hϖH hzero (QuotientGroup.mk' N.normSubgroup (ϖG ^ n)) = Multiplicative.ofAdd ((n : ℤ) : ZMod N.residueDegree).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotientEquivZMod_uniformizer_zpow
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (n : ℤ) :
    N.normQuotientEquivZMod hϖG hϖH hzero
        (QuotientGroup.mk' N.normSubgroup (ϖG ^ n)) =
      Multiplicative.ofAdd ((n : ℤ) : ZMod N.residueDegree)

theorem

normQuotientEquivZMod_uniformizerClass_zpow

L2354 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotientEquivZMod_uniformizerClass_zpow

Documentation

normQuotientEquivZMod_uniformizerClass satisfies the integer-power formula N.normQuotientEquivZMod hϖG hϖH hzero ((QuotientGroup.mk' N.normSubgroup ϖG) ^ n) = Multiplicative.ofAdd ((n : ℤ) : ZMod N.residueDegree).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotientEquivZMod_uniformizerClass_zpow
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (n : ℤ) :
    N.normQuotientEquivZMod hϖG hϖH hzero
        ((QuotientGroup.mk' N.normSubgroup ϖG) ^ n) =
      Multiplicative.ofAdd ((n : ℤ) : ZMod N.residueDegree)

theorem

normQuotientEquivZMod_symm_mk_ofAdd

L2369 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotientEquivZMod_symm_mk_ofAdd

Documentation

Establishes the identity (N.normQuotientEquivZMod hϖG hϖH hzero).symm (Multiplicative.ofAdd ((n : ℤ) : ZMod N.residueDegree)) = QuotientGroup.mk' N.normSubgroup (ϖG ^ n).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotientEquivZMod_symm_mk_ofAdd
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (n : ℤ) :
    (N.normQuotientEquivZMod hϖG hϖH hzero).symm
        (Multiplicative.ofAdd ((n : ℤ) : ZMod N.residueDegree)) =
      QuotientGroup.mk' N.normSubgroup (ϖG ^ n)

theorem

card_normQuotient_eq_residueDegree

L2383 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.card_normQuotient_eq_residueDegree

Documentation

Cardinality form of the norm-quotient computation when the residue degree is nonzero.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem card_normQuotient_eq_residueDegree
    [(N.normSubgroup).Normal]
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup)
    [NeZero N.residueDegree]
    [Finite (G ⧸ N.normSubgroup)] :
    Nat.card (G ⧸ N.normSubgroup) = N.residueDegree

theorem

uniformizer_zpow_mem_normSubgroup_iff_of_zeroSubgroup_le

L2402 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.uniformizer_zpow_mem_normSubgroup_iff_of_zeroSubgroup_le

Documentation

Uniformizer-power criterion for target powers lying in the norm subgroup, assuming all target valuation-zero elements are norms.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem uniformizer_zpow_mem_normSubgroup_iff_of_zeroSubgroup_le
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (n : ℤ) :
    ϖG ^ n ∈ N.normSubgroup ↔ (N.residueDegree : ℤ) ∣ n

theorem

uniformizer_zpow_div_mem_normSubgroup_iff_of_zeroSubgroup_le

L2414 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.uniformizer_zpow_div_mem_normSubgroup_iff_of_zeroSubgroup_le

Documentation

Target uniformizer-power quotients are norms exactly when the exponent difference is divisible by the residue degree, provided all target valuation-zero elements are norms.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem uniformizer_zpow_div_mem_normSubgroup_iff_of_zeroSubgroup_le
    {ϖG : G} (hϖG : vG.IsUniformizer ϖG)
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (m n : ℤ) :
    ϖG ^ m / ϖG ^ n ∈ N.normSubgroup ↔
      (N.residueDegree : ℤ) ∣ m - n

theorem

mem_normSubgroup_iff_exists_zeroSubgroup_mul_norm_uniformizer_zpow_eq

L2426 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.mem_normSubgroup_iff_exists_zeroSubgroup_mul_norm_uniformizer_zpow_eq

Documentation

Normal-form criterion for the norm subgroup when target valuation-zero elements are norms.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem mem_normSubgroup_iff_exists_zeroSubgroup_mul_norm_uniformizer_zpow_eq
    {ϖH : H} (hϖH : vH.IsUniformizer ϖH)
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x : G) :
    x ∈ N.normSubgroup ↔
      ∃ u : G, u ∈ vG.zeroSubgroup ∧
        ∃ n : ℤ, x = u * N.toHom (ϖH ^ n)

theorem

normSubgroup_mul_iff_right

L2442 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normSubgroup_mul_iff_right

Documentation

Membership in the norm subgroup is invariant under right multiplication by a norm.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normSubgroup_mul_iff_right {x h : G} (hh : h ∈ N.normSubgroup) :
    x * h ∈ N.normSubgroup ↔ x ∈ N.normSubgroup

theorem

normSubgroup_mul_iff_left

L2454 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normSubgroup_mul_iff_left

Documentation

Membership in the norm subgroup is invariant under left multiplication by a norm.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normSubgroup_mul_iff_left {h x : G} (hh : h ∈ N.normSubgroup) :
    h * x ∈ N.normSubgroup ↔ x ∈ N.normSubgroup

theorem

normSubgroup_div_iff_right

L2465 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normSubgroup_div_iff_right

Documentation

Dividing on the right by a norm preserves norm-subgroup membership.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normSubgroup_div_iff_right {x h : G} (hh : h ∈ N.normSubgroup) :
    x / h ∈ N.normSubgroup ↔ x ∈ N.normSubgroup

theorem

normSubgroup_div_iff_left

L2473 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normSubgroup_div_iff_left

Documentation

Dividing a norm on the left by an element detects membership of that element in the norm subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normSubgroup_div_iff_left {h x : G} (hh : h ∈ N.normSubgroup) :
    h / x ∈ N.normSubgroup ↔ x ∈ N.normSubgroup

theorem

normSubgroup_mul_norm_iff

L2488 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normSubgroup_mul_norm_iff

Documentation

Characterizes x * N.toHom y ∈ N.normSubgroup by the equivalent condition x ∈ N.normSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normSubgroup_mul_norm_iff (x : G) (y : H) :
    x * N.toHom y ∈ N.normSubgroup ↔ x ∈ N.normSubgroup

theorem

normSubgroup_norm_mul_iff

L2496 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normSubgroup_norm_mul_iff

Documentation

Characterizes N.toHom y * x ∈ N.normSubgroup by the equivalent condition x ∈ N.normSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normSubgroup_norm_mul_iff (y : H) (x : G) :
    N.toHom y * x ∈ N.normSubgroup ↔ x ∈ N.normSubgroup

theorem

normSubgroup_div_norm_iff

L2504 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normSubgroup_div_norm_iff

Documentation

Characterizes x / N.toHom y ∈ N.normSubgroup by the equivalent condition x ∈ N.normSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normSubgroup_div_norm_iff (x : G) (y : H) :
    x / N.toHom y ∈ N.normSubgroup ↔ x ∈ N.normSubgroup

theorem

normSubgroup_norm_div_iff

L2512 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normSubgroup_norm_div_iff

Documentation

Characterizes N.toHom y / x ∈ N.normSubgroup by the equivalent condition x ∈ N.normSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normSubgroup_norm_div_iff (y : H) (x : G) :
    N.toHom y / x ∈ N.normSubgroup ↔ x ∈ N.normSubgroup

theorem

norm_mul_eq_of_norm_eq_div

L2519 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.norm_mul_eq_of_norm_eq_div

Documentation

A norm equality against a quotient can be rewritten as a right-coset equality.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem norm_mul_eq_of_norm_eq_div {x y : G} {z : H}
    (hz : N.toHom z = x / y) :
    N.toHom z * y = x

theorem

norm_eq_div_of_norm_mul_eq

L2527 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.norm_eq_div_of_norm_mul_eq

Documentation

A right-coset equality can be rewritten as a norm equality against a quotient.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem norm_eq_div_of_norm_mul_eq {x y : G} {z : H}
    (hz : N.toHom z * y = x) :
    N.toHom z = x / y

theorem

mul_norm_eq_of_norm_eq_inv_mul

L2535 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.mul_norm_eq_of_norm_eq_inv_mul

Documentation

A norm equality against a left quotient can be rewritten as a left-coset equality.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem mul_norm_eq_of_norm_eq_inv_mul {x y : G} {z : H}
    (hz : N.toHom z = y⁻¹ * x) :
    y * N.toHom z = x

theorem

norm_eq_inv_mul_of_mul_norm_eq

L2543 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.norm_eq_inv_mul_of_mul_norm_eq

Documentation

A left-coset equality can be rewritten as a norm equality against a left quotient.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem norm_eq_inv_mul_of_mul_norm_eq {x y : G} {z : H}
    (hz : y * N.toHom z = x) :
    N.toHom z = y⁻¹ * x

theorem

div_mem_normSubgroup_iff_exists_norm_mul_eq

L2551 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.div_mem_normSubgroup_iff_exists_norm_mul_eq

Documentation

Quotient membership in the norm subgroup is the same as representing the left element as a norm times the right element.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem div_mem_normSubgroup_iff_exists_norm_mul_eq (x y : G) :
    x / y ∈ N.normSubgroup ↔ ∃ z : H, N.toHom z * y = x

theorem

exists_norm_mul_eq_of_div_mem_normSubgroup

L2562 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.exists_norm_mul_eq_of_div_mem_normSubgroup

Documentation

Establishes the identity ∃ z : H, N.toHom z * y = x.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem exists_norm_mul_eq_of_div_mem_normSubgroup
    {x y : G} (hxy : x / y ∈ N.normSubgroup) :
    ∃ z : H, N.toHom z * y = x

theorem

div_mem_normSubgroup_of_exists_norm_mul_eq

L2568 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.div_mem_normSubgroup_of_exists_norm_mul_eq

Documentation

Establishes the membership statement x / y ∈ N.normSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem div_mem_normSubgroup_of_exists_norm_mul_eq
    {x y : G} (hxy : ∃ z : H, N.toHom z * y = x) :
    x / y ∈ N.normSubgroup

theorem

inv_mul_mem_normSubgroup_iff_exists_mul_norm_eq

L2575 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.inv_mul_mem_normSubgroup_iff_exists_mul_norm_eq

Documentation

Left-quotient membership in the norm subgroup is the same as representing the left element as the right element times a norm.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem inv_mul_mem_normSubgroup_iff_exists_mul_norm_eq (x y : G) :
    y⁻¹ * x ∈ N.normSubgroup ↔ ∃ z : H, y * N.toHom z = x

theorem

exists_mul_norm_eq_of_inv_mul_mem_normSubgroup

L2586 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.exists_mul_norm_eq_of_inv_mul_mem_normSubgroup

Documentation

Establishes the identity ∃ z : H, y * N.toHom z = x.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem exists_mul_norm_eq_of_inv_mul_mem_normSubgroup
    {x y : G} (hxy : y⁻¹ * x ∈ N.normSubgroup) :
    ∃ z : H, y * N.toHom z = x

theorem

inv_mul_mem_normSubgroup_of_exists_mul_norm_eq

L2592 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.inv_mul_mem_normSubgroup_of_exists_mul_norm_eq

Documentation

Establishes the membership statement y⁻¹ * x ∈ N.normSubgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem inv_mul_mem_normSubgroup_of_exists_mul_norm_eq
    {x y : G} (hxy : ∃ z : H, y * N.toHom z = x) :
    y⁻¹ * x ∈ N.normSubgroup

theorem

normQuotient_mk_eq_iff_exists_mul_norm_eq

L2599 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normQuotient_mk_eq_iff_exists_mul_norm_eq

Documentation

Equality in the norm quotient is equivalent to a left-coset representative equation when the norm subgroup is normal.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normQuotient_mk_eq_iff_exists_mul_norm_eq
    [(N.normSubgroup).Normal] (x y : G) :
    QuotientGroup.mk' N.normSubgroup x =
        QuotientGroup.mk' N.normSubgroup y ↔
      ∃ z : H, y * N.toHom z = x

theorem

zeroSubgroupQuotientToNormQuotient_mk_eq_iff_exists_mul_norm_eq

L2609 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.zeroSubgroupQuotientToNormQuotient_mk_eq_iff_exists_mul_norm_eq

Documentation

Equality after mapping from G ⧸ zeroSubgroup to the norm quotient is equivalent to a left-coset representative equation.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem zeroSubgroupQuotientToNormQuotient_mk_eq_iff_exists_mul_norm_eq
    [(N.normSubgroup).Normal]
    (hzero : vG.zeroSubgroup ≤ N.normSubgroup) (x y : G) :
    N.zeroSubgroupQuotientToNormQuotient hzero
        (QuotientGroup.mk' vG.zeroSubgroup x) =
      N.zeroSubgroupQuotientToNormQuotient hzero
        (QuotientGroup.mk' vG.zeroSubgroup y) ↔
      ∃ z : H, y * N.toHom z = x

theorem

normSubgroup_eq_sup_of_source_decomposition

L2626 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normSubgroup_eq_sup_of_source_decomposition

Documentation

If every source element is a source-unit part times a power of ϖ, if the image of the chosen source-unit subgroup is P, and if ϖ maps to γ, then the norm subgroup is P ∨ <γ>.

This is the group-theoretic core of finite Lubin--Tate norm-subgroup formulas, stated without a theorem-carrying presentation structure.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normSubgroup_eq_sup_of_source_decomposition
    (U : Subgroup H) (P : Subgroup G) (ϖ : H) (γ : G)
    (hdecomp :
      ∀ y : H, ∃ u : H, u ∈ U ∧ ∃ n : ℤ, y = u * ϖ ^ n)
    (hU : Subgroup.map N.toHom U = P)
    (hϖ : N.toHom ϖ = γ) :
    N.normSubgroup = P ⊔ Subgroup.closure ({γ} : Set G)

theorem

exists_targetSubgroup_mul_generator_zpow_of_mem_normSubgroup

L2664 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.exists_targetSubgroup_mul_generator_zpow_of_mem_normSubgroup

Documentation

Normal form for an element of the norm subgroup from a source decomposition and a prescribed image of the source-unit subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem exists_targetSubgroup_mul_generator_zpow_of_mem_normSubgroup
    (U : Subgroup H) (P : Subgroup G) (ϖ : H) (γ : G)
    (hdecomp :
      ∀ y : H, ∃ u : H, u ∈ U ∧ ∃ n : ℤ, y = u * ϖ ^ n)
    (hU : Subgroup.map N.toHom U = P)
    (hϖ : N.toHom ϖ = γ)
    {x : G} (hx : x ∈ N.normSubgroup) :
    ∃ p : G, p ∈ P ∧ ∃ n : ℤ, x = p * γ ^ n

theorem

mem_normSubgroup_of_targetSubgroup_mul_generator_zpow

L2685 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.mem_normSubgroup_of_targetSubgroup_mul_generator_zpow

Documentation

A target-subgroup element times a power of the selected generator lies in the norm subgroup when the target subgroup is the image of the chosen source subgroup and the generator is the norm of ϖ.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem mem_normSubgroup_of_targetSubgroup_mul_generator_zpow
    (U : Subgroup H) (P : Subgroup G) (ϖ : H) (γ : G)
    (hU : Subgroup.map N.toHom U = P)
    (hϖ : N.toHom ϖ = γ)
    {p x : G} (hp : p ∈ P) {n : ℤ} (hx : x = p * γ ^ n) :
    x ∈ N.normSubgroup

theorem

mem_normSubgroup_iff_exists_targetSubgroup_mul_generator_zpow

L2703 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.mem_normSubgroup_iff_exists_targetSubgroup_mul_generator_zpow

Documentation

Elementwise normal-form characterization of the norm subgroup from source unit decomposition data.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem mem_normSubgroup_iff_exists_targetSubgroup_mul_generator_zpow
    (U : Subgroup H) (P : Subgroup G) (ϖ : H) (γ : G)
    (hdecomp :
      ∀ y : H, ∃ u : H, u ∈ U ∧ ∃ n : ℤ, y = u * ϖ ^ n)
    (hU : Subgroup.map N.toHom U = P)
    (hϖ : N.toHom ϖ = γ) (x : G) :
    x ∈ N.normSubgroup ↔
      ∃ p : G, p ∈ P ∧ ∃ n : ℤ, x = p * γ ^ n

theorem

exists_valuation_generator_multiple_of_mem_normSubgroup

L2721 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.exists_valuation_generator_multiple_of_mem_normSubgroup

Documentation

If the target subgroup in a norm-subgroup normal form has valuation zero, then every norm-subgroup element has valuation a multiple of the selected generator's valuation.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem exists_valuation_generator_multiple_of_mem_normSubgroup
    (U : Subgroup H) (P : Subgroup G) (ϖ : H) (γ : G)
    (hdecomp :
      ∀ y : H, ∃ u : H, u ∈ U ∧ ∃ n : ℤ, y = u * ϖ ^ n)
    (hU : Subgroup.map N.toHom U = P)
    (hϖ : N.toHom ϖ = γ)
    (hP : P ≤ vG.zeroSubgroup)
    {x : G} (hx : x ∈ N.normSubgroup) :
    ∃ n : ℤ, vG.val x = n * vG.val γ

theorem

valuation_generator_of_source_uniformizer

L2740 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.valuation_generator_of_source_uniformizer

Documentation

If the selected source element is a source uniformizer, the valuation of its norm-image generator is the residue degree.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem valuation_generator_of_source_uniformizer
    {ϖ : H} {γ : G}
    (hϖH : vH.IsUniformizer ϖ) (hϖ : N.toHom ϖ = γ) :
    vG.val γ = (N.residueDegree : ℤ)

theorem

targetSubgroup_normal_form_exponent_zero_of_equal_valuation

L2752 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.targetSubgroup_normal_form_exponent_zero_of_equal_valuation

Documentation

In a normal form x / y = p * γ^n, equal target valuations force the generator exponent to be zero, provided P has valuation zero and γ has nonzero valuation.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem targetSubgroup_normal_form_exponent_zero_of_equal_valuation
    (P : Subgroup G) (hP : P ≤ vG.zeroSubgroup)
    {x y p γ : G} (hp : p ∈ P) {n : ℤ}
    (hxy : x / y = p * γ ^ n)
    (hvxy : vG.val x = vG.val y)
    (hγ : vG.val γ ≠ 0) :
    n = 0

theorem

targetSubgroup_quotient_of_mem_normSubgroup_of_equal_valuation

L2770 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.targetSubgroup_quotient_of_mem_normSubgroup_of_equal_valuation

Documentation

Equal target valuations reduce norm-quotient membership to the target subgroup part of a source-decomposition normal form.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem targetSubgroup_quotient_of_mem_normSubgroup_of_equal_valuation
    (U : Subgroup H) (P : Subgroup G) (ϖ : H) (γ : G)
    (hdecomp :
      ∀ y : H, ∃ u : H, u ∈ U ∧ ∃ n : ℤ, y = u * ϖ ^ n)
    (hU : Subgroup.map N.toHom U = P)
    (hϖ : N.toHom ϖ = γ)
    (hP : P ≤ vG.zeroSubgroup)
    (hγ : vG.val γ ≠ 0)
    {x y : G} (hxyN : x / y ∈ N.normSubgroup)
    (hvxy : vG.val x = vG.val y) :
    ∃ p : G, p ∈ P ∧ x / y = p

theorem

normSubgroup_quotient_iff_targetSubgroup_of_equal_valuation

L2792 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normSubgroup_quotient_iff_targetSubgroup_of_equal_valuation

Documentation

With equal target valuations, norm-quotient membership is equivalent to having a representative in the target subgroup part.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normSubgroup_quotient_iff_targetSubgroup_of_equal_valuation
    (U : Subgroup H) (P : Subgroup G) (ϖ : H) (γ : G)
    (hdecomp :
      ∀ y : H, ∃ u : H, u ∈ U ∧ ∃ n : ℤ, y = u * ϖ ^ n)
    (hU : Subgroup.map N.toHom U = P)
    (hϖ : N.toHom ϖ = γ)
    (hP : P ≤ vG.zeroSubgroup)
    (hγ : vG.val γ ≠ 0)
    {x y : G} (hvxy : vG.val x = vG.val y) :
    x / y ∈ N.normSubgroup ↔
      ∃ p : G, p ∈ P ∧ x / y = p

theorem

targetSubgroup_quotient_of_mem_normSubgroup_of_equal_valuation_of_source_uniformizer

L2813 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.targetSubgroup_quotient_of_mem_normSubgroup_of_equal_valuation_of_source_uniformizer

Documentation

The source-uniformizer/residue-degree version of targetSubgroup_quotient_of_mem_normSubgroup_of_equal_valuation.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem targetSubgroup_quotient_of_mem_normSubgroup_of_equal_valuation_of_source_uniformizer
    (U : Subgroup H) (P : Subgroup G) (ϖ : H) (γ : G)
    (hdecomp :
      ∀ y : H, ∃ u : H, u ∈ U ∧ ∃ n : ℤ, y = u * ϖ ^ n)
    (hU : Subgroup.map N.toHom U = P)
    (hϖ : N.toHom ϖ = γ)
    (hP : P ≤ vG.zeroSubgroup)
    (hϖH : vH.IsUniformizer ϖ)
    (hdeg : N.residueDegree ≠ 0)
    {x y : G} (hxyN : x / y ∈ N.normSubgroup)
    (hvxy : vG.val x = vG.val y) :
    ∃ p : G, p ∈ P ∧ x / y = p

theorem

normSubgroup_quotient_iff_targetSubgroup_of_equal_valuation_of_source_uniformizer

L2832 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.normSubgroup_quotient_iff_targetSubgroup_of_equal_valuation_of_source_uniformizer

Documentation

The source-uniformizer/residue-degree version of the equal-valuation criterion for norm-quotient membership.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem normSubgroup_quotient_iff_targetSubgroup_of_equal_valuation_of_source_uniformizer
    (U : Subgroup H) (P : Subgroup G) (ϖ : H) (γ : G)
    (hdecomp :
      ∀ y : H, ∃ u : H, u ∈ U ∧ ∃ n : ℤ, y = u * ϖ ^ n)
    (hU : Subgroup.map N.toHom U = P)
    (hϖ : N.toHom ϖ = γ)
    (hP : P ≤ vG.zeroSubgroup)
    (hϖH : vH.IsUniformizer ϖ)
    (hdeg : N.residueDegree ≠ 0)
    {x y : G} (hvxy : vG.val x = vG.val y) :
    x / y ∈ N.normSubgroup ↔
      ∃ p : G, p ∈ P ∧ x / y = p

theorem

equal_valuation_of_targetSubgroup_quotient

L2851 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.equal_valuation_of_targetSubgroup_quotient

Documentation

A target-subgroup representative of a quotient has zero valuation displacement when the target subgroup has valuation zero.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace LocalFieldTheory
noncomputable section
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)

Lean source · statement

theorem equal_valuation_of_targetSubgroup_quotient
    (P : Subgroup G) (hP : P ≤ vG.zeroSubgroup)
    {x y p : G} (hp : p ∈ P) (hxy : x / y = p) :
    vG.val x = vG.val y

Module documentation

Declarations