Module

Integer.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.Integer

36 declarations indexed from sourceView source ↗

Module documentation

Integer value-group arithmetic

The tame Abhyankar value-group step reduces to lcm arithmetic in a rank-one integer value group. This file isolates that arithmetic without assuming any field-theoretic ramification comparison.

Imports2

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.ValueGroup
Mathlib.Data.Int.ModEq

Imported by2

theorem

int_lcm_dvd_iff_dvd_and_dvd

L27 ↗

TameAbhyankar.int_lcm_dvd_iff_dvd_and_dvd

Documentation

Membership in both integer-multiple value subgroups is the same as membership in the subgroup cut out by the lcm. This is the integer divisibility core of the value-group computation used by tame Abhyankar.

Source context 3 commands

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

noncomputable section
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField

Lean source · statement

theorem int_lcm_dvd_iff_dvd_and_dvd (d e n : ℤ) :
    ((d.lcm e : ℕ) : ℤ) ∣ n ↔ d ∣ n ∧ e ∣ n

theorem

int_lcm_dvd_of_dvd_of_dvd

L35 ↗

TameAbhyankar.int_lcm_dvd_of_dvd_of_dvd

Documentation

Introduction form for the integer value-group lcm divisibility.

Source context 3 commands

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

noncomputable section
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField

Lean source · statement

theorem int_lcm_dvd_of_dvd_of_dvd {d e n : ℤ}
    (hd : d ∣ n) (he : e ∣ n) :
    ((d.lcm e : ℕ) : ℤ) ∣ n

theorem

int_dvd_left_of_lcm_dvd

L41 ↗

TameAbhyankar.int_dvd_left_of_lcm_dvd

Documentation

Left projection from lcm divisibility in the integer value group.

Source context 3 commands

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

noncomputable section
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField

Lean source · statement

theorem int_dvd_left_of_lcm_dvd {d e n : ℤ}
    (h : ((d.lcm e : ℕ) : ℤ) ∣ n) :
    d ∣ n

theorem

int_dvd_right_of_lcm_dvd

L47 ↗

TameAbhyankar.int_dvd_right_of_lcm_dvd

Documentation

Right projection from lcm divisibility in the integer value group.

Source context 3 commands

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

noncomputable section
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField

Lean source · statement

theorem int_dvd_right_of_lcm_dvd {d e n : ℤ}
    (h : ((d.lcm e : ℕ) : ℤ) ∣ n) :
    e ∣ n

theorem

mem_integerMultipleSubgroup_lcm_iff

L54 ↗

TameAbhyankar.mem_integerMultipleSubgroup_lcm_iff

Documentation

Existing LocalFieldTheory.DiscreteValuationField.integerMultipleSubgroup form of the lcm value-group intersection.

Source context 3 commands

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

noncomputable section
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField

Lean source · statement

theorem mem_integerMultipleSubgroup_lcm_iff
    (d e : ℤ) (n : Multiplicative ℤ) :
    n ∈ integerMultipleSubgroup ((d.lcm e : ℕ) : ℤ) ↔
      n ∈ integerMultipleSubgroup d ∧
        n ∈ integerMultipleSubgroup e

theorem

integerMultipleSubgroup_lcm_eq_inf

L66 ↗

TameAbhyankar.integerMultipleSubgroup_lcm_eq_inf

Documentation

The subgroup of value exponents divisible by lcm d e is the intersection of the subgroups divisible by d and by e.

Source context 3 commands

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

noncomputable section
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField

Lean source · statement

theorem integerMultipleSubgroup_lcm_eq_inf (d e : ℤ) :
    integerMultipleSubgroup ((d.lcm e : ℕ) : ℤ) =
      integerMultipleSubgroup d ⊓ integerMultipleSubgroup e

theorem

mem_integerMultipleSubgroup_lcm_of_mem_left_of_mem_right

L75 ↗

TameAbhyankar.mem_integerMultipleSubgroup_lcm_of_mem_left_of_mem_right

