NYLL
Module

NormFiltration.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.NormFiltration
88 declarations indexed from sourceView source ↗

Module documentation

Norm compatibility with unit filtrations

A compatibility hypothesis for a norm and two unit filtrations immediately produces homomorphisms on every filtration level.

Imports1
Imported by2

Declarations

abbrev

MapsFiltrationLevels

L35 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.MapsFiltrationLevels
Documentation

A compatibility hypothesis for the norm and two filtrations.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
abbrev MapsFiltrationLevels : Prop
def

mapLevelOfMapsFiltrationLevels

L40 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.mapLevelOfMapsFiltrationLevels
Documentation

The norm map restricted to a filtration level.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · full declaration
def mapLevelOfMapsFiltrationLevels
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ) :
    UH.principalUnitSubgroup n →* UG.principalUnitSubgroup (targetLevel n) where
  toFun x := ⟨N.toHom x.1, hN n x.2⟩
  map_one' := by
    apply Subtype.ext
    exact N.toHom.map_one
  map_mul' x y := by
    apply Subtype.ext
    exact N.toHom.map_mul x.1 y.1
theorem

mapLevelOfMapsFiltrationLevels_apply

L55 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.mapLevelOfMapsFiltrationLevels_apply
Documentation

The defining evaluation formula for mapLevelOfMapsFiltrationLevels is (mapLevelOfMapsFiltrationLevels N UG UH targetLevel hN n x : G) = N.toHom x.1.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem mapLevelOfMapsFiltrationLevels_apply
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    (x : UH.principalUnitSubgroup n) :
    (mapLevelOfMapsFiltrationLevels N UG UH targetLevel hN n x : G) =
      N.toHom x.1
theorem

maps_principalUnitSubgroup_of_mapsFiltrationLevels

L63 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.maps_principalUnitSubgroup_of_mapsFiltrationLevels
Documentation

The raw membership consequence of filtration compatibility.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem maps_principalUnitSubgroup_of_mapsFiltrationLevels
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ) {x : H}
    (hx : x ∈ UH.principalUnitSubgroup n) :
    N.toHom x ∈ UG.principalUnitSubgroup (targetLevel n)
theorem

maps_principalUnitSubgroup_of_mapsFiltrationLevels_of_le

L71 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.maps_principalUnitSubgroup_of_mapsFiltrationLevels_of_le
Documentation

If the norm sends U_H^n into U_G^(targetLevel n), then it also sends it into any coarser target level.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem maps_principalUnitSubgroup_of_mapsFiltrationLevels_of_le
    (hN : MapsFiltrationLevels N UG UH targetLevel) {n m : ℕ}
    (hm : m ≤ targetLevel n) {x : H}
    (hx : x ∈ UH.principalUnitSubgroup n) :
    N.toHom x ∈ UG.principalUnitSubgroup m
theorem

mapsFiltrationLevels_of_le

L80 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.mapsFiltrationLevels_of_le
Documentation

Filtration compatibility can be weakened by replacing the target level by a coarser one.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem mapsFiltrationLevels_of_le {targetLevel' : ℕ → ℕ}
    (hN : MapsFiltrationLevels N UG UH targetLevel)
    (hle : ∀ n, targetLevel' n ≤ targetLevel n) :
    MapsFiltrationLevels N UG UH targetLevel'
theorem

mapLevelOfMapsFiltrationLevels_surjective_iff

L89 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.mapLevelOfMapsFiltrationLevels_surjective_iff
Documentation

Surjectivity of the norm on a filtration level, stated without subtypes.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem mapLevelOfMapsFiltrationLevels_surjective_iff
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ) :
    Function.Surjective
      (mapLevelOfMapsFiltrationLevels N UG UH targetLevel hN n) ↔
      ∀ y ∈ UG.principalUnitSubgroup (targetLevel n),
        ∃ x ∈ UH.principalUnitSubgroup n, N.toHom x = y
theorem

mapLevelOfMapsFiltrationLevels_range_eq_top_iff

L109 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.mapLevelOfMapsFiltrationLevels_range_eq_top_iff
Documentation

Characterizes (mapLevelOfMapsFiltrationLevels N UG UH targetLevel hN n).range = ⊤ by the equivalent condition ∀ y ∈ UG.principalUnitSubgroup (targetLevel n), ∃ x ∈ UH.principalUnitSubgroup n, N.toHom x = y.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem mapLevelOfMapsFiltrationLevels_range_eq_top_iff
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ) :
    (mapLevelOfMapsFiltrationLevels N UG UH targetLevel hN n).range = ⊤ ↔
      ∀ y ∈ UG.principalUnitSubgroup (targetLevel n),
        ∃ x ∈ UH.principalUnitSubgroup n, N.toHom x = y
def

quotientMapOfMapsFiltrationLevels

L118 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels
Documentation

A compatible norm descends to the quotient by a filtration level.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
def quotientMapOfMapsFiltrationLevels
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] :
    H ⧸ UH.principalUnitSubgroup n →*
      G ⧸ UG.principalUnitSubgroup (targetLevel n)
theorem

quotientMapOfMapsFiltrationLevels_apply_mk

L134 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_apply_mk
Documentation

The defining evaluation formula for quotientMapOfMapsFiltrationLevels is quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n (QuotientGroup.mk x) = QuotientGroup.mk (N.toHom x).

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_apply_mk
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] (x : H) :
    quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n
        (QuotientGroup.mk x) =
      QuotientGroup.mk (N.toHom x)
theorem

quotientMapOfMapsFiltrationLevels_apply_mk'

L148 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_apply_mk'
Documentation

Establishes the identity quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n (QuotientGroup.mk' (UH.principalUnitSubgroup n) x) = QuotientGroup.mk' (UG.principalUnitSubgroup (targetLevel n)) (N.toHom x).

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_apply_mk'
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] (x : H) :
    quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n
        (QuotientGroup.mk' (UH.principalUnitSubgroup n) x) =
      QuotientGroup.mk' (UG.principalUnitSubgroup (targetLevel n))
        (N.toHom x)
def

filtrationPreimageSubgroup

L159 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.filtrationPreimageSubgroup
Documentation

The preimage of the target filtration subgroup under the valued norm.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
def filtrationPreimageSubgroup (n : ℕ) : Subgroup H
theorem

mem_filtrationPreimageSubgroup_iff

L166 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.mem_filtrationPreimageSubgroup_iff
Documentation

Characterizes x ∈ N.filtrationPreimageSubgroup UG targetLevel n by the equivalent condition N.toHom x ∈ UG.principalUnitSubgroup (targetLevel n).

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem mem_filtrationPreimageSubgroup_iff (n : ℕ) (x : H) :
    x ∈ N.filtrationPreimageSubgroup UG targetLevel n ↔
      N.toHom x ∈ UG.principalUnitSubgroup (targetLevel n)
theorem

principalUnitSubgroup_le_filtrationPreimageSubgroup

L174 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitSubgroup_le_filtrationPreimageSubgroup
Documentation

Proves the bound UH.principalUnitSubgroup n ≤ N.filtrationPreimageSubgroup UG targetLevel n.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitSubgroup_le_filtrationPreimageSubgroup
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ) :
    UH.principalUnitSubgroup n ≤
      N.filtrationPreimageSubgroup UG targetLevel n
instance

filtrationPreimageSubgroup_normal

L182 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.filtrationPreimageSubgroup_normal
Documentation

The subgroup appearing in (N.filtrationPreimageSubgroup UG targetLevel n).Normal is normal.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
instance filtrationPreimageSubgroup_normal
    (n : ℕ) [(UG.principalUnitSubgroup (targetLevel n)).Normal] :
    (N.filtrationPreimageSubgroup UG targetLevel n).Normal
def

filtrationPreimageClassInQuotient

L190 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.filtrationPreimageClassInQuotient
Documentation

The class of the norm-preimage of the target filtration subgroup inside the source quotient H ⧸ U_H^n.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
def filtrationPreimageClassInQuotient (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal] :
    Subgroup (H ⧸ UH.principalUnitSubgroup n)
instance

filtrationPreimageClassInQuotient_normal

L200 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.filtrationPreimageClassInQuotient_normal
Documentation

The subgroup appearing in (N.filtrationPreimageClassInQuotient UG UH targetLevel n).Normal is normal.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
instance filtrationPreimageClassInQuotient_normal
    (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] :
    (N.filtrationPreimageClassInQuotient UG UH targetLevel n).Normal
theorem

mem_filtrationPreimageClassInQuotient_iff

