NYLL
Module

NormDownLcm.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.NonarchimedeanLocalField.Galois.NormDownLcm
4 declarations indexed from sourceView source ↗

Module documentation

Galois norm-down lcm value-step inclusions

This file keeps the Galois residue-degree lcm subgroup comparisons for the norm-down ramification image separate from the construction of that image.

Imports1
Imported by1

Declarations

theorem

normPoweredBaseUnitsImageSubgroup_valueImage_le_galoisResidueDegree_lcm

L51 ↗
TameAbhyankar.NAField.normPoweredBaseUnitsImageSubgroup_valueImage_le_galoisResidueDegree_lcm
Documentation

The concrete normed powered ramification image inherits the common-top Galois residue-degree lcm value-step inclusion.

Source context 24 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section GaloisNormPoweredLcm
variable {K L L' M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field L'] [ValuativeRel L'] [TopologicalSpace L']
variable [IsNonarchimedeanLocalField L']
variable [Field M]
variable [Algebra K L] [Algebra K L']
variable [Algebra K M]
variable [Algebra L M] [Algebra L' M]
variable [IsScalarTower K L M] [IsScalarTower K L' M]
variable [Module.Free L M] [Module.Free L' M]
variable [FiniteDimensional K L] [IsGalois K L]
variable [FiniteDimensional K L'] [IsGalois K L']
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
Lean source · statement
theorem normPoweredBaseUnitsImageSubgroup_valueImage_le_galoisResidueDegree_lcm :
    (multiplicativeIntegerValuation K).subgroupValueSubgroup
        (normPoweredBaseUnitsImageSubgroup (K := K) (L := L) (M := M)) ≤
      integerMultipleSubgroup
        ((((Module.finrank 𝓀[K] 𝓀[L] : ℤ).lcm
          (Module.finrank 𝓀[K] 𝓀[L'] : ℤ) : ℕ) : ℤ))
theorem

normPoweredBaseUnitsImageSubgroup_valueImage_le_galoisResidueDegree_lcm_symm

L65 ↗
TameAbhyankar.NAField.normPoweredBaseUnitsImageSubgroup_valueImage_le_galoisResidueDegree_lcm_symm
Documentation

Symmetric branch version of the concrete normed powered ramification-image Galois residue-degree lcm value-step inclusion.

Source context 24 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section GaloisNormPoweredLcm
variable {K L L' M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field L'] [ValuativeRel L'] [TopologicalSpace L']
variable [IsNonarchimedeanLocalField L']
variable [Field M]
variable [Algebra K L] [Algebra K L']
variable [Algebra K M]
variable [Algebra L M] [Algebra L' M]
variable [IsScalarTower K L M] [IsScalarTower K L' M]
variable [Module.Free L M] [Module.Free L' M]
variable [FiniteDimensional K L] [IsGalois K L]
variable [FiniteDimensional K L'] [IsGalois K L']
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
Lean source · statement
theorem normPoweredBaseUnitsImageSubgroup_valueImage_le_galoisResidueDegree_lcm_symm :
    (multiplicativeIntegerValuation K).subgroupValueSubgroup
        (normPoweredBaseUnitsImageSubgroup (K := K) (L := L') (M := M)) ≤
      integerMultipleSubgroup
        ((((Module.finrank 𝓀[K] 𝓀[L'] : ℤ).lcm
          (Module.finrank 𝓀[K] 𝓀[L] : ℤ) : ℕ) : ℤ))
theorem

integerMultipleSubgroup_galoisNormDownRamificationStep_le_lcm

L101 ↗
TameAbhyankar.NAField.integerMultipleSubgroup_galoisNormDownRamificationStep_le_lcm
Documentation

Subgroup-value form of the lcm divisor carried by the Galois norm-down ramification step.

Source context 24 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section GaloisNormDownLcmSubgroup
variable {K L L' M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field L'] [ValuativeRel L'] [TopologicalSpace L']
variable [IsNonarchimedeanLocalField L']
variable [Field M]
variable [Algebra K L] [Algebra K L']
variable [Algebra K M]
variable [Algebra L M] [Algebra L' M]
variable [IsScalarTower K L M] [IsScalarTower K L' M]
variable [Module.Free L M] [Module.Free L' M]
variable [FiniteDimensional K L] [IsGalois K L]
variable [FiniteDimensional K L'] [IsGalois K L']
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
Lean source · statement
theorem integerMultipleSubgroup_galoisNormDownRamificationStep_le_lcm :
    integerMultipleSubgroup
        (galoisNormDownRamificationStepNat (K := K) (L := L) (M := M) :
          ℤ) ≤
      integerMultipleSubgroup
        ((((Module.finrank 𝓀[K] 𝓀[L] : ℤ).lcm
          (Module.finrank 𝓀[K] 𝓀[L'] : ℤ) : ℕ) : ℤ))
theorem

integerMultipleSubgroup_galoisNormDownRamificationStep_le_lcm_symm

L140 ↗
TameAbhyankar.NAField.integerMultipleSubgroup_galoisNormDownRamificationStep_le_lcm_symm
Documentation

Symmetric subgroup-value form of the lcm divisor carried by the Galois norm-down ramification step.

Source context 24 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section GaloisNormDownLcmSubgroupSymm
variable {K L L' M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field L'] [ValuativeRel L'] [TopologicalSpace L']
variable [IsNonarchimedeanLocalField L']
variable [Field M]
variable [Algebra K L] [Algebra K L']
variable [Algebra K M]
variable [Algebra L M] [Algebra L' M]
variable [IsScalarTower K L M] [IsScalarTower K L' M]
variable [Module.Free L M] [Module.Free L' M]
variable [FiniteDimensional K L] [IsGalois K L]
variable [FiniteDimensional K L'] [IsGalois K L']
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
Lean source · statement
theorem integerMultipleSubgroup_galoisNormDownRamificationStep_le_lcm_symm :
    integerMultipleSubgroup
        (galoisNormDownRamificationStepNat (K := K) (L := L') (M := M) :
          ℤ) ≤
      integerMultipleSubgroup
        ((((Module.finrank 𝓀[K] 𝓀[L'] : ℤ).lcm
          (Module.finrank 𝓀[K] 𝓀[L] : ℤ) : ℕ) : ℤ))

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