Module

PrincipalUnitActions.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.PrincipalUnitActions

27 declarations indexed from sourceView source ↗

Module documentation

Actions on principal-unit quotients

Transports valuation-ring automorphisms to maximal-ideal powers, principal units, and their successive quotients, together with the resulting actions.

Imports1

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.PrincipalUnitQuotients

Imported by2

theorem

integerRingEquiv_mem_maximalIdeal

L24 ↗

LocalFieldTheory.integerRingEquiv_mem_maximalIdeal

Documentation

A ring equivalence of a valuation integer ring preserves the maximal ideal.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerRingEquiv_mem_maximalIdeal
    (K : Type u) [Field K] [ValuativeRel K]
    (e : 𝒪[K] ≃+* 𝒪[K]) (x : 𝒪[K]) :
    e x ∈ (𝓂[K] : Ideal 𝒪[K]) ↔ x ∈ (𝓂[K] : Ideal 𝒪[K])

theorem

integerRingEquiv_map_maximalIdeal

L32 ↗

LocalFieldTheory.integerRingEquiv_map_maximalIdeal

Documentation

A ring equivalence of a valuation integer ring maps the maximal ideal to itself.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerRingEquiv_map_maximalIdeal
    (K : Type u) [Field K] [ValuativeRel K]
    (e : 𝒪[K] ≃+* 𝒪[K]) :
    Ideal.map e.toRingHom (𝓂[K] : Ideal 𝒪[K]) = (𝓂[K] : Ideal 𝒪[K])

theorem

integerRingEquiv_map_maximalIdeal_pow

L50 ↗

LocalFieldTheory.integerRingEquiv_map_maximalIdeal_pow

Documentation

A ring equivalence of a valuation integer ring maps every maximal-ideal power to itself.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerRingEquiv_map_maximalIdeal_pow
    (K : Type u) [Field K] [ValuativeRel K]
    (e : 𝒪[K] ≃+* 𝒪[K]) (n : Nat) :
    Ideal.map e.toRingHom (𝓂[K] ^ n : Ideal 𝒪[K]) =
      (𝓂[K] ^ n : Ideal 𝒪[K])

theorem

integerRingEquiv_mem_maximalIdeal_pow

L58 ↗

LocalFieldTheory.integerRingEquiv_mem_maximalIdeal_pow

Documentation

Membership in every maximal-ideal power is invariant under an integer-ring equivalence.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerRingEquiv_mem_maximalIdeal_pow
    (K : Type u) [Field K] [ValuativeRel K]
    (e : 𝒪[K] ≃+* 𝒪[K]) (n : Nat) (x : 𝒪[K]) :
    e x ∈ (𝓂[K] ^ n : Ideal 𝒪[K]) ↔ x ∈ (𝓂[K] ^ n : Ideal 𝒪[K])

def

maximalIdealPowMapEquivOfIntegerRingEquiv

L76 ↗

LocalFieldTheory.maximalIdealPowMapEquivOfIntegerRingEquiv

Documentation

The induced additive equivalence on the ideal power 𝓂^n.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def maximalIdealPowMapEquivOfIntegerRingEquiv
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K]) :
    ((𝓂[K] ^ n : Ideal 𝒪[K]) : Type u) ≃+
      ((𝓂[K] ^ n : Ideal 𝒪[K]) : Type u) where
  toFun a := ⟨e (a : 𝒪[K]), (integerRingEquiv_mem_maximalIdeal_pow K e n a).2 a.2⟩
  invFun a :=
    ⟨e.symm (a : 𝒪[K]), (integerRingEquiv_mem_maximalIdeal_pow K e.symm n a).2 a.2⟩
  left_inv := by
    intro a
    ext
    simp
  right_inv := by
    intro a
    ext
    simp
  map_add' := by
    intro a b
    ext
    simp

theorem

maximalIdealPowMapEquivOfIntegerRingEquiv_apply

L99 ↗

LocalFieldTheory.maximalIdealPowMapEquivOfIntegerRingEquiv_apply

Documentation

An integer-ring equivalence transports an element of a maximal-ideal power by applying the underlying ring equivalence.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem maximalIdealPowMapEquivOfIntegerRingEquiv_apply
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K])
    (a : ((𝓂[K] ^ n : Ideal 𝒪[K]) : Type u)) :
    (maximalIdealPowMapEquivOfIntegerRingEquiv K n e a : 𝒪[K]) = e (a : 𝒪[K])