L213 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.mem_filtrationPreimageClassInQuotient_iff
Documentation

Characterizes q ∈ N.filtrationPreimageClassInQuotient UG UH targetLevel n by the equivalent condition ∃ x : H, x ∈ N.filtrationPreimageSubgroup UG targetLevel n ∧ QuotientGroup.mk' (UH.principalUnitSubgroup n) x = q.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem mem_filtrationPreimageClassInQuotient_iff
    (n : ℕ) [(UH.principalUnitSubgroup n).Normal]
    (q : H ⧸ UH.principalUnitSubgroup n) :
    q ∈ N.filtrationPreimageClassInQuotient UG UH targetLevel n ↔
      ∃ x : H, x ∈ N.filtrationPreimageSubgroup UG targetLevel n ∧
        QuotientGroup.mk' (UH.principalUnitSubgroup n) x = q
theorem

mem_filtrationPreimageClassInQuotient_iff_exists_norm_mem

L226 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.mem_filtrationPreimageClassInQuotient_iff_exists_norm_mem
Documentation

Characterizes q ∈ N.filtrationPreimageClassInQuotient UG UH targetLevel n by the equivalent condition ∃ x : H, N.toHom x ∈ UG.principalUnitSubgroup (targetLevel n) ∧ QuotientGroup.mk' (UH.principalUnitSubgroup n) x = q.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem mem_filtrationPreimageClassInQuotient_iff_exists_norm_mem
    (n : ℕ) [(UH.principalUnitSubgroup n).Normal]
    (q : H ⧸ UH.principalUnitSubgroup n) :
    q ∈ N.filtrationPreimageClassInQuotient UG UH targetLevel n ↔
      ∃ x : H, N.toHom x ∈ UG.principalUnitSubgroup (targetLevel n) ∧
        QuotientGroup.mk' (UH.principalUnitSubgroup n) x = q
theorem

filtrationPreimageClassInQuotient_mk_mem

L243 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.filtrationPreimageClassInQuotient_mk_mem
Documentation

Establishes the membership statement QuotientGroup.mk' (UH.principalUnitSubgroup n) x ∈ N.filtrationPreimageClassInQuotient UG UH targetLevel n.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem filtrationPreimageClassInQuotient_mk_mem
    {n : ℕ} [(UH.principalUnitSubgroup n).Normal] {x : H}
    (hx : x ∈ N.filtrationPreimageSubgroup UG targetLevel n) :
    QuotientGroup.mk' (UH.principalUnitSubgroup n) x ∈
      N.filtrationPreimageClassInQuotient UG UH targetLevel n
theorem

quotientMapOfMapsFiltrationLevels_ker_eq_filtrationPreimageClass

L253 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_ker_eq_filtrationPreimageClass
Documentation

The kernel of the quotient norm map is the class of the preimage of the target filtration subgroup in the source quotient.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_ker_eq_filtrationPreimageClass
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] :
    (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n).ker =
      N.filtrationPreimageClassInQuotient UG UH targetLevel n
theorem

mem_quotientMapOfMapsFiltrationLevels_ker_iff

L266 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.mem_quotientMapOfMapsFiltrationLevels_ker_iff
Documentation

Characterizes q ∈ (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n).ker by the equivalent condition q ∈ N.filtrationPreimageClassInQuotient UG UH targetLevel n.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem mem_quotientMapOfMapsFiltrationLevels_ker_iff
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (q : H ⧸ UH.principalUnitSubgroup n) :
    q ∈ (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n).ker ↔
      q ∈ N.filtrationPreimageClassInQuotient UG UH targetLevel n
theorem

quotientMapOfMapsFiltrationLevels_eq_one_iff_mem_filtrationPreimageClass

L278 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_eq_one_iff_mem_filtrationPreimageClass
Documentation

Kernel criterion for arbitrary quotient elements under a filtration quotient norm map.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_eq_one_iff_mem_filtrationPreimageClass
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (q : H ⧸ UH.principalUnitSubgroup n) :
    quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n q = 1 ↔
      q ∈ N.filtrationPreimageClassInQuotient UG UH targetLevel n
theorem

quotientMapOfMapsFiltrationLevels_eq_one_iff_exists_norm_mem_repr

L290 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_eq_one_iff_exists_norm_mem_repr
Documentation

Kernel criterion for arbitrary quotient elements, expanded as a concrete representative whose norm lies in the target filtration subgroup.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_eq_one_iff_exists_norm_mem_repr
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (q : H ⧸ UH.principalUnitSubgroup n) :
    quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n q = 1 ↔
      ∃ x : H, N.toHom x ∈ UG.principalUnitSubgroup (targetLevel n) ∧
        QuotientGroup.mk' (UH.principalUnitSubgroup n) x = q
theorem

quotientMapOfMapsFiltrationLevels_eq_iff_div_mem_filtrationPreimageClass

L305 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_eq_iff_div_mem_filtrationPreimageClass
Documentation

Equality criterion for arbitrary quotient elements under a filtration quotient norm map, in right-quotient form.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_eq_iff_div_mem_filtrationPreimageClass
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (q r : H ⧸ UH.principalUnitSubgroup n) :
    quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n q =
        quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n r ↔
      q / r ∈ N.filtrationPreimageClassInQuotient UG UH targetLevel n
theorem

quotientMapOfMapsFiltrationLevels_eq_iff_exists_norm_mem_div_repr

L319 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_eq_iff_exists_norm_mem_div_repr
Documentation

Equality criterion for arbitrary quotient elements, expanded as a concrete representative of q / r whose norm lies in the target filtration subgroup.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_eq_iff_exists_norm_mem_div_repr
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (q r : H ⧸ UH.principalUnitSubgroup n) :
    quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n q =
        quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n r ↔
      ∃ x : H, N.toHom x ∈ UG.principalUnitSubgroup (targetLevel n) ∧
        QuotientGroup.mk' (UH.principalUnitSubgroup n) x = q / r
theorem

quotientMapOfMapsFiltrationLevels_eq_iff_inv_mul_mem_filtrationPreimageClass

L335 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_eq_iff_inv_mul_mem_filtrationPreimageClass
Documentation

Equality criterion for arbitrary quotient elements under a filtration quotient norm map, in left-quotient form.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_eq_iff_inv_mul_mem_filtrationPreimageClass
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (q r : H ⧸ UH.principalUnitSubgroup n) :
    quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n q =
        quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n r ↔
      r⁻¹ * q ∈ N.filtrationPreimageClassInQuotient UG UH targetLevel n
theorem

quotientMapOfMapsFiltrationLevels_eq_iff_exists_norm_mem_inv_mul_repr

L352 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_eq_iff_exists_norm_mem_inv_mul_repr
Documentation

Equality criterion for arbitrary quotient elements, expanded as a concrete representative of r⁻¹ * q whose norm lies in the target filtration subgroup.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_eq_iff_exists_norm_mem_inv_mul_repr
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (q r : H ⧸ UH.principalUnitSubgroup n) :
    quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n q =
        quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n r ↔
      ∃ x : H, N.toHom x ∈ UG.principalUnitSubgroup (targetLevel n) ∧
        QuotientGroup.mk' (UH.principalUnitSubgroup n) x = r⁻¹ * q
theorem

quotientMapOfMapsFiltrationLevels_mk_mem_filtrationPreimageClass_iff

L371 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_mk_mem_filtrationPreimageClass_iff
Documentation

Characterizes QuotientGroup.mk' (UH.principalUnitSubgroup n) x ∈ N.filtrationPreimageClassInQuotient UG UH targetLevel n by the equivalent condition N.toHom x ∈ UG.principalUnitSubgroup (targetLevel n).

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_mk_mem_filtrationPreimageClass_iff
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] (x : H) :
    QuotientGroup.mk' (UH.principalUnitSubgroup n) x ∈
        N.filtrationPreimageClassInQuotient UG UH targetLevel n ↔
      N.toHom x ∈ UG.principalUnitSubgroup (targetLevel n)
theorem

quotientMapOfMapsFiltrationLevels_injective_iff_filtrationPreimageClass_eq_bot

L389 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_injective_iff_filtrationPreimageClass_eq_bot
Documentation

Injectivity of the filtration quotient norm map is equivalent to the filtration-preimage kernel class being trivial.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_injective_iff_filtrationPreimageClass_eq_bot
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] :
    Function.Injective
        (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n) ↔
      N.filtrationPreimageClassInQuotient UG UH targetLevel n = ⊥
