Module

QuotientTransition.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnitPadicAction.QuotientTransition

3 declarations indexed from sourceView source ↗

Module documentation

Transitions between principal-unit quotients

These additive maps use the concrete principal-unit filtration of a complete discrete valuation field. Neither finiteness nor a scalar action is required.

Imports2

Imported by3

def

principalUnitQuotientCarrierTransitionAdd

L31 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitQuotientCarrierTransitionAdd

Documentation

Additive form of a transition between principal-unit quotients.

Source context 6 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField
open Internal
universe u v
variable {K : Type u} [Field K]

Lean source · full declaration

def Internal.principalUnitQuotientCarrierTransitionAdd
    (F : CompleteDVF.{u, v} K) {m n : ℕ} (hmn : m ≤ n) :
    Additive (Internal.principalUnitQuotientCarrier F n) →+
      Additive (Internal.principalUnitQuotientCarrier F m) where
  toFun x := Additive.ofMul
    (principalUnitQuotientCarrierTransition F hmn (Additive.toMul x))
  map_zero' := by
    change Additive.ofMul
        (principalUnitQuotientCarrierTransition F hmn 1) = Additive.ofMul 1
    rw [map_one]
  map_add' x y := by
    change Additive.ofMul
        (principalUnitQuotientCarrierTransition F hmn
          (Additive.toMul x * Additive.toMul y)) =
      Additive.ofMul
        (principalUnitQuotientCarrierTransition F hmn (Additive.toMul x) *
          principalUnitQuotientCarrierTransition F hmn (Additive.toMul y))
    rw [map_mul]

def

transition

L53 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient.transition

Documentation

Reduction between two wrapped discrete quotient coordinates.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField
open Internal
universe u v
variable {K : Type u} [Field K]
namespace DiscretePrincipalUnitQuotient

Lean source · full declaration

def transition (F : CompleteDVF.{u, v} K) {m n : ℕ} (hmn : m ≤ n) :
    DiscretePrincipalUnitQuotient F n →+
      DiscretePrincipalUnitQuotient F m where
  toFun x := of F m
    (Internal.principalUnitQuotientCarrierTransitionAdd F hmn x.val)
  map_zero' := by
    apply (addEquiv F m).injective
    change Internal.principalUnitQuotientCarrierTransitionAdd F hmn 0 = 0
    exact (Internal.principalUnitQuotientCarrierTransitionAdd F hmn).map_zero
  map_add' x y := by
    apply (addEquiv F m).injective
    change Internal.principalUnitQuotientCarrierTransitionAdd F hmn
        (x.val + y.val) =
      Internal.principalUnitQuotientCarrierTransitionAdd F hmn x.val +
        Internal.principalUnitQuotientCarrierTransitionAdd F hmn y.val
    exact (Internal.principalUnitQuotientCarrierTransitionAdd F hmn).map_add x.val y.val

theorem

val_transition

L71 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient.val_transition

Documentation

The wrapped transition has the original additive transition as its value.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField
open Internal
universe u v
variable {K : Type u} [Field K]
namespace DiscretePrincipalUnitQuotient

Lean source · statement

theorem val_transition
    (F : CompleteDVF.{u, v} K) {m n : ℕ} (hmn : m ≤ n)
    (x : DiscretePrincipalUnitQuotient F n) :
    (transition F hmn x).val =
      Internal.principalUnitQuotientCarrierTransitionAdd F hmn x.val

Module documentation

Transitions between principal-unit quotients

Declarations

principalUnitQuotientCarrierTransitionAdd

transition

val_transition