theorem

maximalIdealPowSuccQuotMapOfIntegerRingEquiv_respects

L106 ↗

LocalFieldTheory.maximalIdealPowSuccQuotMapOfIntegerRingEquiv_respects

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem maximalIdealPowSuccQuotMapOfIntegerRingEquiv_respects
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K])
    (a b : ((𝓂[K] ^ n : Ideal 𝒪[K]) : Type u))
    (hab : a - b ∈ maximalIdealPowSuccSubmodule K n) :
    maximalIdealPowSuccQuotMk K n
        (maximalIdealPowMapEquivOfIntegerRingEquiv K n e a) =
      maximalIdealPowSuccQuotMk K n
        (maximalIdealPowMapEquivOfIntegerRingEquiv K n e b)

def

maximalIdealPowSuccQuotMapOfIntegerRingEquiv

L125 ↗

LocalFieldTheory.maximalIdealPowSuccQuotMapOfIntegerRingEquiv

Documentation

The induced additive homomorphism on 𝓂^n/𝓂^(n+1).

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def maximalIdealPowSuccQuotMapOfIntegerRingEquiv
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K]) :
    MaximalIdealPowSuccQuot K n →+ MaximalIdealPowSuccQuot K n

theorem

maximalIdealPowSuccQuotMapOfIntegerRingEquiv_mk

L155 ↗

LocalFieldTheory.maximalIdealPowSuccQuotMapOfIntegerRingEquiv_mk

Documentation

The map on successive maximal-ideal quotients sends a representative to the class of its image under the ring equivalence.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem maximalIdealPowSuccQuotMapOfIntegerRingEquiv_mk
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K])
    (a : ((𝓂[K] ^ n : Ideal 𝒪[K]) : Type u)) :
    maximalIdealPowSuccQuotMapOfIntegerRingEquiv K n e
        (maximalIdealPowSuccQuotMk K n a) =
      maximalIdealPowSuccQuotMk K n
        (maximalIdealPowMapEquivOfIntegerRingEquiv K n e a)

def

maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv

L173 ↗

LocalFieldTheory.maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv

Documentation

The induced additive equivalence on 𝓂^n/𝓂^(n+1).

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K]) :
    MaximalIdealPowSuccQuot K n ≃+ MaximalIdealPowSuccQuot K n where
  toFun := maximalIdealPowSuccQuotMapOfIntegerRingEquiv K n e
  invFun := maximalIdealPowSuccQuotMapOfIntegerRingEquiv K n e.symm
  left_inv := by
    intro x
    refine MaximalIdealPowSuccQuot.inductionOn n
      (motive := fun x' =>
        maximalIdealPowSuccQuotMapOfIntegerRingEquiv K n e.symm
            (maximalIdealPowSuccQuotMapOfIntegerRingEquiv K n e x') = x')
      x ?_
    intro a
    rw [maximalIdealPowSuccQuotMapOfIntegerRingEquiv_mk,
      maximalIdealPowSuccQuotMapOfIntegerRingEquiv_mk]
    have h := (maximalIdealPowMapEquivOfIntegerRingEquiv K n e).left_inv a
    exact congrArg (maximalIdealPowSuccQuotMk K n) h
  right_inv := by
    intro x
    refine MaximalIdealPowSuccQuot.inductionOn n
      (motive := fun x' =>
        maximalIdealPowSuccQuotMapOfIntegerRingEquiv K n e
            (maximalIdealPowSuccQuotMapOfIntegerRingEquiv K n e.symm x') = x')
      x ?_
    intro a
    rw [maximalIdealPowSuccQuotMapOfIntegerRingEquiv_mk,
      maximalIdealPowSuccQuotMapOfIntegerRingEquiv_mk]
    have h := (maximalIdealPowMapEquivOfIntegerRingEquiv K n e).right_inv a
    exact congrArg (maximalIdealPowSuccQuotMk K n) h
  map_add' := by
    intro x y
    exact map_add (maximalIdealPowSuccQuotMapOfIntegerRingEquiv K n e) x y

theorem

maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv_mk

L209 ↗

LocalFieldTheory.maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv_mk

Documentation

The equivalence of successive maximal-ideal quotients acts on classes by applying the integer-ring equivalence.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv_mk
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K])
    (a : ((𝓂[K] ^ n : Ideal 𝒪[K]) : Type u)) :
    maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv K n e
        (maximalIdealPowSuccQuotMk K n a) =
      maximalIdealPowSuccQuotMk K n
        (maximalIdealPowMapEquivOfIntegerRingEquiv K n e a)