theorem

quotientMapOfMapsFiltrationLevels_injective_iff_forall_norm_mem

L404 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_injective_iff_forall_norm_mem
Documentation

Concrete representative criterion for injectivity of the filtration quotient norm map. An element whose norm lands in the target filtration must already be trivial modulo the source filtration.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_injective_iff_forall_norm_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] :
    Function.Injective
        (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n) ↔
      ∀ x : H, N.toHom x ∈ UG.principalUnitSubgroup (targetLevel n) →
        QuotientGroup.mk' (UH.principalUnitSubgroup n) x = 1
theorem

quotientMapOfMapsFiltrationLevels_injective_of_forall_norm_mem

L442 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_injective_of_forall_norm_mem
Documentation

A practical injectivity criterion for filtration quotient norm maps.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_injective_of_forall_norm_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (hKer : ∀ x : H,
      N.toHom x ∈ UG.principalUnitSubgroup (targetLevel n) →
        QuotientGroup.mk' (UH.principalUnitSubgroup n) x = 1) :
    Function.Injective
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n)
theorem

quotientModuloFiltrationPreimageClass_mk_eq_one_iff

L456 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientModuloFiltrationPreimageClass_mk_eq_one_iff
Documentation

One criterion in the double quotient by the filtration-preimage kernel class.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientModuloFiltrationPreimageClass_mk_eq_one_iff
    (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (q : H ⧸ UH.principalUnitSubgroup n) :
    QuotientGroup.mk'
        (N.filtrationPreimageClassInQuotient UG UH targetLevel n) q = 1 ↔
      q ∈ N.filtrationPreimageClassInQuotient UG UH targetLevel n
theorem

quotientModuloFiltrationPreimageClass_mk_mk_eq_one_iff

L471 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientModuloFiltrationPreimageClass_mk_mk_eq_one_iff
Documentation

Characterizes QuotientGroup.mk' (N.filtrationPreimageClassInQuotient UG UH targetLevel n) (QuotientGroup.mk' (UH.principalUnitSubgroup n) x) = 1 by the equivalent condition N.toHom x ∈ UG.principalUnitSubgroup (targetLevel n).

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientModuloFiltrationPreimageClass_mk_mk_eq_one_iff
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] (x : H) :
    QuotientGroup.mk'
        (N.filtrationPreimageClassInQuotient UG UH targetLevel n)
        (QuotientGroup.mk' (UH.principalUnitSubgroup n) x) = 1 ↔
      N.toHom x ∈ UG.principalUnitSubgroup (targetLevel n)
theorem

quotientModuloFiltrationPreimageClass_mk_eq_iff_div_mem

L485 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientModuloFiltrationPreimageClass_mk_eq_iff_div_mem
Documentation

Equality criterion in the double quotient by the filtration-preimage kernel class.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientModuloFiltrationPreimageClass_mk_eq_iff_div_mem
    (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (q r : H ⧸ UH.principalUnitSubgroup n) :
    QuotientGroup.mk'
        (N.filtrationPreimageClassInQuotient UG UH targetLevel n) q =
      QuotientGroup.mk'
        (N.filtrationPreimageClassInQuotient UG UH targetLevel n) r ↔
      q / r ∈ N.filtrationPreimageClassInQuotient UG UH targetLevel n
theorem

quotientModuloFiltrationPreimageClass_mk_mk_eq_iff

L507 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientModuloFiltrationPreimageClass_mk_mk_eq_iff
Documentation

Characterizes QuotientGroup.mk' (N.filtrationPreimageClassInQuotient UG UH targetLevel n) (QuotientGroup.mk' (UH.principalUnitSubgroup n) x) = QuotientGroup.mk' (N.filtrationPreimageClassInQuotient UG UH targetLevel n) (QuotientGroup.mk' (UH.principalUnitSubgroup n) y) by the equivalent condition N.toHom (x / y) ∈ UG.principalUnitSubgroup (targetLevel n).

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientModuloFiltrationPreimageClass_mk_mk_eq_iff
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] (x y : H) :
    QuotientGroup.mk'
        (N.filtrationPreimageClassInQuotient UG UH targetLevel n)
        (QuotientGroup.mk' (UH.principalUnitSubgroup n) x) =
      QuotientGroup.mk'
        (N.filtrationPreimageClassInQuotient UG UH targetLevel n)
        (QuotientGroup.mk' (UH.principalUnitSubgroup n) y) ↔
      N.toHom (x / y) ∈ UG.principalUnitSubgroup (targetLevel n)
theorem

quotientModuloFiltrationPreimageClass_mk_mk_eq_iff_inv_mul

L526 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientModuloFiltrationPreimageClass_mk_mk_eq_iff_inv_mul
Documentation

Left-quotient form of quotientModuloFiltrationPreimageClass_mk_mk_eq_iff.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientModuloFiltrationPreimageClass_mk_mk_eq_iff_inv_mul
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] (x y : H) :
    QuotientGroup.mk'
        (N.filtrationPreimageClassInQuotient UG UH targetLevel n)
        (QuotientGroup.mk' (UH.principalUnitSubgroup n) x) =
      QuotientGroup.mk'
        (N.filtrationPreimageClassInQuotient UG UH targetLevel n)
        (QuotientGroup.mk' (UH.principalUnitSubgroup n) y) ↔
      N.toHom (y⁻¹ * x) ∈ UG.principalUnitSubgroup (targetLevel n)
def

quotientModuloFiltrationPreimageClassEquivRange

L546 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientModuloFiltrationPreimageClassEquivRange
Documentation

First-isomorphism form of the filtration quotient norm map, with codomain the actual range when no surjectivity hypothesis is available.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
def quotientModuloFiltrationPreimageClassEquivRange
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] :
    (H ⧸ UH.principalUnitSubgroup n) ⧸
        N.filtrationPreimageClassInQuotient UG UH targetLevel n ≃*
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n).range
theorem

quotientModuloFiltrationPreimageClassEquivRange_mk

L564 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientModuloFiltrationPreimageClassEquivRange_mk
Documentation

Establishes the identity N.quotientModuloFiltrationPreimageClassEquivRange UG UH targetLevel hN n (QuotientGroup.mk' (N.filtrationPreimageClassInQuotient UG UH targetLevel n) q) = (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n).rangeRestrict q.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientModuloFiltrationPreimageClassEquivRange_mk
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (q : H ⧸ UH.principalUnitSubgroup n) :
    N.quotientModuloFiltrationPreimageClassEquivRange
        UG UH targetLevel hN n
        (QuotientGroup.mk'
          (N.filtrationPreimageClassInQuotient UG UH targetLevel n) q) =
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n).rangeRestrict q
theorem

quotientModuloFiltrationPreimageClassEquivRange_mk_mk

L582 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientModuloFiltrationPreimageClassEquivRange_mk_mk
Documentation

Establishes the identity N.quotientModuloFiltrationPreimageClassEquivRange UG UH targetLevel hN n (QuotientGroup.mk' (N.filtrationPreimageClassInQuotient UG UH targetLevel n) (QuotientGroup.mk' (UH.principalUnitSubgroup n) x)) = (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n).rangeRestrict (QuotientGroup.mk' (UH.principalUnitSubgroup n) x).

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientModuloFiltrationPreimageClassEquivRange_mk_mk
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] (x : H) :
    N.quotientModuloFiltrationPreimageClassEquivRange
        UG UH targetLevel hN n
        (QuotientGroup.mk'
          (N.filtrationPreimageClassInQuotient UG UH targetLevel n)
          (QuotientGroup.mk' (UH.principalUnitSubgroup n) x)) =
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n).rangeRestrict
        (QuotientGroup.mk' (UH.principalUnitSubgroup n) x)
theorem

coe_quotientModuloFiltrationPreimageClassEquivRange_mk

L601 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.coe_quotientModuloFiltrationPreimageClassEquivRange_mk
Documentation

Establishes the identity ((N.quotientModuloFiltrationPreimageClassEquivRange UG UH targetLevel hN n (QuotientGroup.mk' (N.filtrationPreimageClassInQuotient UG UH targetLevel n) q) : (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n).range) : G ⧸ UG.principalUnitSubgroup (targetLevel n)) = quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n q.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem coe_quotientModuloFiltrationPreimageClassEquivRange_mk
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (q : H ⧸ UH.principalUnitSubgroup n) :
    ((N.quotientModuloFiltrationPreimageClassEquivRange
        UG UH targetLevel hN n
        (QuotientGroup.mk'
          (N.filtrationPreimageClassInQuotient UG UH targetLevel n) q) :
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n).range) :
        G ⧸ UG.principalUnitSubgroup (targetLevel n)) =
      quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n q
theorem

coe_quotientModuloFiltrationPreimageClassEquivRange_mk_mk

L624 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.coe_quotientModuloFiltrationPreimageClassEquivRange_mk_mk
Documentation

Establishes the identity ((N.quotientModuloFiltrationPreimageClassEquivRange UG UH targetLevel hN n (QuotientGroup.mk' (N.filtrationPreimageClassInQuotient UG UH targetLevel n) (QuotientGroup.mk' (UH.principalUnitSubgroup n) x)) : (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n).range) : G ⧸ UG.principalUnitSubgroup (targetLevel n)) = QuotientGroup.mk' (UG.principalUnitSubgroup (targetLevel n)) (N.toHom x).

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem coe_quotientModuloFiltrationPreimageClassEquivRange_mk_mk
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] (x : H) :
    ((N.quotientModuloFiltrationPreimageClassEquivRange
        UG UH targetLevel hN n
        (QuotientGroup.mk'
          (N.filtrationPreimageClassInQuotient UG UH targetLevel n)
          (QuotientGroup.mk' (UH.principalUnitSubgroup n) x)) :
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n).range) :
        G ⧸ UG.principalUnitSubgroup (targetLevel n)) =
      QuotientGroup.mk' (UG.principalUnitSubgroup (targetLevel n))
        (N.toHom x)
theorem

quotientModuloFiltrationPreimageClassEquivRange_symm_rangeRestrict

L647 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientModuloFiltrationPreimageClassEquivRange_symm_rangeRestrict
Documentation

Establishes the identity (N.quotientModuloFiltrationPreimageClassEquivRange UG UH targetLevel hN n).symm ((quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n).rangeRestrict q) = QuotientGroup.mk' (N.filtrationPreimageClassInQuotient UG UH targetLevel n) q.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientModuloFiltrationPreimageClassEquivRange_symm_rangeRestrict
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (q : H ⧸ UH.principalUnitSubgroup n) :
    (N.quotientModuloFiltrationPreimageClassEquivRange
        UG UH targetLevel hN n).symm
        ((quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n).rangeRestrict q) =
      QuotientGroup.mk'
        (N.filtrationPreimageClassInQuotient UG UH targetLevel n) q
theorem

quotientModuloFiltrationPreimageClassEquivRange_symm_rangeRestrict_mk

L684 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientModuloFiltrationPreimageClassEquivRange_symm_rangeRestrict_mk
Documentation

Establishes the identity (N.quotientModuloFiltrationPreimageClassEquivRange UG UH targetLevel hN n).symm ((quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n).rangeRestrict (QuotientGroup.mk' (UH.principalUnitSubgroup n) x)) = QuotientGroup.mk' (N.filtrationPreimageClassInQuotient UG UH targetLevel n) (QuotientGroup.mk' (UH.principalUnitSubgroup n) x).

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientModuloFiltrationPreimageClassEquivRange_symm_rangeRestrict_mk
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] (x : H) :
    (N.quotientModuloFiltrationPreimageClassEquivRange
        UG UH targetLevel hN n).symm
        ((quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n).rangeRestrict
          (QuotientGroup.mk' (UH.principalUnitSubgroup n) x)) =
      QuotientGroup.mk'
        (N.filtrationPreimageClassInQuotient UG UH targetLevel n)
        (QuotientGroup.mk' (UH.principalUnitSubgroup n) x)
def

quotientModuloFiltrationPreimageClassEquivTargetOfSurjective

L699 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientModuloFiltrationPreimageClassEquivTargetOfSurjective
Documentation

First-isomorphism form of a surjective filtration quotient norm map.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
def quotientModuloFiltrationPreimageClassEquivTargetOfSurjective
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (hSurj : Function.Surjective
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n)) :
    (H ⧸ UH.principalUnitSubgroup n) ⧸
        N.filtrationPreimageClassInQuotient UG UH targetLevel n ≃*
      G ⧸ UG.principalUnitSubgroup (targetLevel n)
theorem

quotientModuloFiltrationPreimageClassEquivTargetOfSurjective_mk

L719 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientModuloFiltrationPreimageClassEquivTargetOfSurjective_mk
Documentation

Establishes the identity N.quotientModuloFiltrationPreimageClassEquivTargetOfSurjective UG UH targetLevel hN n hSurj (QuotientGroup.mk' (N.filtrationPreimageClassInQuotient UG UH targetLevel n) q) = quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n q.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientModuloFiltrationPreimageClassEquivTargetOfSurjective_mk
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (hSurj : Function.Surjective
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n))
    (q : H ⧸ UH.principalUnitSubgroup n) :
    N.quotientModuloFiltrationPreimageClassEquivTargetOfSurjective
        UG UH targetLevel hN n hSurj
        (QuotientGroup.mk'
          (N.filtrationPreimageClassInQuotient UG UH targetLevel n) q) =
      quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n q
theorem

quotientModuloFiltrationPreimageClassEquivTargetOfSurjective_mk_mk

L747 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientModuloFiltrationPreimageClassEquivTargetOfSurjective_mk_mk
Documentation

Establishes the identity N.quotientModuloFiltrationPreimageClassEquivTargetOfSurjective UG UH targetLevel hN n hSurj (QuotientGroup.mk' (N.filtrationPreimageClassInQuotient UG UH targetLevel n) (QuotientGroup.mk' (UH.principalUnitSubgroup n) x)) = QuotientGroup.mk' (UG.principalUnitSubgroup (targetLevel n)) (N.toHom x).

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientModuloFiltrationPreimageClassEquivTargetOfSurjective_mk_mk
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (hSurj : Function.Surjective
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n)) (x : H) :
    N.quotientModuloFiltrationPreimageClassEquivTargetOfSurjective
        UG UH targetLevel hN n hSurj
        (QuotientGroup.mk'
          (N.filtrationPreimageClassInQuotient UG UH targetLevel n)
          (QuotientGroup.mk' (UH.principalUnitSubgroup n) x)) =
      QuotientGroup.mk' (UG.principalUnitSubgroup (targetLevel n))
        (N.toHom x)
theorem

coe_quotientModuloFiltrationPreimageClassEquivRange_eq_targetOfSurjective

L766 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.coe_quotientModuloFiltrationPreimageClassEquivRange_eq_targetOfSurjective
Documentation

Under quotient-level surjectivity, the target-valued first-isomorphism equivalence is the range-valued equivalence followed by the range inclusion.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem coe_quotientModuloFiltrationPreimageClassEquivRange_eq_targetOfSurjective
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (hSurj : Function.Surjective
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n))
    (z : (H ⧸ UH.principalUnitSubgroup n) ⧸
        N.filtrationPreimageClassInQuotient UG UH targetLevel n) :
    ((N.quotientModuloFiltrationPreimageClassEquivRange
        UG UH targetLevel hN n z :
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n).range) :
        G ⧸ UG.principalUnitSubgroup (targetLevel n)) =
      N.quotientModuloFiltrationPreimageClassEquivTargetOfSurjective
        UG UH targetLevel hN n hSurj z
theorem

quotientModuloFiltrationPreimageClassEquivTargetOfSurjective_symm_map

L803 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientModuloFiltrationPreimageClassEquivTargetOfSurjective_symm_map
Documentation

Establishes the identity (N.quotientModuloFiltrationPreimageClassEquivTargetOfSurjective UG UH targetLevel hN n hSurj).symm (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n q) = QuotientGroup.mk' (N.filtrationPreimageClassInQuotient UG UH targetLevel n) q.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientModuloFiltrationPreimageClassEquivTargetOfSurjective_symm_map
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (hSurj : Function.Surjective
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n))
    (q : H ⧸ UH.principalUnitSubgroup n) :
    (N.quotientModuloFiltrationPreimageClassEquivTargetOfSurjective
        UG UH targetLevel hN n hSurj).symm
        (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n q) =
      QuotientGroup.mk'
        (N.filtrationPreimageClassInQuotient UG UH targetLevel n) q
theorem

quotientModuloFiltrationPreimageClassEquivTargetOfSurjective_symm_mk

L841 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientModuloFiltrationPreimageClassEquivTargetOfSurjective_symm_mk
Documentation

Establishes the identity (N.quotientModuloFiltrationPreimageClassEquivTargetOfSurjective UG UH targetLevel hN n hSurj).symm (QuotientGroup.mk' (UG.principalUnitSubgroup (targetLevel n)) (N.toHom x)) = QuotientGroup.mk' (N.filtrationPreimageClassInQuotient UG UH targetLevel n) (QuotientGroup.mk' (UH.principalUnitSubgroup n) x).

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientModuloFiltrationPreimageClassEquivTargetOfSurjective_symm_mk
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (hSurj : Function.Surjective
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n)) (x : H) :
    (N.quotientModuloFiltrationPreimageClassEquivTargetOfSurjective
        UG UH targetLevel hN n hSurj).symm
        (QuotientGroup.mk' (UG.principalUnitSubgroup (targetLevel n))
          (N.toHom x)) =
      QuotientGroup.mk'
        (N.filtrationPreimageClassInQuotient UG UH targetLevel n)
        (QuotientGroup.mk' (UH.principalUnitSubgroup n) x)
theorem

quotientMapOfMapsFiltrationLevels_mk_eq_one_iff

L861 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_mk_eq_one_iff
Documentation

Kernel criterion for the quotient map induced by filtration-compatible norms.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_mk_eq_one_iff
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] (x : H) :
    quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n
        (QuotientGroup.mk x) = 1 ↔
      N.toHom x ∈ UG.principalUnitSubgroup (targetLevel n)
theorem

quotientMapOfMapsFiltrationLevels_mk_eq_iff

L873 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_mk_eq_iff
Documentation

Equality criterion for the quotient map induced by filtration-compatible norms.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_mk_eq_iff
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] (x y : H) :
    quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n
        (QuotientGroup.mk x) =
      quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n
        (QuotientGroup.mk y) ↔
      N.toHom (x / y) ∈ UG.principalUnitSubgroup (targetLevel n)
theorem

quotientMapOfMapsFiltrationLevels_mk_eq_iff_inv_mul

L891 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_mk_eq_iff_inv_mul
Documentation

Left-quotient equality criterion for the quotient map induced by filtration-compatible norms.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_mk_eq_iff_inv_mul
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] (x y : H) :
    quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n
        (QuotientGroup.mk x) =
      quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n
        (QuotientGroup.mk y) ↔
      N.toHom (y⁻¹ * x) ∈ UG.principalUnitSubgroup (targetLevel n)
theorem

quotientMapOfMapsFiltrationLevels_surjective_iff_exists_div_mem

L908 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_surjective_iff_exists_div_mem
Documentation

Quotient-level surjectivity is equivalent to lifting every target element up to the target filtration subgroup.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_surjective_iff_exists_div_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] :
    Function.Surjective
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n) ↔
      ∀ g : G, ∃ x : H,
        N.toHom x / g ∈ UG.principalUnitSubgroup (targetLevel n)
theorem

quotientMapOfMapsFiltrationLevels_surjective_of_exists_div_mem

L940 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_surjective_of_exists_div_mem
Documentation

A practical quotient-surjectivity criterion: it is enough to lift every target element modulo the target filtration subgroup.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_surjective_of_exists_div_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (hLift : ∀ g : G, ∃ x : H,
      N.toHom x / g ∈ UG.principalUnitSubgroup (targetLevel n)) :
    Function.Surjective
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n)
theorem

