NYLL
Module

Common.lean

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

Module documentation

Common norm images and value steps

This file generates the two lower value-step inclusions used by the transport layer from concrete ValuedNorm.normSubgroup containments.

Imports1
Imported by2

Declarations

theorem

subgroupValueSubgroup_le_residueDegreeMultiple_of_le_normSubgroup

L32 ↗
TameAbhyankar.ValuedNorm.subgroupValueSubgroup_le_residueDegreeMultiple_of_le_normSubgroup
Documentation

If a subgroup of the target group lies in the norm subgroup of a ValuedNorm, then every value attained on that subgroup is divisible by the valued norm residue degree.

Source context 8 commands

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

noncomputable section
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
namespace ValuedNorm
variable {G H H' : Type _} [Group G] [Group H] [Group H']
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable {vH' : MultiplicativeIntegerValuation H'}
Lean source · statement
theorem subgroupValueSubgroup_le_residueDegreeMultiple_of_le_normSubgroup
    (N : ValuedNorm vG vH) {T : Subgroup G}
    (hT : T ≤ N.normSubgroup) :
    vG.subgroupValueSubgroup T ≤
      integerMultipleSubgroup (N.residueDegree : ℤ)
theorem

lcm_dvd_of_exists_mem_val_of_common_le_normSubgroups

L45 ↗
TameAbhyankar.ValuedNorm.lcm_dvd_of_exists_mem_val_of_common_le_normSubgroups
Documentation

Common-norm-image form of the lcm step: a larger common image subgroup contained in two norm subgroups supplies the two lower value-step inclusions, and any actual value generated by a smaller ramification image subgroup is therefore divisible by the lcm of the two valued norm residue degrees.

Source context 8 commands

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

noncomputable section
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
namespace ValuedNorm
variable {G H H' : Type _} [Group G] [Group H] [Group H']
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable {vH' : MultiplicativeIntegerValuation H'}
Lean source · statement
theorem lcm_dvd_of_exists_mem_val_of_common_le_normSubgroups
    (N : ValuedNorm vG vH) (N' : ValuedNorm vG vH')
    {S T : Subgroup G} {n : ℤ}
    (hn : ∃ x : G, x ∈ S ∧ vG.val x = n)
    (hST : S ≤ T)
    (hT : T ≤ N.normSubgroup)
    (hT' : T ≤ N'.normSubgroup) :
    ((((N.residueDegree : ℤ).lcm (N'.residueDegree : ℤ) : ℕ) : ℤ) ∣ n)

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