theorem

principalUnits_integerRingEquiv_mem_self

L220 ↗

LocalFieldTheory.principalUnits_integerRingEquiv_mem_self

Documentation

Principal units are preserved by every valuation-integer-ring equivalence.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnits_integerRingEquiv_mem_self
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K]) (u : 𝒪[K]ˣ)
    (hu : u ∈ principalUnits K n) :
    Units.mapEquiv e.toMulEquiv u ∈ principalUnits K n

def

principalUnitsMapEquivOfIntegerRingEquiv

L229 ↗

LocalFieldTheory.principalUnitsMapEquivOfIntegerRingEquiv

Documentation

The induced multiplicative equivalence on the n-th principal-unit group.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def principalUnitsMapEquivOfIntegerRingEquiv
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K]) :
    principalUnits K n ≃* principalUnits K n where
  toFun u :=
    ⟨Units.mapEquiv e.toMulEquiv u.1,
      principalUnits_integerRingEquiv_mem_self K n e u.1 u.2⟩
  invFun u :=
    ⟨Units.mapEquiv e.symm.toMulEquiv u.1,
      principalUnits_integerRingEquiv_mem_self K n e.symm u.1 u.2⟩
  left_inv := by
    intro u
    ext
    simp
  right_inv := by
    intro u
    ext
    simp
  map_mul' := by
    intro a b
    ext
    simp

theorem

principalUnitsMapEquivOfIntegerRingEquiv_apply

L254 ↗

LocalFieldTheory.principalUnitsMapEquivOfIntegerRingEquiv_apply

Documentation

An integer-ring equivalence transports principal units by applying it to their underlying units. An integer-ring equivalence transports principal units by applying it to their underlying units.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsMapEquivOfIntegerRingEquiv_apply
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K]) (u : principalUnits K n) :
    principalUnitsMapEquivOfIntegerRingEquiv K n e u =
      ⟨Units.mapEquiv e.toMulEquiv u.1,
        principalUnits_integerRingEquiv_mem_self K n e u.1 u.2⟩

theorem

principalUnitsMapEquivOfIntegerRingEquiv_oneAdd

L264 ↗

LocalFieldTheory.principalUnitsMapEquivOfIntegerRingEquiv_oneAdd

Documentation

Transport of a principal unit of the form 1 + x is the principal unit formed from the transported x.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsMapEquivOfIntegerRingEquiv_oneAdd
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (hn : 1 ≤ n) (e : 𝒪[K] ≃+* 𝒪[K])
    (a : (𝓂[K] ^ n : Ideal 𝒪[K])) :
    principalUnitsMapEquivOfIntegerRingEquiv K n e
        (principalUnitOneAddOfMemPowSubgroup K hn (a : 𝒪[K]) a.2) =
      principalUnitOneAddOfMemPowSubgroup K hn
        (e (a : 𝒪[K])) ((integerRingEquiv_mem_maximalIdeal_pow K e n a).2 a.2)

def

principalUnitsSuccQuotMapOfIntegerRingEquiv

L277 ↗

LocalFieldTheory.principalUnitsSuccQuotMapOfIntegerRingEquiv

Documentation

The induced homomorphism on the successive principal-unit quotient.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def principalUnitsSuccQuotMapOfIntegerRingEquiv
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K]) :
    PrincipalUnitsSuccQuot K n →* PrincipalUnitsSuccQuot K n

theorem

principalUnitsSuccQuotMapOfIntegerRingEquiv_apply

L292 ↗

LocalFieldTheory.principalUnitsSuccQuotMapOfIntegerRingEquiv_apply

Documentation

The map on successive principal-unit quotients sends each class to the class of its transported representative.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotMapOfIntegerRingEquiv_apply
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K]) (u : principalUnits K n) :
    principalUnitsSuccQuotMapOfIntegerRingEquiv K n e
        (principalUnitsSuccQuotMk K n u) =
      principalUnitsSuccQuotMk K n
        (principalUnitsMapEquivOfIntegerRingEquiv K n e u)

def

