NYLL
Module

Transport.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.Transport
2 declarations indexed from sourceView source ↗

Module documentation

Transport for subgroup value images

The common-top value-group comparison needs one transport step: the actual ramification image is a subgroup of a larger common image, while the two lower value-step inclusions are naturally proved for that larger common image.

Imports1
Imported by2

Declarations

theorem

subgroupValueSubgroup_le_integerMultipleSubgroup_lcm_of_le

L29 ↗
TameAbhyankar.MultiplicativeIntegerValuation.subgroupValueSubgroup_le_integerMultipleSubgroup_lcm_of_le
Documentation

Lower value-step inclusions for a larger common image restrict to a smaller ramification image and combine into the lcm value-step inclusion.

Source context 5 commands

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

noncomputable section
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type _} [Group G]
Lean source · statement
theorem subgroupValueSubgroup_le_integerMultipleSubgroup_lcm_of_le
    (V : MultiplicativeIntegerValuation G) {S T : Subgroup G} {d e : ℤ}
    (hST : S ≤ T)
    (hd : V.subgroupValueSubgroup T ≤ integerMultipleSubgroup d)
    (he : V.subgroupValueSubgroup T ≤ integerMultipleSubgroup e) :
    V.subgroupValueSubgroup S ≤
      integerMultipleSubgroup ((d.lcm e : ℕ) : ℤ)
theorem

int_lcm_dvd_of_exists_mem_val_of_le_of_subgroupValueSubgroup_le

L44 ↗
TameAbhyankar.MultiplicativeIntegerValuation.int_lcm_dvd_of_exists_mem_val_of_le_of_subgroupValueSubgroup_le
Documentation

Concrete transport form: if an actual element of the smaller ramification image has valuation n, and the larger common image satisfies the two lower value-step inclusions, then n is divisible by the lcm of the two lower steps.

Source context 5 commands

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

noncomputable section
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type _} [Group G]
Lean source · statement
theorem int_lcm_dvd_of_exists_mem_val_of_le_of_subgroupValueSubgroup_le
    (V : MultiplicativeIntegerValuation G) {S T : Subgroup G} {n d e : ℤ}
    (hn : ∃ x : G, x ∈ S ∧ V.val x = n)
    (hST : S ≤ T)
    (hd : V.subgroupValueSubgroup T ≤ integerMultipleSubgroup d)
    (he : V.subgroupValueSubgroup T ≤ integerMultipleSubgroup e) :
    ((d.lcm e : ℕ) : ℤ) ∣ n

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.