Documentation

Introduction form for the lcm value-subgroup intersection.

Source context 3 commands

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

noncomputable section
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField

Lean source · statement

theorem mem_integerMultipleSubgroup_lcm_of_mem_left_of_mem_right
    {d e : ℤ} {n : Multiplicative ℤ}
    (hd : n ∈ integerMultipleSubgroup d)
    (he : n ∈ integerMultipleSubgroup e) :
    n ∈ integerMultipleSubgroup ((d.lcm e : ℕ) : ℤ)

theorem

integerMultipleSubgroup_le_iff_dvd

L84 ↗

TameAbhyankar.integerMultipleSubgroup_le_iff_dvd

Documentation

Inclusion between integer-multiple value subgroups is exactly divisibility of the corresponding integer steps, with the order reversed.

Source context 3 commands

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

noncomputable section
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField

Lean source · statement

theorem integerMultipleSubgroup_le_iff_dvd (a b : ℤ) :
    integerMultipleSubgroup b ≤ integerMultipleSubgroup a ↔ a ∣ b

theorem

integerMultipleSubgroup_le_inf_iff_lcm_dvd

L98 ↗

TameAbhyankar.integerMultipleSubgroup_le_inf_iff_lcm_dvd

Documentation

If an integer-multiple value subgroup lies in the intersection of the two lower value-step subgroups, its step is divisible by the lcm of the two lower steps.

Source context 3 commands

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

noncomputable section
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField

Lean source · statement

theorem integerMultipleSubgroup_le_inf_iff_lcm_dvd (n d e : ℤ) :
    integerMultipleSubgroup n ≤ integerMultipleSubgroup d ⊓
        integerMultipleSubgroup e ↔
      ((d.lcm e : ℕ) : ℤ) ∣ n

theorem

int_lcm_dvd_of_integerMultipleSubgroup_le_of_le

L107 ↗

TameAbhyankar.int_lcm_dvd_of_integerMultipleSubgroup_le_of_le

Documentation

Introduction form for extracting lcm divisibility from two integer-multiple subgroup inclusions.

Source context 3 commands

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

noncomputable section
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField

Lean source · statement

theorem int_lcm_dvd_of_integerMultipleSubgroup_le_of_le
    {n d e : ℤ}
    (hd : integerMultipleSubgroup n ≤ integerMultipleSubgroup d)
    (he : integerMultipleSubgroup n ≤ integerMultipleSubgroup e) :
    ((d.lcm e : ℕ) : ℤ) ∣ n

theorem

subgroupValueSubgroup_le_valueSubgroup

L124 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.subgroupValueSubgroup_le_valueSubgroup

Documentation

The values attained by a subgroup form a sub-value group of the ambient value subgroup.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open TameAbhyankar
variable {G : Type _} [Group G]

Lean source · statement

theorem subgroupValueSubgroup_le_valueSubgroup
    (V : MultiplicativeIntegerValuation G) (S : Subgroup G) :
    V.subgroupValueSubgroup S ≤ V.valueSubgroup

theorem

subgroupValueSubgroup_le_integerMultipleSubgroup_lcm

L134 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.subgroupValueSubgroup_le_integerMultipleSubgroup_lcm

Documentation

Introduction form for lcm divisibility on a subgroup value image.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open TameAbhyankar
variable {G : Type _} [Group G]

Lean source · statement

theorem subgroupValueSubgroup_le_integerMultipleSubgroup_lcm
    (V : MultiplicativeIntegerValuation G) (S : Subgroup G) {d e : ℤ}
    (hd : V.subgroupValueSubgroup S ≤ integerMultipleSubgroup d)
    (he : V.subgroupValueSubgroup S ≤ integerMultipleSubgroup e) :
    V.subgroupValueSubgroup S ≤
      integerMultipleSubgroup ((d.lcm e : ℕ) : ℤ)

theorem