principalUnitsSuccQuotMapEquivOfIntegerRingEquiv

L302 ↗

LocalFieldTheory.principalUnitsSuccQuotMapEquivOfIntegerRingEquiv

Documentation

The induced multiplicative equivalence on U^n/U^(n+1).

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def principalUnitsSuccQuotMapEquivOfIntegerRingEquiv
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K]) :
    PrincipalUnitsSuccQuot K n ≃* PrincipalUnitsSuccQuot K n where
  toFun := principalUnitsSuccQuotMapOfIntegerRingEquiv K n e
  invFun := principalUnitsSuccQuotMapOfIntegerRingEquiv K n e.symm
  left_inv := by
    intro x
    refine PrincipalUnitsSuccQuot.inductionOn n
      (motive := fun x' =>
        principalUnitsSuccQuotMapOfIntegerRingEquiv K n e.symm
            (principalUnitsSuccQuotMapOfIntegerRingEquiv K n e x') = x')
      x ?_
    intro u
    rw [principalUnitsSuccQuotMapOfIntegerRingEquiv_apply,
      principalUnitsSuccQuotMapOfIntegerRingEquiv_apply]
    have h := (principalUnitsMapEquivOfIntegerRingEquiv K n e).left_inv u
    exact congrArg
      (fun z : principalUnits K n =>
        principalUnitsSuccQuotMk K n z) h
  right_inv := by
    intro x
    refine PrincipalUnitsSuccQuot.inductionOn n
      (motive := fun x' =>
        principalUnitsSuccQuotMapOfIntegerRingEquiv K n e
            (principalUnitsSuccQuotMapOfIntegerRingEquiv K n e.symm x') = x')
      x ?_
    intro u
    rw [principalUnitsSuccQuotMapOfIntegerRingEquiv_apply,
      principalUnitsSuccQuotMapOfIntegerRingEquiv_apply]
    have h := (principalUnitsMapEquivOfIntegerRingEquiv K n e).right_inv u
    exact congrArg
      (fun z : principalUnits K n =>
        principalUnitsSuccQuotMk K n z) h
  map_mul' := by
    intro x y
    exact map_mul (principalUnitsSuccQuotMapOfIntegerRingEquiv K n e) x y

theorem

principalUnitsSuccQuotMapEquivOfIntegerRingEquiv_apply

L342 ↗

LocalFieldTheory.principalUnitsSuccQuotMapEquivOfIntegerRingEquiv_apply

Documentation

The equivalence of successive principal-unit quotients is induced by transport along the integer-ring equivalence.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotMapEquivOfIntegerRingEquiv_apply
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K]) (u : principalUnits K n) :
    principalUnitsSuccQuotMapEquivOfIntegerRingEquiv K n e
        (principalUnitsSuccQuotMk K n u) =
      principalUnitsSuccQuotMk K n
        (principalUnitsMapEquivOfIntegerRingEquiv K n e u)

def

principalUnitsSuccQuotAddEquivOfIntegerRingEquiv

L353 ↗

LocalFieldTheory.principalUnitsSuccQuotAddEquivOfIntegerRingEquiv

Documentation

The induced additive equivalence on the additive form of U^n/U^(n+1).

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def principalUnitsSuccQuotAddEquivOfIntegerRingEquiv
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K]) :
    Additive (PrincipalUnitsSuccQuot K n) ≃+
      Additive (PrincipalUnitsSuccQuot K n) where
  toFun x :=
    Additive.ofMul
      (principalUnitsSuccQuotMapEquivOfIntegerRingEquiv K n e (Additive.toMul x))
  invFun x :=
    Additive.ofMul
      (principalUnitsSuccQuotMapEquivOfIntegerRingEquiv K n e.symm (Additive.toMul x))
  left_inv := by
    intro x
    change Additive.ofMul
        (principalUnitsSuccQuotMapEquivOfIntegerRingEquiv K n e.symm
          (principalUnitsSuccQuotMapEquivOfIntegerRingEquiv K n e (Additive.toMul x))) =
      Additive.ofMul (Additive.toMul x)
    exact congrArg Additive.ofMul
      ((principalUnitsSuccQuotMapEquivOfIntegerRingEquiv K n e).left_inv
        (Additive.toMul x))
  right_inv := by
    intro x
    change Additive.ofMul
        (principalUnitsSuccQuotMapEquivOfIntegerRingEquiv K n e
          (principalUnitsSuccQuotMapEquivOfIntegerRingEquiv K n e.symm
            (Additive.toMul x))) =
      Additive.ofMul (Additive.toMul x)
    exact congrArg Additive.ofMul
      ((principalUnitsSuccQuotMapEquivOfIntegerRingEquiv K n e).right_inv
        (Additive.toMul x))
  map_add' := by
    intro x y
    change Additive.ofMul
        (principalUnitsSuccQuotMapEquivOfIntegerRingEquiv K n e
          (Additive.toMul (x + y))) =
      Additive.ofMul
        (principalUnitsSuccQuotMapEquivOfIntegerRingEquiv K n e (Additive.toMul x) *
          principalUnitsSuccQuotMapEquivOfIntegerRingEquiv K n e (Additive.toMul y))
    rw [show Additive.toMul (x + y) = Additive.toMul x * Additive.toMul y from rfl]
    rw [map_mul]

