NYLL
Module

MixedCharCharacterLogRepresentation.lean

Nyll.Yamaguchi26AbfaithfulGalois.Analytic.MixedCharCharacterLogRepresentation
11 declarations indexed from sourceView source ↗

Module documentation

The character subspace of the actual principal-unit logarithm image

The range carries its inherited p-adic module structure. Twisting its actual representation and taking subgroup invariants constructs the character subspace. Normality supplies stability under the full group action; it is not needed for the field inclusion, eigenvector criterion, or saturation. No p-adic module structure is registered on the ambient field.

Imports5
Imported by3

Declarations

abbrev

PrincipalUnitLogImageOfMixedChar

L35 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.PrincipalUnitLogImageOfMixedChar
Documentation

The actual logarithm image, with the module structure inherited from its range.

Source context 5 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u w
variable {K : Type u} [Field K] [CharZero K]
variable (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
  [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
  (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
Lean source · statement
abbrev PrincipalUnitLogImageOfMixedChar : Type u
def

principalUnitLogImageRepresentationOfMixedChar

L48 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogImageRepresentationOfMixedChar
Documentation

Logarithm equivariance supplies the action on its actual range.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u w
variable {K : Type u} [Field K] [CharZero K]
variable (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
  [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
  (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
section ImageAction
variable {Γ : Type w} [Monoid Γ]
  (σ : Γ →* (K ≃+* K)) (hval : ∀ (g : Γ) (x : K), v (σ g x) = v x)
Lean source · statement
def principalUnitLogImageRepresentationOfMixedChar :
    Representation ℤ_[p] Γ (PrincipalUnitLogImageOfMixedChar v p)
def

characterLogSubmoduleOfMixedChar

L70 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.characterLogSubmoduleOfMixedChar
Documentation

The actual character submodule of the logarithm image.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u w
variable {K : Type u} [Field K] [CharZero K]
variable (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
  [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
  (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
section CharacterSpace
variable {Γ : Type w} [Group Γ]
  (σ : Γ →* (K ≃+* K)) (hval : ∀ (g : Γ) (x : K), v (σ g x) = v x)
  (χ : Γ →* ℤ_[p]ˣ) (Δ : Subgroup Γ)
Lean source · statement
def characterLogSubmoduleOfMixedChar :
    Submodule ℤ_[p] (PrincipalUnitLogImageOfMixedChar v p)
abbrev

CharacterLogSpaceOfMixedChar

L76 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.CharacterLogSpaceOfMixedChar
Documentation

The character log space uses the existing submodule carrier and its module.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u w
variable {K : Type u} [Field K] [CharZero K]
variable (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
  [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
  (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
section CharacterSpace
variable {Γ : Type w} [Group Γ]
  (σ : Γ →* (K ≃+* K)) (hval : ∀ (g : Γ) (x : K), v (σ g x) = v x)
  (χ : Γ →* ℤ_[p]ˣ) (Δ : Subgroup Γ)
Lean source · statement
abbrev CharacterLogSpaceOfMixedChar : Type u
def

characterLogInclusionOfMixedChar

L80 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.characterLogInclusionOfMixedChar
Documentation

The original field value of a vector in the character log space.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u w
variable {K : Type u} [Field K] [CharZero K]
variable (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
  [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
  (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
section CharacterSpace
variable {Γ : Type w} [Group Γ]
  (σ : Γ →* (K ≃+* K)) (hval : ∀ (g : Γ) (x : K), v (σ g x) = v x)
  (χ : Γ →* ℤ_[p]ˣ) (Δ : Subgroup Γ)
Lean source · full declaration
def characterLogInclusionOfMixedChar :
    CharacterLogSpaceOfMixedChar v p σ hval χ Δ →+ K where
  toFun x := ((x : PrincipalUnitLogImageOfMixedChar v p) : K)
  map_zero' := rfl
  map_add' _ _ := rfl
theorem

characterLogInclusionOfMixedChar_injective

L87 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.characterLogInclusionOfMixedChar_injective
Documentation

Passing to the original field loses no information.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u w
variable {K : Type u} [Field K] [CharZero K]
variable (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
  [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
  (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
section CharacterSpace
variable {Γ : Type w} [Group Γ]
  (σ : Γ →* (K ≃+* K)) (hval : ∀ (g : Γ) (x : K), v (σ g x) = v x)
  (χ : Γ →* ℤ_[p]ˣ) (Δ : Subgroup Γ)
Lean source · statement
theorem characterLogInclusionOfMixedChar_injective :
    Function.Injective (characterLogInclusionOfMixedChar v p σ hval χ Δ)
theorem

exists_principalUnit_log_eq_characterLogInclusion

L93 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_principalUnit_log_eq_characterLogInclusion
Documentation

Every character log vector retains a preimage under the original logarithm.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u w
variable {K : Type u} [Field K] [CharZero K]
variable (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
  [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
  (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
section CharacterSpace
variable {Γ : Type w} [Group Γ]
  (σ : Γ →* (K ≃+* K)) (hval : ∀ (g : Γ) (x : K), v (σ g x) = v x)
  (χ : Γ →* ℤ_[p]ˣ) (Δ : Subgroup Γ)
Lean source · statement
theorem exists_principalUnit_log_eq_characterLogInclusion
    (x : CharacterLogSpaceOfMixedChar v p σ hval χ Δ) :
    ∃ a : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1,
      (principalUnitLogOfMixedChar v p a).toAdd =
        characterLogInclusionOfMixedChar v p σ hval χ Δ x
theorem

mem_characterLogSubmoduleOfMixedChar_iff

L102 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.mem_characterLogSubmoduleOfMixedChar_iff
Documentation

Membership is the actual character eigenvector equation in the field.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u w
variable {K : Type u} [Field K] [CharZero K]
variable (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
  [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
  (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
section CharacterSpace
variable {Γ : Type w} [Group Γ]
  (σ : Γ →* (K ≃+* K)) (hval : ∀ (g : Γ) (x : K), v (σ g x) = v x)
  (χ : Γ →* ℤ_[p]ˣ) (Δ : Subgroup Γ)
Lean source · statement
theorem mem_characterLogSubmoduleOfMixedChar_iff
    (x : PrincipalUnitLogImageOfMixedChar v p) :
    x ∈ characterLogSubmoduleOfMixedChar v p σ hval χ Δ ↔
      ∀ δ : Δ, σ (δ : Γ) (x : K) =
        padicIntToFieldOfMixedChar v p (χ (δ : Γ) : ℤ_[p]) * (x : K)
theorem

mem_characterLogSubmoduleOfMixedChar_of_nsmul_mem

L118 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.mem_characterLogSubmoduleOfMixedChar_of_nsmul_mem
Documentation

The character condition is saturated inside the actual log image for nonzero natural multiples. Characteristic zero is inherited from the original field.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u w
variable {K : Type u} [Field K] [CharZero K]
variable (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
  [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
  (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
section CharacterSpace
variable {Γ : Type w} [Group Γ]
  (σ : Γ →* (K ≃+* K)) (hval : ∀ (g : Γ) (x : K), v (σ g x) = v x)
  (χ : Γ →* ℤ_[p]ˣ) (Δ : Subgroup Γ)
Lean source · statement
theorem mem_characterLogSubmoduleOfMixedChar_of_nsmul_mem
    (n : ℕ) (hn : n ≠ 0) (x : PrincipalUnitLogImageOfMixedChar v p)
    (hx : n • x ∈ characterLogSubmoduleOfMixedChar v p σ hval χ Δ) :
    x ∈ characterLogSubmoduleOfMixedChar v p σ hval χ Δ
def

characterLogRepresentationOfMixedChar

L133 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.characterLogRepresentationOfMixedChar
Documentation

Normality constructs the full group action on the character log space.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u w
variable {K : Type u} [Field K] [CharZero K]
variable (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
  [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
  (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
section CharacterSpace
variable {Γ : Type w} [Group Γ]
  (σ : Γ →* (K ≃+* K)) (hval : ∀ (g : Γ) (x : K), v (σ g x) = v x)
  (χ : Γ →* ℤ_[p]ˣ) (Δ : Subgroup Γ)
variable [Δ.Normal]
Lean source · statement
def characterLogRepresentationOfMixedChar :
    Representation ℤ_[p] Γ (CharacterLogSpaceOfMixedChar v p σ hval χ Δ)
theorem

characterLogInclusionOfMixedChar_action

L139 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.characterLogInclusionOfMixedChar_action
Documentation

The constructed action is exactly the inverse-character-twisted field action.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u w
variable {K : Type u} [Field K] [CharZero K]
variable (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
  [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
  (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
section CharacterSpace
variable {Γ : Type w} [Group Γ]
  (σ : Γ →* (K ≃+* K)) (hval : ∀ (g : Γ) (x : K), v (σ g x) = v x)
  (χ : Γ →* ℤ_[p]ˣ) (Δ : Subgroup Γ)
variable [Δ.Normal]
Lean source · statement
theorem characterLogInclusionOfMixedChar_action
    (g : Γ) (x : CharacterLogSpaceOfMixedChar v p σ hval χ Δ) :
    characterLogInclusionOfMixedChar v p σ hval χ Δ
        (characterLogRepresentationOfMixedChar v p σ hval χ Δ g x) =
      padicIntToFieldOfMixedChar v p (((χ g)⁻¹ : ℤ_[p]ˣ) : ℤ_[p]) *
        σ g (characterLogInclusionOfMixedChar v p σ hval χ Δ x)

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