quotientMapOfMapsFiltrationLevels_range_eq_top_iff_exists_div_mem

L953 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_range_eq_top_iff_exists_div_mem
Documentation

Quotient-map range is top exactly when every target element is a norm modulo the target filtration subgroup.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_range_eq_top_iff_exists_div_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] :
    (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n).range = ⊤ ↔
      ∀ g : G, ∃ x : H,
        N.toHom x / g ∈ UG.principalUnitSubgroup (targetLevel n)
theorem

quotientMapOfMapsFiltrationLevels_surjective_iff_exists_inv_mul_mem

L965 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_surjective_iff_exists_inv_mul_mem
Documentation

Left-quotient form of quotient-level surjectivity.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_surjective_iff_exists_inv_mul_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] :
    Function.Surjective
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n) ↔
      ∀ g : G, ∃ x : H,
        g⁻¹ * N.toHom x ∈ UG.principalUnitSubgroup (targetLevel n)
theorem

quotientMapOfMapsFiltrationLevels_surjective_of_exists_inv_mul_mem

L988 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_surjective_of_exists_inv_mul_mem
Documentation

A practical left-quotient criterion for quotient-level surjectivity.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_surjective_of_exists_inv_mul_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (hLift : ∀ g : G, ∃ x : H,
      g⁻¹ * N.toHom x ∈ UG.principalUnitSubgroup (targetLevel n)) :
    Function.Surjective
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n)
theorem