integerMultipleSubgroup_le_subgroupValueSubgroup_of_ofAdd_mem

L145 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.integerMultipleSubgroup_le_subgroupValueSubgroup_of_ofAdd_mem

Documentation

Membership of the generator ofAdd n in a subgroup value image generates the whole integer-multiple subgroup cut out by n.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open TameAbhyankar
variable {G : Type _} [Group G]

Lean source · statement

theorem integerMultipleSubgroup_le_subgroupValueSubgroup_of_ofAdd_mem
    (V : MultiplicativeIntegerValuation G) {S : Subgroup G} {n : ℤ}
    (hn : Multiplicative.ofAdd n ∈ V.subgroupValueSubgroup S) :
    integerMultipleSubgroup n ≤ V.subgroupValueSubgroup S

theorem

integerMultipleSubgroup_le_subgroupValueSubgroup_iff_ofAdd_mem

L154 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.integerMultipleSubgroup_le_subgroupValueSubgroup_iff_ofAdd_mem

Documentation

The integer-multiple subgroup generated by n lies in a subgroup value image exactly when the generator ofAdd n lies in that image.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open TameAbhyankar
variable {G : Type _} [Group G]

Lean source · statement

theorem integerMultipleSubgroup_le_subgroupValueSubgroup_iff_ofAdd_mem
    (V : MultiplicativeIntegerValuation G) (S : Subgroup G) (n : ℤ) :
    integerMultipleSubgroup n ≤ V.subgroupValueSubgroup S ↔
      Multiplicative.ofAdd n ∈ V.subgroupValueSubgroup S

theorem

integerMultipleSubgroup_le_subgroupValueSubgroup_iff_exists_mem_val

L168 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.integerMultipleSubgroup_le_subgroupValueSubgroup_iff_exists_mem_val

Documentation

The subgroup-image inclusion required in the value-group comparison is equivalent to producing an actual subgroup element with valuation n.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open TameAbhyankar
variable {G : Type _} [Group G]

Lean source · statement

theorem integerMultipleSubgroup_le_subgroupValueSubgroup_iff_exists_mem_val
    (V : MultiplicativeIntegerValuation G) (S : Subgroup G) (n : ℤ) :
    integerMultipleSubgroup n ≤ V.subgroupValueSubgroup S ↔
      ∃ x : G, x ∈ S ∧ V.val x = n

theorem

int_lcm_dvd_of_integerMultipleSubgroup_le_subgroupValueSubgroup_of_subgroupValueSubgroup_le

L178 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.int_lcm_dvd_of_integerMultipleSubgroup_le_subgroupValueSubgroup_of_subgroupValueSubgroup_le

Documentation

Subgroup-image sandwich form: if an integer-multiple subgroup maps into a subgroup value image, and that image lies in two lower value-step subgroups, then the image step is divisible by the lcm of the two lower steps.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open TameAbhyankar
variable {G : Type _} [Group G]

Lean source · statement

theorem int_lcm_dvd_of_integerMultipleSubgroup_le_subgroupValueSubgroup_of_subgroupValueSubgroup_le
    (V : MultiplicativeIntegerValuation G) {S : Subgroup G} {n d e : ℤ}
    (himage : integerMultipleSubgroup n ≤ V.subgroupValueSubgroup S)
    (hd : V.subgroupValueSubgroup S ≤ integerMultipleSubgroup d)
    (he : V.subgroupValueSubgroup S ≤ integerMultipleSubgroup e) :
    ((d.lcm e : ℕ) : ℤ) ∣ n

theorem

int_lcm_dvd_of_ofAdd_mem_subgroupValueSubgroup_of_subgroupValueSubgroup_le

L190 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.int_lcm_dvd_of_ofAdd_mem_subgroupValueSubgroup_of_subgroupValueSubgroup_le

Documentation

Membership form of the subgroup-image lcm sandwich: once the generator ofAdd n lies in the subgroup value image, two lower value-step inclusions for that image force n to be divisible by the lcm of the lower steps.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open TameAbhyankar
variable {G : Type _} [Group G]