theorem

principalUnitsSuccQuotAddEquivOfIntegerRingEquiv_apply

L397 ↗

LocalFieldTheory.principalUnitsSuccQuotAddEquivOfIntegerRingEquiv_apply

Documentation

The additive equivalence on successive principal-unit quotients agrees with transport of quotient representatives.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotAddEquivOfIntegerRingEquiv_apply
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K]) (x : PrincipalUnitsSuccQuot K n) :
    principalUnitsSuccQuotAddEquivOfIntegerRingEquiv K n e (Additive.ofMul x) =
      Additive.ofMul (principalUnitsSuccQuotMapEquivOfIntegerRingEquiv K n e x)

def

maximalIdealPowSuccQuotMultiplicativeMapEquivOfIntegerRingEquiv

L406 ↗

LocalFieldTheory.maximalIdealPowSuccQuotMultiplicativeMapEquivOfIntegerRingEquiv

Documentation

Multiplicative form of the induced equivalence on 𝓂^n/𝓂^(n+1).

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def maximalIdealPowSuccQuotMultiplicativeMapEquivOfIntegerRingEquiv
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K]) :
    Multiplicative (MaximalIdealPowSuccQuot K n) ≃*
      Multiplicative (MaximalIdealPowSuccQuot K n) where
  toFun x :=
    Multiplicative.ofAdd
      (maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv K n e
        (Multiplicative.toAdd x))
  invFun x :=
    Multiplicative.ofAdd
      (maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv K n e.symm
        (Multiplicative.toAdd x))
  left_inv := by
    intro x
    change Multiplicative.ofAdd
        (maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv K n e.symm
          (maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv K n e
            (Multiplicative.toAdd x))) =
      Multiplicative.ofAdd (Multiplicative.toAdd x)
    exact congrArg Multiplicative.ofAdd
      ((maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv K n e).left_inv
        (Multiplicative.toAdd x))
  right_inv := by
    intro x
    change Multiplicative.ofAdd
        (maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv K n e
          (maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv K n e.symm
            (Multiplicative.toAdd x))) =
      Multiplicative.ofAdd (Multiplicative.toAdd x)
    exact congrArg Multiplicative.ofAdd
      ((maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv K n e).right_inv
        (Multiplicative.toAdd x))
  map_mul' := by
    intro x y
    change Multiplicative.ofAdd
        (maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv K n e
          (Multiplicative.toAdd (x * y))) =
      Multiplicative.ofAdd
        (maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv K n e
          (Multiplicative.toAdd x) +
        maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv K n e
          (Multiplicative.toAdd y))
    rw [show Multiplicative.toAdd (x * y) =
        Multiplicative.toAdd x + Multiplicative.toAdd y from rfl]
    rw [map_add]

theorem

maximalIdealPowSuccQuotMultiplicativeMapEquivOfIntegerRingEquiv_apply

L456 ↗

LocalFieldTheory.maximalIdealPowSuccQuotMultiplicativeMapEquivOfIntegerRingEquiv_apply

Documentation

The multiplicative encoding of a successive ideal-quotient equivalence applies the original additive transport map.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem maximalIdealPowSuccQuotMultiplicativeMapEquivOfIntegerRingEquiv_apply
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K]) (x : MaximalIdealPowSuccQuot K n) :
    maximalIdealPowSuccQuotMultiplicativeMapEquivOfIntegerRingEquiv K n e
        (Multiplicative.ofAdd x) =
      Multiplicative.ofAdd (maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv K n e x)