quotientMapOfMapsFiltrationLevels_comp_targetLevelChange

L1001 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_comp_targetLevelChange
Documentation

Coarsening the target filtration level commutes with the induced quotient norm map.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_comp_targetLevelChange
    {targetLevel' : ℕ → ℕ}
    (hN : MapsFiltrationLevels N UG UH targetLevel)
    (hle : ∀ n, targetLevel' n ≤ targetLevel n) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    [(UG.principalUnitSubgroup (targetLevel' n)).Normal] :
    (UG.quotient_principalUnitSubgroup_mapOfLe (hle n)).comp
        (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n) =
      quotientMapOfMapsFiltrationLevels N UG UH targetLevel'
        (N.mapsFiltrationLevels_of_le UG UH targetLevel hN hle) n
theorem

quotientMapOfMapsFiltrationLevels_sourceLevelChange

L1020 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_sourceLevelChange
Documentation

The quotient norm maps are natural in the source and target filtration levels.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_sourceLevelChange
    (hN : MapsFiltrationLevels N UG UH targetLevel) {m n : ℕ}
    (hmn : m ≤ n) (htarget : targetLevel m ≤ targetLevel n)
    [(UH.principalUnitSubgroup n).Normal]
    [(UH.principalUnitSubgroup m).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    [(UG.principalUnitSubgroup (targetLevel m)).Normal] :
    (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN m).comp
        (UH.quotient_principalUnitSubgroup_mapOfLe hmn) =
      (UG.quotient_principalUnitSubgroup_mapOfLe htarget).comp
        (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n)
theorem

quotientMapOfMapsFiltrationLevels_surjective_of_targetLevelChange

L1039 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_surjective_of_targetLevelChange
Documentation

Surjectivity of a quotient norm map descends when the target filtration level is coarsened.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_surjective_of_targetLevelChange
    {targetLevel' : ℕ → ℕ}
    (hN : MapsFiltrationLevels N UG UH targetLevel)
    (hle : ∀ n, targetLevel' n ≤ targetLevel n) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    [(UG.principalUnitSubgroup (targetLevel' n)).Normal]
    (hSurj : Function.Surjective
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n)) :
    Function.Surjective
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel'
        (N.mapsFiltrationLevels_of_le UG UH targetLevel hN hle) n)
theorem

quotientMapOfMapsFiltrationLevels_range_eq_top_of_targetLevelChange

L1062 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_range_eq_top_of_targetLevelChange
Documentation

Range-top form of quotientMapOfMapsFiltrationLevels_surjective_of_targetLevelChange.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_range_eq_top_of_targetLevelChange
    {targetLevel' : ℕ → ℕ}
    (hN : MapsFiltrationLevels N UG UH targetLevel)
    (hle : ∀ n, targetLevel' n ≤ targetLevel n) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    [(UG.principalUnitSubgroup (targetLevel' n)).Normal]
    (hRange :
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n).range =
        ⊤) :
    (quotientMapOfMapsFiltrationLevels N UG UH targetLevel'
      (N.mapsFiltrationLevels_of_le UG UH targetLevel hN hle) n).range =
        ⊤
theorem

quotientMapOfMapsFiltrationLevels_surjective_of_sourceLevelChange

L1081 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_surjective_of_sourceLevelChange
Documentation

Surjectivity of quotient norm maps descends along compatible source and target filtration level changes.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_surjective_of_sourceLevelChange
    (hN : MapsFiltrationLevels N UG UH targetLevel) {m n : ℕ}
    (hmn : m ≤ n) (htarget : targetLevel m ≤ targetLevel n)
    [(UH.principalUnitSubgroup n).Normal]
    [(UH.principalUnitSubgroup m).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    [(UG.principalUnitSubgroup (targetLevel m)).Normal]
    (hSurj : Function.Surjective
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n)) :
    Function.Surjective
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN m)
def