Lean source · statement

theorem int_lcm_dvd_of_ofAdd_mem_subgroupValueSubgroup_of_subgroupValueSubgroup_le
    (V : MultiplicativeIntegerValuation G) {S : Subgroup G} {n d e : ℤ}
    (hn : Multiplicative.ofAdd n ∈ V.subgroupValueSubgroup S)
    (hd : V.subgroupValueSubgroup S ≤ integerMultipleSubgroup d)
    (he : V.subgroupValueSubgroup S ≤ integerMultipleSubgroup e) :
    ((d.lcm e : ℕ) : ℤ) ∣ n

theorem

valueSubgroup_le_integerMultipleSubgroup_iff

L203 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.valueSubgroup_le_integerMultipleSubgroup_iff

Documentation

A value-subgroup inclusion into an integer-multiple subgroup is exactly a divisibility statement for every valuation exponent.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open TameAbhyankar
variable {G : Type _} [Group G]

Lean source · statement

theorem valueSubgroup_le_integerMultipleSubgroup_iff
    (V : MultiplicativeIntegerValuation G) (d : ℤ) :
    V.valueSubgroup ≤ integerMultipleSubgroup d ↔
      ∀ x : G, d ∣ V.val x

theorem

valueSubgroup_le_integerMultipleSubgroup_lcm_iff

L229 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.valueSubgroup_le_integerMultipleSubgroup_lcm_iff

Documentation

A value subgroup lies in the lcm multiple subgroup exactly when it lies in both lower multiple subgroups. This is the subgroup-inclusion form needed when the ramification-image comparison has produced the two lower value-step inclusions.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open TameAbhyankar
variable {G : Type _} [Group G]

Lean source · statement

theorem valueSubgroup_le_integerMultipleSubgroup_lcm_iff
    (V : MultiplicativeIntegerValuation G) (d e : ℤ) :
    V.valueSubgroup ≤ integerMultipleSubgroup ((d.lcm e : ℕ) : ℤ) ↔
      V.valueSubgroup ≤ integerMultipleSubgroup d ∧
        V.valueSubgroup ≤ integerMultipleSubgroup e

theorem

valueSubgroup_le_integerMultipleSubgroup_lcm

L238 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.valueSubgroup_le_integerMultipleSubgroup_lcm

Documentation

Introduction form for the lcm value-subgroup inclusion.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open TameAbhyankar
variable {G : Type _} [Group G]

Lean source · statement

theorem valueSubgroup_le_integerMultipleSubgroup_lcm
    (V : MultiplicativeIntegerValuation G) {d e : ℤ}
    (hd : V.valueSubgroup ≤ integerMultipleSubgroup d)
    (he : V.valueSubgroup ≤ integerMultipleSubgroup e) :
    V.valueSubgroup ≤ integerMultipleSubgroup ((d.lcm e : ℕ) : ℤ)

theorem

integerMultipleSubgroup_le_valueSubgroup_of_exists_val

L248 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.integerMultipleSubgroup_le_valueSubgroup_of_exists_val

Documentation

If the valuation takes the value n, then all multiples of n lie in the value subgroup. This supplies the image-subgroup inclusion used by the ramification-image comparison from an actual value generator.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open TameAbhyankar
variable {G : Type _} [Group G]

Lean source · statement

theorem integerMultipleSubgroup_le_valueSubgroup_of_exists_val
    (V : MultiplicativeIntegerValuation G) {n : ℤ}
    (hn : ∃ x : G, V.val x = n) :
    integerMultipleSubgroup n ≤ V.valueSubgroup

theorem

integerMultipleSubgroup_le_valueSubgroup_of_ofAdd_mem

L264 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.integerMultipleSubgroup_le_valueSubgroup_of_ofAdd_mem

Documentation