theorem

principalUnitsSuccQuotOfMaximalIdealPowSuccQuot_integerRingEquiv

L466 ↗

LocalFieldTheory.principalUnitsSuccQuotOfMaximalIdealPowSuccQuot_integerRingEquiv

Documentation

The map 𝓂^n/𝓂^(n+1) → U^n/U^(n+1) induced by a ↦ 1+a is equivariant for every valuation-integer-ring automorphism.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotOfMaximalIdealPowSuccQuot_integerRingEquiv
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (hn : 1 ≤ n) (e : 𝒪[K] ≃+* 𝒪[K])
    (x : MaximalIdealPowSuccQuot K n) :
    principalUnitsSuccQuotMapEquivOfIntegerRingEquiv K n e
        (principalUnitsSuccQuotOfMaximalIdealPowSuccQuot K n hn x) =
      principalUnitsSuccQuotOfMaximalIdealPowSuccQuot K n hn
        (maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv K n e x)

theorem

principalUnitsSuccQuotOfMaximalIdealPowSuccQuotAdd_integerRingEquiv

L493 ↗

LocalFieldTheory.principalUnitsSuccQuotOfMaximalIdealPowSuccQuotAdd_integerRingEquiv

Documentation

Additive form of equivariance of a ↦ 1+a on successive quotients.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotOfMaximalIdealPowSuccQuotAdd_integerRingEquiv
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (hn : 1 ≤ n) (e : 𝒪[K] ≃+* 𝒪[K])
    (x : MaximalIdealPowSuccQuot K n) :
    Additive.ofMul
        (principalUnitsSuccQuotMapEquivOfIntegerRingEquiv K n e
          (principalUnitsSuccQuotOfMaximalIdealPowSuccQuot K n hn x)) =
    principalUnitsSuccQuotOfMaximalIdealPowSuccQuotAdd K n hn
        (maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv K n e x)

theorem

maximalIdealPowSuccQuotAddEquivPrincipalUnitsSuccQuot_integerRingEquiv

L507 ↗

LocalFieldTheory.maximalIdealPowSuccQuotAddEquivPrincipalUnitsSuccQuot_integerRingEquiv

Documentation

The additive isomorphism 𝓂^n/𝓂^(n+1) ≃ U^n/U^(n+1) is equivariant for every valuation-integer-ring automorphism.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem maximalIdealPowSuccQuotAddEquivPrincipalUnitsSuccQuot_integerRingEquiv
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (hn : 1 ≤ n) (e : 𝒪[K] ≃+* 𝒪[K])
    (x : MaximalIdealPowSuccQuot K n) :
    principalUnitsSuccQuotAddEquivOfIntegerRingEquiv K n e
        (maximalIdealPowSuccQuotAddEquivPrincipalUnitsSuccQuot K n hn x) =
      maximalIdealPowSuccQuotAddEquivPrincipalUnitsSuccQuot K n hn
        (maximalIdealPowSuccQuotMapEquivOfIntegerRingEquiv K n e x)

theorem

maximalIdealPowSuccQuotMulEquivPrincipalUnitsSuccQuot_integerRingEquiv

L524 ↗

LocalFieldTheory.maximalIdealPowSuccQuotMulEquivPrincipalUnitsSuccQuot_integerRingEquiv

Documentation

Multiplicative equivariance of the associated-graded comparison Multiplicative (𝓂^n/𝓂^(n+1)) ≃* U^n/U^(n+1) for every valuation-integer-ring automorphism.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem maximalIdealPowSuccQuotMulEquivPrincipalUnitsSuccQuot_integerRingEquiv
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (hn : 1 ≤ n) (e : 𝒪[K] ≃+* 𝒪[K])
    (x : Multiplicative (MaximalIdealPowSuccQuot K n)) :
    principalUnitsSuccQuotMapEquivOfIntegerRingEquiv K n e
        (maximalIdealPowSuccQuotMulEquivPrincipalUnitsSuccQuot K n hn x) =
      maximalIdealPowSuccQuotMulEquivPrincipalUnitsSuccQuot K n hn
        (maximalIdealPowSuccQuotMultiplicativeMapEquivOfIntegerRingEquiv K n e x)

Module documentation

Actions on principal-unit quotients

Declarations