principalUnitSubquotientMapOfMapsFiltrationLevels

L1106 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitSubquotientMapOfMapsFiltrationLevels
Documentation

A filtration-compatible norm induces maps on principal-unit subquotients: U_H^m/U_H^n → U_G^(targetLevel m)/U_G^(targetLevel n).

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
def principalUnitSubquotientMapOfMapsFiltrationLevels
    (hN : MapsFiltrationLevels N UG UH targetLevel) {m n : ℕ}
    (_hmn : m ≤ n) (_htarget : targetLevel m ≤ targetLevel n)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] :
    UH.principalUnitSubquotient m n →*
      UG.principalUnitSubquotient (targetLevel m) (targetLevel n)
theorem

principalUnitSubquotientMapOfMapsFiltrationLevels_apply_mk

L1129 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitSubquotientMapOfMapsFiltrationLevels_apply_mk
Documentation

The defining evaluation formula for principalUnitSubquotientMapOfMapsFiltrationLevels is N.principalUnitSubquotientMapOfMapsFiltrationLevels UG UH targetLevel hN hmn htarget (UH.principalUnitSubquotientMk m n x) = UG.principalUnitSubquotientMk (targetLevel m) (targetLevel n) (mapLevelOfMapsFiltrationLevels N UG UH targetLevel hN m x).

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitSubquotientMapOfMapsFiltrationLevels_apply_mk
    (hN : MapsFiltrationLevels N UG UH targetLevel) {m n : ℕ}
    (hmn : m ≤ n) (htarget : targetLevel m ≤ targetLevel n)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (x : UH.principalUnitSubgroup m) :
    N.principalUnitSubquotientMapOfMapsFiltrationLevels
        UG UH targetLevel hN hmn htarget
        (UH.principalUnitSubquotientMk m n x) =
      UG.principalUnitSubquotientMk (targetLevel m) (targetLevel n)
        (mapLevelOfMapsFiltrationLevels N UG UH targetLevel hN m x)
theorem

coe_principalUnitSubquotientEquivClassInQuotient_map

L1144 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.coe_principalUnitSubquotientEquivClassInQuotient_map
Documentation

The subquotient norm map agrees with the ambient quotient norm map under the canonical embeddings of subquotients as classes in ambient quotients.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem coe_principalUnitSubquotientEquivClassInQuotient_map
    (hN : MapsFiltrationLevels N UG UH targetLevel) {m n : ℕ}
    (hmn : m ≤ n) (htarget : targetLevel m ≤ targetLevel n)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (z : UH.principalUnitSubquotient m n) :
    ((UG.principalUnitSubquotientEquivClassInQuotientOfLe htarget
        (N.principalUnitSubquotientMapOfMapsFiltrationLevels
          UG UH targetLevel hN hmn htarget z) :
      UG.principalUnitSubgroupClassInQuotient (targetLevel m)
        (targetLevel n)) :
      G ⧸ UG.principalUnitSubgroup (targetLevel n)) =
      quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n
        ((UH.principalUnitSubquotientEquivClassInQuotientOfLe hmn z :
          UH.principalUnitSubgroupClassInQuotient m n) :
          H ⧸ UH.principalUnitSubgroup n)
def

principalUnitGradedPieceMapOfMapsFiltrationLevels

L1179 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitGradedPieceMapOfMapsFiltrationLevels
Documentation

The graded-piece form of principalUnitSubquotientMapOfMapsFiltrationLevels.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
def principalUnitGradedPieceMapOfMapsFiltrationLevels
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    (htarget : targetLevel n ≤ targetLevel (n + 1))
    [(UH.principalUnitSubgroup (n + 1)).Normal]
    [(UG.principalUnitSubgroup (targetLevel (n + 1))).Normal] :
    UH.principalUnitGradedPiece n →*
      UG.principalUnitSubquotient (targetLevel n) (targetLevel (n + 1))
theorem

principalUnitGradedPieceMapOfMapsFiltrationLevels_apply_mk

L1196 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitGradedPieceMapOfMapsFiltrationLevels_apply_mk
Documentation

The defining evaluation formula for principalUnitGradedPieceMapOfMapsFiltrationLevels is N.principalUnitGradedPieceMapOfMapsFiltrationLevels UG UH targetLevel hN n htarget (UH.principalUnitGradedPieceMk n x) = UG.principalUnitSubquotientMk (targetLevel n) (targetLevel (n + 1)) (mapLevelOfMapsFiltrationLevels N UG UH targetLevel hN n x).

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitGradedPieceMapOfMapsFiltrationLevels_apply_mk
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    (htarget : targetLevel n ≤ targetLevel (n + 1))
    [(UH.principalUnitSubgroup (n + 1)).Normal]
    [(UG.principalUnitSubgroup (targetLevel (n + 1))).Normal]
    (x : UH.principalUnitSubgroup n) :
    N.principalUnitGradedPieceMapOfMapsFiltrationLevels
        UG UH targetLevel hN n htarget
        (UH.principalUnitGradedPieceMk n x) =
      UG.principalUnitSubquotientMk (targetLevel n) (targetLevel (n + 1))
        (mapLevelOfMapsFiltrationLevels N UG UH targetLevel hN n x)
theorem

principalUnitSubquotientMapOfMapsFiltrationLevels_mk_eq_one_iff

L1211 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitSubquotientMapOfMapsFiltrationLevels_mk_eq_one_iff
Documentation

Kernel criterion on representatives for the principal-unit subquotient map induced by a filtration-compatible norm.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitSubquotientMapOfMapsFiltrationLevels_mk_eq_one_iff
    (hN : MapsFiltrationLevels N UG UH targetLevel) {m n : ℕ}
    (hmn : m ≤ n) (htarget : targetLevel m ≤ targetLevel n)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (x : UH.principalUnitSubgroup m) :
    N.principalUnitSubquotientMapOfMapsFiltrationLevels
        UG UH targetLevel hN hmn htarget
        (UH.principalUnitSubquotientMk m n x) = 1 ↔
      N.toHom (x : H) ∈ UG.principalUnitSubgroup (targetLevel n)
theorem

principalUnitSubquotientMapOfMapsFiltrationLevels_mk_eq_iff_div_mem

L1229 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitSubquotientMapOfMapsFiltrationLevels_mk_eq_iff_div_mem
Documentation

Equality criterion on representatives for the principal-unit subquotient map induced by a filtration-compatible norm, in right-quotient form.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitSubquotientMapOfMapsFiltrationLevels_mk_eq_iff_div_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) {m n : ℕ}
    (hmn : m ≤ n) (htarget : targetLevel m ≤ targetLevel n)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (x y : UH.principalUnitSubgroup m) :
    N.principalUnitSubquotientMapOfMapsFiltrationLevels
        UG UH targetLevel hN hmn htarget
        (UH.principalUnitSubquotientMk m n x) =
      N.principalUnitSubquotientMapOfMapsFiltrationLevels
        UG UH targetLevel hN hmn htarget
        (UH.principalUnitSubquotientMk m n y) ↔
      N.toHom ((x / y : UH.principalUnitSubgroup m) : H) ∈
        UG.principalUnitSubgroup (targetLevel n)
theorem

principalUnitSubquotientMapOfMapsFiltrationLevels_mk_eq_iff_inv_mul_mem

L1254 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitSubquotientMapOfMapsFiltrationLevels_mk_eq_iff_inv_mul_mem
Documentation

Equality criterion on representatives for the principal-unit subquotient map induced by a filtration-compatible norm, in left-quotient form.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitSubquotientMapOfMapsFiltrationLevels_mk_eq_iff_inv_mul_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) {m n : ℕ}
    (hmn : m ≤ n) (htarget : targetLevel m ≤ targetLevel n)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (x y : UH.principalUnitSubgroup m) :
    N.principalUnitSubquotientMapOfMapsFiltrationLevels
        UG UH targetLevel hN hmn htarget
        (UH.principalUnitSubquotientMk m n x) =
      N.principalUnitSubquotientMapOfMapsFiltrationLevels
        UG UH targetLevel hN hmn htarget
        (UH.principalUnitSubquotientMk m n y) ↔
      N.toHom ((y⁻¹ * x : UH.principalUnitSubgroup m) : H) ∈
        UG.principalUnitSubgroup (targetLevel n)
theorem

principalUnitSubquotientMapOfMapsFiltrationLevels_surjective_iff_exists_div_mem