Membership of Multiplicative.ofAdd n in the value subgroup generates the whole integer-multiple subgroup cut out by n.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open TameAbhyankar
variable {G : Type _} [Group G]

Lean source · statement

theorem integerMultipleSubgroup_le_valueSubgroup_of_ofAdd_mem
    (V : MultiplicativeIntegerValuation G) {n : ℤ}
    (hn : Multiplicative.ofAdd n ∈ V.valueSubgroup) :
    integerMultipleSubgroup n ≤ V.valueSubgroup

theorem

integerMultipleSubgroup_le_valueSubgroup_iff_ofAdd_mem

L273 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.integerMultipleSubgroup_le_valueSubgroup_iff_ofAdd_mem

Documentation

The whole integer-multiple subgroup generated by n lies in the value subgroup exactly when its generator lies in the value subgroup.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open TameAbhyankar
variable {G : Type _} [Group G]

Lean source · statement

theorem integerMultipleSubgroup_le_valueSubgroup_iff_ofAdd_mem
    (V : MultiplicativeIntegerValuation G) (n : ℤ) :
    integerMultipleSubgroup n ≤ V.valueSubgroup ↔
      Multiplicative.ofAdd n ∈ V.valueSubgroup

theorem

integerMultipleSubgroup_le_valueSubgroup_iff_exists_val

L287 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.integerMultipleSubgroup_le_valueSubgroup_iff_exists_val

Documentation

The image-subgroup inclusion required in the value-group comparison is equivalent to producing an actual element with valuation n.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open TameAbhyankar
variable {G : Type _} [Group G]

Lean source · statement

theorem integerMultipleSubgroup_le_valueSubgroup_iff_exists_val
    (V : MultiplicativeIntegerValuation G) (n : ℤ) :
    integerMultipleSubgroup n ≤ V.valueSubgroup ↔ ∃ x : G, V.val x = n

theorem

int_lcm_dvd_of_integerMultipleSubgroup_le_valueSubgroup_of_valueSubgroup_le

L296 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.int_lcm_dvd_of_integerMultipleSubgroup_le_valueSubgroup_of_valueSubgroup_le

Documentation

If an integer-multiple value subgroup maps into a valuation value subgroup, and that value subgroup lies in two lower value-step subgroups, then the image step is divisible by the lcm of the two lower steps.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open TameAbhyankar
variable {G : Type _} [Group G]

Lean source · statement

theorem int_lcm_dvd_of_integerMultipleSubgroup_le_valueSubgroup_of_valueSubgroup_le
    (V : MultiplicativeIntegerValuation G) {n d e : ℤ}
    (himage : integerMultipleSubgroup n ≤ V.valueSubgroup)
    (hd : V.valueSubgroup ≤ integerMultipleSubgroup d)
    (he : V.valueSubgroup ≤ integerMultipleSubgroup e) :
    ((d.lcm e : ℕ) : ℤ) ∣ n

theorem

int_lcm_dvd_of_exists_val_of_valueSubgroup_le

L308 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.int_lcm_dvd_of_exists_val_of_valueSubgroup_le

Documentation

Generator form of the value-subgroup sandwich: once the value subgroup has a value generator n, two lower value-step inclusions force n to be divisible by the lcm of the two lower steps.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open TameAbhyankar
variable {G : Type _} [Group G]

Lean source · statement

theorem int_lcm_dvd_of_exists_val_of_valueSubgroup_le
    (V : MultiplicativeIntegerValuation G) {n d e : ℤ}
    (hn : ∃ x : G, V.val x = n)
    (hd : V.valueSubgroup ≤ integerMultipleSubgroup d)
    (he : V.valueSubgroup ≤ integerMultipleSubgroup e) :
    ((d.lcm e : ℕ) : ℤ) ∣ n

theorem

forall_lcm_dvd_val_iff

L318 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.forall_lcm_dvd_val_iff

Documentation

Elementwise valuation-exponent form of the lcm criterion.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open TameAbhyankar
variable {G : Type _} [Group G]

Lean source · statement

theorem forall_lcm_dvd_val_iff
    (V : MultiplicativeIntegerValuation G) (d e : ℤ) :
    (∀ x : G, ((d.lcm e : ℕ) : ℤ) ∣ V.val x) ↔
      (∀ x : G, d ∣ V.val x) ∧
        (∀ x : G, e ∣ V.val x)

theorem

lcm_dvd_val_of_dvd_val_of_dvd_val

L330 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.lcm_dvd_val_of_dvd_val_of_dvd_val

Documentation

Introduction form for the elementwise valuation-exponent lcm criterion.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open TameAbhyankar
variable {G : Type _} [Group G]

Lean source · statement

theorem lcm_dvd_val_of_dvd_val_of_dvd_val
    (V : MultiplicativeIntegerValuation G) {d e : ℤ}
    (hd : ∀ x : G, d ∣ V.val x)
    (he : ∀ x : G, e ∣ V.val x) :
    ∀ x : G, ((d.lcm e : ℕ) : ℤ) ∣ V.val x

theorem

valuationHom_mem_integerMultipleSubgroup_lcm_of_mem_left_of_mem_right

L338 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.valuationHom_mem_integerMultipleSubgroup_lcm_of_mem_left_of_mem_right

Documentation

Elementwise valuation form of the lcm value-subgroup inclusion.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open TameAbhyankar
variable {G : Type _} [Group G]

Lean source · statement

theorem valuationHom_mem_integerMultipleSubgroup_lcm_of_mem_left_of_mem_right
    (V : MultiplicativeIntegerValuation G) {d e : ℤ} (x : G)
    (hd : V.valuationHom x ∈ integerMultipleSubgroup d)
    (he : V.valuationHom x ∈ integerMultipleSubgroup e) :
    V.valuationHom x ∈ integerMultipleSubgroup ((d.lcm e : ℕ) : ℤ)

theorem

exists_val_residueDegree_of_source_uniformizer

L357 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.exists_val_residueDegree_of_source_uniformizer

Documentation

A source uniformizer for a valued norm produces a target element whose valuation is the norm residue degree.

Source context 6 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.ValuedNorm
open TameAbhyankar
variable {G H : Type _} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}

Lean source · statement

theorem exists_val_residueDegree_of_source_uniformizer
    (N : ValuedNorm vG vH) {ϖ : H} (hϖ : vH.IsUniformizer ϖ) :
    ∃ x : G, vG.val x = (N.residueDegree : ℤ)

theorem

integerMultipleSubgroup_residueDegree_le_valueSubgroup_of_source_uniformizer

L365 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.integerMultipleSubgroup_residueDegree_le_valueSubgroup_of_source_uniformizer

Documentation

The value subgroup generated by the norm image of a source uniformizer contains the integer-multiple subgroup cut out by the residue degree.

Source context 6 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.ValuedNorm
open TameAbhyankar
variable {G H : Type _} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}

Lean source · statement

theorem integerMultipleSubgroup_residueDegree_le_valueSubgroup_of_source_uniformizer
    (N : ValuedNorm vG vH) {ϖ : H} (hϖ : vH.IsUniformizer ϖ) :
    integerMultipleSubgroup (N.residueDegree : ℤ) ≤ vG.valueSubgroup

theorem

dvd_residueDegree_of_source_uniformizer_of_valueSubgroup_le

L373 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.dvd_residueDegree_of_source_uniformizer_of_valueSubgroup_le

Documentation

A lower value-step inclusion forces the valued norm residue degree to be divisible by that step, once the source valuation has a uniformizer.

Source context 6 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.ValuedNorm
open TameAbhyankar
variable {G H : Type _} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}

Lean source · statement

theorem dvd_residueDegree_of_source_uniformizer_of_valueSubgroup_le
    (N : ValuedNorm vG vH) {ϖ : H} (hϖ : vH.IsUniformizer ϖ)
    {d : ℤ} (hd : vG.valueSubgroup ≤ integerMultipleSubgroup d) :
    d ∣ (N.residueDegree : ℤ)