L1276 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitSubquotientMapOfMapsFiltrationLevels_surjective_iff_exists_div_mem
Documentation

Surjectivity of the principal-unit subquotient norm map is equivalent to lifting every target representative modulo the next target level.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitSubquotientMapOfMapsFiltrationLevels_surjective_iff_exists_div_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) {m n : ℕ}
    (hmn : m ≤ n) (htarget : targetLevel m ≤ targetLevel n)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] :
    Function.Surjective
        (N.principalUnitSubquotientMapOfMapsFiltrationLevels
          UG UH targetLevel hN hmn htarget) ↔
      ∀ y : UG.principalUnitSubgroup (targetLevel m),
        ∃ x : UH.principalUnitSubgroup m,
          N.toHom (x : H) / (y : G) ∈
            UG.principalUnitSubgroup (targetLevel n)
theorem

principalUnitSubquotientMapOfMapsFiltrationLevels_surjective_of_exists_div_mem

L1332 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitSubquotientMapOfMapsFiltrationLevels_surjective_of_exists_div_mem
Documentation

A practical surjectivity criterion for principal-unit subquotient norm maps.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitSubquotientMapOfMapsFiltrationLevels_surjective_of_exists_div_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) {m n : ℕ}
    (hmn : m ≤ n) (htarget : targetLevel m ≤ targetLevel n)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (hLift : ∀ y : UG.principalUnitSubgroup (targetLevel m),
      ∃ x : UH.principalUnitSubgroup m,
        N.toHom (x : H) / (y : G) ∈
          UG.principalUnitSubgroup (targetLevel n)) :
    Function.Surjective
      (N.principalUnitSubquotientMapOfMapsFiltrationLevels
        UG UH targetLevel hN hmn htarget)
theorem

principalUnitSubquotientMapOfMapsFiltrationLevels_range_eq_top_iff_exists_div_mem

L1349 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitSubquotientMapOfMapsFiltrationLevels_range_eq_top_iff_exists_div_mem
Documentation

Range-top form of the principal-unit subquotient norm map surjectivity criterion.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitSubquotientMapOfMapsFiltrationLevels_range_eq_top_iff_exists_div_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) {m n : ℕ}
    (hmn : m ≤ n) (htarget : targetLevel m ≤ targetLevel n)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] :
    (N.principalUnitSubquotientMapOfMapsFiltrationLevels
        UG UH targetLevel hN hmn htarget).range = ⊤ ↔
      ∀ y : UG.principalUnitSubgroup (targetLevel m),
        ∃ x : UH.principalUnitSubgroup m,
          N.toHom (x : H) / (y : G) ∈
            UG.principalUnitSubgroup (targetLevel n)
theorem

principalUnitSubquotientMapOfMapsFiltrationLevels_range_eq_top_of_exists_div_mem

L1366 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitSubquotientMapOfMapsFiltrationLevels_range_eq_top_of_exists_div_mem
Documentation

Range-top form of principalUnitSubquotientMapOfMapsFiltrationLevels_surjective_of_exists_div_mem.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitSubquotientMapOfMapsFiltrationLevels_range_eq_top_of_exists_div_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) {m n : ℕ}
    (hmn : m ≤ n) (htarget : targetLevel m ≤ targetLevel n)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (hLift : ∀ y : UG.principalUnitSubgroup (targetLevel m),
      ∃ x : UH.principalUnitSubgroup m,
        N.toHom (x : H) / (y : G) ∈
          UG.principalUnitSubgroup (targetLevel n)) :
    (N.principalUnitSubquotientMapOfMapsFiltrationLevels
        UG UH targetLevel hN hmn htarget).range = ⊤
theorem

principalUnitSubquotientMapOfMapsFiltrationLevels_surjective_iff_exists_inv_mul_mem

L1381 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitSubquotientMapOfMapsFiltrationLevels_surjective_iff_exists_inv_mul_mem
Documentation

Left-quotient form of principal-unit subquotient norm map surjectivity.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitSubquotientMapOfMapsFiltrationLevels_surjective_iff_exists_inv_mul_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) {m n : ℕ}
    (hmn : m ≤ n) (htarget : targetLevel m ≤ targetLevel n)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] :
    Function.Surjective
        (N.principalUnitSubquotientMapOfMapsFiltrationLevels
          UG UH targetLevel hN hmn htarget) ↔
      ∀ y : UG.principalUnitSubgroup (targetLevel m),
        ∃ x : UH.principalUnitSubgroup m,
          (y : G)⁻¹ * N.toHom (x : H) ∈
            UG.principalUnitSubgroup (targetLevel n)
theorem

principalUnitSubquotientMapOfMapsFiltrationLevels_surjective_of_exists_inv_mul_mem

L1409 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitSubquotientMapOfMapsFiltrationLevels_surjective_of_exists_inv_mul_mem
Documentation

A practical left-quotient surjectivity criterion for principal-unit subquotient norm maps.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitSubquotientMapOfMapsFiltrationLevels_surjective_of_exists_inv_mul_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) {m n : ℕ}
    (hmn : m ≤ n) (htarget : targetLevel m ≤ targetLevel n)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (hLift : ∀ y : UG.principalUnitSubgroup (targetLevel m),
      ∃ x : UH.principalUnitSubgroup m,
        (y : G)⁻¹ * N.toHom (x : H) ∈
          UG.principalUnitSubgroup (targetLevel n)) :
    Function.Surjective
      (N.principalUnitSubquotientMapOfMapsFiltrationLevels
        UG UH targetLevel hN hmn htarget)
theorem

principalUnitSubquotientMapOfMapsFiltrationLevels_range_eq_top_iff_exists_inv_mul_mem

L1425 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitSubquotientMapOfMapsFiltrationLevels_range_eq_top_iff_exists_inv_mul_mem
Documentation

Range-top left-quotient criterion for principal-unit subquotient norm maps.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitSubquotientMapOfMapsFiltrationLevels_range_eq_top_iff_exists_inv_mul_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) {m n : ℕ}
    (hmn : m ≤ n) (htarget : targetLevel m ≤ targetLevel n)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal] :
    (N.principalUnitSubquotientMapOfMapsFiltrationLevels
        UG UH targetLevel hN hmn htarget).range = ⊤ ↔
      ∀ y : UG.principalUnitSubgroup (targetLevel m),
        ∃ x : UH.principalUnitSubgroup m,
          (y : G)⁻¹ * N.toHom (x : H) ∈
            UG.principalUnitSubgroup (targetLevel n)
theorem

principalUnitSubquotientMapOfMapsFiltrationLevels_range_eq_top_of_exists_inv_mul_mem

L1442 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitSubquotientMapOfMapsFiltrationLevels_range_eq_top_of_exists_inv_mul_mem
Documentation

Range-top form of principalUnitSubquotientMapOfMapsFiltrationLevels_surjective_of_exists_inv_mul_mem.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitSubquotientMapOfMapsFiltrationLevels_range_eq_top_of_exists_inv_mul_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) {m n : ℕ}
    (hmn : m ≤ n) (htarget : targetLevel m ≤ targetLevel n)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (hLift : ∀ y : UG.principalUnitSubgroup (targetLevel m),
      ∃ x : UH.principalUnitSubgroup m,
        (y : G)⁻¹ * N.toHom (x : H) ∈
          UG.principalUnitSubgroup (targetLevel n)) :
    (N.principalUnitSubquotientMapOfMapsFiltrationLevels
        UG UH targetLevel hN hmn htarget).range = ⊤
theorem

principalUnitGradedPieceMapOfMapsFiltrationLevels_mk_eq_one_iff

L1457 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitGradedPieceMapOfMapsFiltrationLevels_mk_eq_one_iff
Documentation

Kernel criterion on representatives for the graded-piece norm map.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitGradedPieceMapOfMapsFiltrationLevels_mk_eq_one_iff
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    (htarget : targetLevel n ≤ targetLevel (n + 1))
    [(UH.principalUnitSubgroup (n + 1)).Normal]
    [(UG.principalUnitSubgroup (targetLevel (n + 1))).Normal]
    (x : UH.principalUnitSubgroup n) :
    N.principalUnitGradedPieceMapOfMapsFiltrationLevels
        UG UH targetLevel hN n htarget
        (UH.principalUnitGradedPieceMk n x) = 1 ↔
      N.toHom (x : H) ∈ UG.principalUnitSubgroup (targetLevel (n + 1))
theorem

principalUnitGradedPieceMapOfMapsFiltrationLevels_mk_eq_iff_div_mem