theorem

lcm_dvd_residueDegree_of_source_uniformizer_of_valueSubgroup_le

L386 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.lcm_dvd_residueDegree_of_source_uniformizer_of_valueSubgroup_le

Documentation

Two lower value-step inclusions force the valued norm residue degree to be divisible by their lcm. This is the norm-image input shape needed by the tame Abhyankar value-group comparison.

Source context 6 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.ValuedNorm
open TameAbhyankar
variable {G H : Type _} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}

Lean source · statement

theorem lcm_dvd_residueDegree_of_source_uniformizer_of_valueSubgroup_le
    (N : ValuedNorm vG vH) {ϖ : H} (hϖ : vH.IsUniformizer ϖ)
    {d e : ℤ}
    (hd : vG.valueSubgroup ≤ integerMultipleSubgroup d)
    (he : vG.valueSubgroup ≤ integerMultipleSubgroup e) :
    ((d.lcm e : ℕ) : ℤ) ∣ (N.residueDegree : ℤ)

theorem

subgroupValueSubgroup_normSubgroup_eq_integerMultipleSubgroup

L398 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.subgroupValueSubgroup_normSubgroup_eq_integerMultipleSubgroup

Documentation

With a source uniformizer, the valuation values attained on the valued norm subgroup are exactly the residue-degree multiples.

Source context 6 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.ValuedNorm
open TameAbhyankar
variable {G H : Type _} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}

Lean source · statement

theorem subgroupValueSubgroup_normSubgroup_eq_integerMultipleSubgroup
    (N : ValuedNorm vG vH) {ϖ : H} (hϖ : vH.IsUniformizer ϖ) :
    vG.subgroupValueSubgroup N.normSubgroup =
      integerMultipleSubgroup (N.residueDegree : ℤ)

theorem

dvd_residueDegree_of_source_uniformizer_of_normSubgroupValueSubgroup_le

L420 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.dvd_residueDegree_of_source_uniformizer_of_normSubgroupValueSubgroup_le

Documentation

A lower value-step inclusion on the actual valued-norm image forces the valued norm residue degree to be divisible by that step.

Source context 6 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.ValuedNorm
open TameAbhyankar
variable {G H : Type _} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}

Lean source · statement

theorem dvd_residueDegree_of_source_uniformizer_of_normSubgroupValueSubgroup_le
    (N : ValuedNorm vG vH) {ϖ : H} (hϖ : vH.IsUniformizer ϖ)
    {d : ℤ}
    (hd :
      vG.subgroupValueSubgroup N.normSubgroup ≤ integerMultipleSubgroup d) :
    d ∣ (N.residueDegree : ℤ)

theorem

lcm_dvd_residueDegree_of_source_uniformizer_of_normSubgroupValueSubgroup_le

L436 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm.lcm_dvd_residueDegree_of_source_uniformizer_of_normSubgroupValueSubgroup_le

Documentation

Two lower value-step inclusions on the actual valued-norm image force the valued norm residue degree to be divisible by the lcm of those two steps.

Source context 6 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.ValuedNorm
open TameAbhyankar
variable {G H : Type _} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}

Lean source · statement

theorem lcm_dvd_residueDegree_of_source_uniformizer_of_normSubgroupValueSubgroup_le
    (N : ValuedNorm vG vH) {ϖ : H} (hϖ : vH.IsUniformizer ϖ)
    {d e : ℤ}
    (hd :
      vG.subgroupValueSubgroup N.normSubgroup ≤ integerMultipleSubgroup d)
    (he :
      vG.subgroupValueSubgroup N.normSubgroup ≤ integerMultipleSubgroup e) :
    ((d.lcm e : ℕ) : ℤ) ∣ (N.residueDegree : ℤ)

Module documentation

Integer value-group arithmetic

Declarations