L1472 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitGradedPieceMapOfMapsFiltrationLevels_mk_eq_iff_div_mem
Documentation

Right-quotient equality criterion on representatives for the graded-piece norm map.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitGradedPieceMapOfMapsFiltrationLevels_mk_eq_iff_div_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    (htarget : targetLevel n ≤ targetLevel (n + 1))
    [(UH.principalUnitSubgroup (n + 1)).Normal]
    [(UG.principalUnitSubgroup (targetLevel (n + 1))).Normal]
    (x y : UH.principalUnitSubgroup n) :
    N.principalUnitGradedPieceMapOfMapsFiltrationLevels
        UG UH targetLevel hN n htarget
        (UH.principalUnitGradedPieceMk n x) =
      N.principalUnitGradedPieceMapOfMapsFiltrationLevels
        UG UH targetLevel hN n htarget
        (UH.principalUnitGradedPieceMk n y) ↔
      N.toHom ((x / y : UH.principalUnitSubgroup n) : H) ∈
        UG.principalUnitSubgroup (targetLevel (n + 1))
theorem

principalUnitGradedPieceMapOfMapsFiltrationLevels_mk_eq_iff_inv_mul_mem

L1491 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitGradedPieceMapOfMapsFiltrationLevels_mk_eq_iff_inv_mul_mem
Documentation

Left-quotient equality criterion on representatives for the graded-piece norm map.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitGradedPieceMapOfMapsFiltrationLevels_mk_eq_iff_inv_mul_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    (htarget : targetLevel n ≤ targetLevel (n + 1))
    [(UH.principalUnitSubgroup (n + 1)).Normal]
    [(UG.principalUnitSubgroup (targetLevel (n + 1))).Normal]
    (x y : UH.principalUnitSubgroup n) :
    N.principalUnitGradedPieceMapOfMapsFiltrationLevels
        UG UH targetLevel hN n htarget
        (UH.principalUnitGradedPieceMk n x) =
      N.principalUnitGradedPieceMapOfMapsFiltrationLevels
        UG UH targetLevel hN n htarget
        (UH.principalUnitGradedPieceMk n y) ↔
      N.toHom ((y⁻¹ * x : UH.principalUnitSubgroup n) : H) ∈
        UG.principalUnitSubgroup (targetLevel (n + 1))
theorem

principalUnitGradedPieceMapOfMapsFiltrationLevels_surjective_iff_exists_div_mem

L1509 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitGradedPieceMapOfMapsFiltrationLevels_surjective_iff_exists_div_mem
Documentation

Right-quotient surjectivity criterion for the graded-piece norm map.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitGradedPieceMapOfMapsFiltrationLevels_surjective_iff_exists_div_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    (htarget : targetLevel n ≤ targetLevel (n + 1))
    [(UH.principalUnitSubgroup (n + 1)).Normal]
    [(UG.principalUnitSubgroup (targetLevel (n + 1))).Normal] :
    Function.Surjective
        (N.principalUnitGradedPieceMapOfMapsFiltrationLevels
          UG UH targetLevel hN n htarget) ↔
      ∀ y : UG.principalUnitSubgroup (targetLevel n),
        ∃ x : UH.principalUnitSubgroup n,
          N.toHom (x : H) / (y : G) ∈
            UG.principalUnitSubgroup (targetLevel (n + 1))
theorem

principalUnitGradedPieceMapOfMapsFiltrationLevels_surjective_iff_exists_inv_mul_mem

L1525 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitGradedPieceMapOfMapsFiltrationLevels_surjective_iff_exists_inv_mul_mem
Documentation

Left-quotient surjectivity criterion for the graded-piece norm map.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitGradedPieceMapOfMapsFiltrationLevels_surjective_iff_exists_inv_mul_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    (htarget : targetLevel n ≤ targetLevel (n + 1))
    [(UH.principalUnitSubgroup (n + 1)).Normal]
    [(UG.principalUnitSubgroup (targetLevel (n + 1))).Normal] :
    Function.Surjective
        (N.principalUnitGradedPieceMapOfMapsFiltrationLevels
          UG UH targetLevel hN n htarget) ↔
      ∀ y : UG.principalUnitSubgroup (targetLevel n),
        ∃ x : UH.principalUnitSubgroup n,
          (y : G)⁻¹ * N.toHom (x : H) ∈
            UG.principalUnitSubgroup (targetLevel (n + 1))
theorem

principalUnitGradedPieceMapOfMapsFiltrationLevels_range_eq_top_iff_exists_div_mem

L1541 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitGradedPieceMapOfMapsFiltrationLevels_range_eq_top_iff_exists_div_mem
Documentation

Range-top right-quotient criterion for the graded-piece norm map.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitGradedPieceMapOfMapsFiltrationLevels_range_eq_top_iff_exists_div_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    (htarget : targetLevel n ≤ targetLevel (n + 1))
    [(UH.principalUnitSubgroup (n + 1)).Normal]
    [(UG.principalUnitSubgroup (targetLevel (n + 1))).Normal] :
    (N.principalUnitGradedPieceMapOfMapsFiltrationLevels
        UG UH targetLevel hN n htarget).range = ⊤ ↔
      ∀ y : UG.principalUnitSubgroup (targetLevel n),
        ∃ x : UH.principalUnitSubgroup n,
          N.toHom (x : H) / (y : G) ∈
            UG.principalUnitSubgroup (targetLevel (n + 1))
theorem

principalUnitGradedPieceMapOfMapsFiltrationLevels_range_eq_top_iff_exists_inv_mul_mem

L1556 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.principalUnitGradedPieceMapOfMapsFiltrationLevels_range_eq_top_iff_exists_inv_mul_mem
Documentation

Range-top left-quotient criterion for the graded-piece norm map.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem principalUnitGradedPieceMapOfMapsFiltrationLevels_range_eq_top_iff_exists_inv_mul_mem
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    (htarget : targetLevel n ≤ targetLevel (n + 1))
    [(UH.principalUnitSubgroup (n + 1)).Normal]
    [(UG.principalUnitSubgroup (targetLevel (n + 1))).Normal] :
    (N.principalUnitGradedPieceMapOfMapsFiltrationLevels
        UG UH targetLevel hN n htarget).range = ⊤ ↔
      ∀ y : UG.principalUnitSubgroup (targetLevel n),
        ∃ x : UH.principalUnitSubgroup n,
          (y : G)⁻¹ * N.toHom (x : H) ∈
            UG.principalUnitSubgroup (targetLevel (n + 1))
theorem

quotientMapOfMapsFiltrationLevels_range_eq_top_of_sourceLevelChange

L1572 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_range_eq_top_of_sourceLevelChange
Documentation

Range-top form of quotientMapOfMapsFiltrationLevels_surjective_of_sourceLevelChange.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_range_eq_top_of_sourceLevelChange
    (hN : MapsFiltrationLevels N UG UH targetLevel) {m n : ℕ}
    (hmn : m ≤ n) (htarget : targetLevel m ≤ targetLevel n)
    [(UH.principalUnitSubgroup n).Normal]
    [(UH.principalUnitSubgroup m).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    [(UG.principalUnitSubgroup (targetLevel m)).Normal]
    (hRange :
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n).range =
        ⊤) :
    (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN m).range =
        ⊤
theorem

quotientMapOfMapsFiltrationLevels_surjective_of_surjective

L1590 ↗
LocalFieldTheory.DiscreteValuationField.ValuedNorm.quotientMapOfMapsFiltrationLevels_surjective_of_surjective
Documentation

A surjective valued norm induces a surjective map on the quotients by any compatible filtration level.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuedNorm
variable {G : Type u} {H : Type v} [Group G] [Group H]
variable {vG : MultiplicativeIntegerValuation G}
variable {vH : MultiplicativeIntegerValuation H}
variable (N : ValuedNorm vG vH)
variable (UG : AntitoneSubgroupFiltration G) (UH : AntitoneSubgroupFiltration H)
variable (targetLevel : ℕ → ℕ)
Lean source · statement
theorem quotientMapOfMapsFiltrationLevels_surjective_of_surjective
    (hN : MapsFiltrationLevels N UG UH targetLevel) (n : ℕ)
    [(UH.principalUnitSubgroup n).Normal]
    [(UG.principalUnitSubgroup (targetLevel n)).Normal]
    (hSurj : Function.Surjective N.toHom) :
    Function.Surjective
      (quotientMapOfMapsFiltrationLevels N UG UH targetLevel hN n)

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