Module

PowerIndex.lean

Nyll.ValuedFieldTheory.LocalField.GroupTheory.PowerIndex

66 declarations indexed from sourceView source ↗

Module documentation

Power indices in commutative groups

Reusable kernel, quotient, product, and additive-transport formulas for n-th powers in commutative groups. The basic power map and its image and kernel are mathlib's powMonoidHom, MonoidHom.range, and MonoidHom.ker.

Imports5

Mathlib.SetTheory.Cardinal.Finite
Mathlib.Algebra.Group.Subgroup.Ker
Mathlib.Algebra.Group.Hom.Basic
Nyll.ValuedFieldTheory.LocalField.GroupTheory.IntegerMultipleSubgroup
Mathlib.RingTheory.RootsOfUnity.Basic

Imported by7

theorem

powMonoidHom_range_one_mem

L41 ↗

LocalFieldTheory.powMonoidHom_range_one_mem

Documentation

The identity element is an n-th power and hence lies in the range of the power endomorphism. The identity element is an n-th power and hence lies in the range of the power endomorphism.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem powMonoidHom_range_one_mem (n : ℕ) :
    (1 : G) ∈ (powMonoidHom n : G →* G).range

theorem

powMonoidHom_range_index_le

L48 ↗

LocalFieldTheory.powMonoidHom_range_index_le

Documentation

A subgroup of a commutative group contains the powers indexed by its index.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem powMonoidHom_range_index_le (H : Subgroup G) :
    (powMonoidHom H.index : G →* G).range ≤ H

theorem

card_nthPowerQuotient_eq_nthPowerKernel

L57 ↗

LocalFieldTheory.card_nthPowerQuotient_eq_nthPowerKernel

Documentation

In a finite commutative group, the n-th-power quotient has the same cardinality as the subgroup of n-torsion elements. This is the finite kernel/cokernel equality for the power endomorphism.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem card_nthPowerQuotient_eq_nthPowerKernel
    [Finite G] (n : ℕ) :
    Nat.card (G ⧸ (powMonoidHom n : G →* G).range) =
      Nat.card ((powMonoidHom n : G →* G).ker)

def

nthPowerKernelEquivOfMulEquiv

L65 ↗

LocalFieldTheory.nthPowerKernelEquivOfMulEquiv

Documentation

A multiplicative equivalence transports n-torsion kernels.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · full declaration

def nthPowerKernelEquivOfMulEquiv (n : ℕ) (e : G ≃* H) :
    (powMonoidHom n : G →* G).ker ≃* (powMonoidHom n : H →* H).ker where
  toFun x :=
    ⟨e (x : G), by
      have hx : (x : G) ^ n = 1 :=
        (MonoidHom.mem_ker (G := G)).1 x.property
      change (e (x : G)) ^ n = 1
      simpa [map_pow] using congrArg e hx⟩
  invFun y :=
    ⟨e.symm (y : H), by
      have hy : (y : H) ^ n = 1 :=
        (MonoidHom.mem_ker (G := H)).1 y.property
      change (e.symm (y : H)) ^ n = 1
      simpa [map_pow] using congrArg e.symm hy⟩
  left_inv x := by
    ext
    simp
  right_inv y := by
    ext
    simp
  map_mul' x y := by
    ext
    simp

theorem

powMonoidHom_range_map

L91 ↗

LocalFieldTheory.powMonoidHom_range_map

Documentation

A multiplicative equivalence carries the range of the n-th power map onto the corresponding range.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem powMonoidHom_range_map (n : ℕ) (e : G ≃* H) :
    ((powMonoidHom n : G →* G).range).map e.toMonoidHom = (powMonoidHom n : H →* H).range

theorem

powMonoidHom_ker_map

L96 ↗

LocalFieldTheory.powMonoidHom_ker_map

Documentation

A multiplicative equivalence transports n-torsion kernels.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem powMonoidHom_ker_map (n : ℕ) (e : G ≃* H) :
    ((powMonoidHom n : G →* G).ker).map e.toMonoidHom =
      (powMonoidHom n : H →* H).ker

theorem

finite_nthPowerKernel_of_injective

L118 ↗

LocalFieldTheory.finite_nthPowerKernel_of_injective

Documentation

An injective multiplicative homomorphism transports finiteness of the ambient power kernel to the source power kernel.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem finite_nthPowerKernel_of_injective
    (n : ℕ) (f : G →* H) (hf : Function.Injective f)
    [Finite ((powMonoidHom n : H →* H).ker)] :
    Finite ((powMonoidHom n : G →* G).ker)

theorem

powMonoidHom_ker_units_eq_rootsOfUnity

L135 ↗

LocalFieldTheory.powMonoidHom_ker_units_eq_rootsOfUnity

Documentation

The power kernel in the unit group of a commutative ring is Mathlib's group of roots of unity.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem powMonoidHom_ker_units_eq_rootsOfUnity
    (R : Type*) [CommRing R] (n : ℕ) :
    (powMonoidHom n : Rˣ →* Rˣ).ker = rootsOfUnity n R

instance

finite_powMonoidHom_ker_units

L143 ↗

LocalFieldTheory.finite_powMonoidHom_ker_units

Documentation

For nonzero exponent over a domain, the unit-group power kernel is finite because it is the finite set of roots of X ^ n - 1.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

instance finite_powMonoidHom_ker_units
    (R : Type*) [CommRing R] [IsDomain R] (n : ℕ) [NeZero n] :
    Finite ((powMonoidHom n : Rˣ →* Rˣ).ker)

def

nthPowerQuotientEquivOfMulEquiv

L150 ↗

LocalFieldTheory.nthPowerQuotientEquivOfMulEquiv

Documentation

A multiplicative equivalence transports quotients by n-th powers.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

def nthPowerQuotientEquivOfMulEquiv (n : ℕ) (e : G ≃* H) :
    G ⧸ (powMonoidHom n : G →* G).range ≃* H ⧸ (powMonoidHom n : H →* H).range

theorem

nthPowerQuotientEquivOfMulEquiv_mk

L158 ↗

LocalFieldTheory.nthPowerQuotientEquivOfMulEquiv_mk

Documentation

The quotient equivalence induced by a multiplicative equivalence maps each power-class representative to its image.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem nthPowerQuotientEquivOfMulEquiv_mk (n : ℕ) (e : G ≃* H) (x : G) :
    nthPowerQuotientEquivOfMulEquiv G H n e
        (QuotientGroup.mk' ((powMonoidHom n : G →* G).range) x) =
      QuotientGroup.mk' ((powMonoidHom n : H →* H).range) (e x)

theorem

finite_nthPowerQuotient_of_mulEquiv

L166 ↗

LocalFieldTheory.finite_nthPowerQuotient_of_mulEquiv

Documentation

Finiteness of a power quotient transports backwards along a multiplicative equivalence.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem finite_nthPowerQuotient_of_mulEquiv
    (n : ℕ) (e : G ≃* H)
    [Finite (H ⧸ (powMonoidHom n : H →* H).range)] :
    Finite (G ⧸ (powMonoidHom n : G →* G).range)

def

nthPowerKernelProductEquiv

L176 ↗

LocalFieldTheory.nthPowerKernelProductEquiv

Documentation

The n-torsion kernel of a product is the product of the two n-torsion kernels.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · full declaration

def nthPowerKernelProductEquiv (n : ℕ) :
    (powMonoidHom n : (G × H) →* (G × H)).ker ≃*
      (powMonoidHom n : G →* G).ker × (powMonoidHom n : H →* H).ker where
  toFun x :=
    (⟨(x : G × H).1, by
        have hx : (x : G × H) ^ n = 1 :=
          (MonoidHom.mem_ker (G := G × H)).1 x.property
        have hfst := congrArg Prod.fst hx
        simpa using hfst⟩,
      ⟨(x : G × H).2, by
        have hx : (x : G × H) ^ n = 1 :=
          (MonoidHom.mem_ker (G := G × H)).1 x.property
        have hsnd := congrArg Prod.snd hx
        simpa using hsnd⟩)
  invFun x :=
    ⟨((x.1 : G), (x.2 : H)), by
      have hx₁ : (x.1 : G) ^ n = 1 :=
        (MonoidHom.mem_ker (G := G)).1 x.1.property
      have hx₂ : (x.2 : H) ^ n = 1 :=
        (MonoidHom.mem_ker (G := H)).1 x.2.property
      change (((x.1 : G), (x.2 : H)) : G × H) ^ n = 1
      ext <;> simp [hx₁, hx₂]⟩
  left_inv x := by
    ext <;> rfl
  right_inv x := by
    ext <;> rfl
  map_mul' x y := by
    ext <;> rfl

instance

finite_powMonoidHom_ker_prod

L207 ↗

LocalFieldTheory.finite_powMonoidHom_ker_prod

Documentation

Finiteness of the two factor kernels transports across the canonical product-kernel equivalence.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

instance finite_powMonoidHom_ker_prod (n : ℕ)
    [Finite ((powMonoidHom n : G →* G).ker)]
    [Finite ((powMonoidHom n : H →* H).ker)] :
    Finite ((powMonoidHom n : (G × H) →* (G × H)).ker)

theorem

cardinal_mk_nthPowerKernelProduct

L217 ↗

LocalFieldTheory.cardinal_mk_nthPowerKernelProduct

Documentation

General cardinal form of the product-kernel decomposition. This is the source of truth before any finiteness specialization.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem cardinal_mk_nthPowerKernelProduct (n : ℕ) :
    Cardinal.mk ((powMonoidHom n : (G × H) →* (G × H)).ker) =
      Cardinal.mk
        ((powMonoidHom n : G →* G).ker × (powMonoidHom n : H →* H).ker)

theorem

card_nthPowerKernelProduct

L224 ↗

LocalFieldTheory.card_nthPowerKernelProduct

Documentation

Cardinality form of nthPowerKernelProductEquiv.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem card_nthPowerKernelProduct (n : ℕ)
    [Finite ((powMonoidHom n : G →* G).ker)]
    [Finite ((powMonoidHom n : H →* H).ker)] :
    Nat.card ((powMonoidHom n : (G × H) →* (G × H)).ker) =
      Nat.card ((powMonoidHom n : G →* G).ker) *
        Nat.card ((powMonoidHom n : H →* H).ker)

theorem

card_nthPowerKernel_eq_mul_of_mulEquiv_prod

L235 ↗

LocalFieldTheory.card_nthPowerKernel_eq_mul_of_mulEquiv_prod

Documentation

A product decomposition of a commutative group splits the cardinality of the n-torsion kernel as the product of the two factor kernels.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem card_nthPowerKernel_eq_mul_of_mulEquiv_prod
    (n : ℕ) (e : G ≃* H × U)
    [Finite ((powMonoidHom n : G →* G).ker)]
    [Finite ((powMonoidHom n : H →* H).ker)]
    [Finite ((powMonoidHom n : U →* U).ker)] :
    Nat.card ((powMonoidHom n : G →* G).ker) =
      Nat.card ((powMonoidHom n : H →* H).ker) *
        Nat.card ((powMonoidHom n : U →* U).ker)

theorem

cardinal_mk_nthPowerKernel_eq_of_mulEquiv_prod

L255 ↗

LocalFieldTheory.cardinal_mk_nthPowerKernel_eq_of_mulEquiv_prod

Documentation

General cardinal form of the kernel decomposition transported by a multiplicative product equivalence.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem cardinal_mk_nthPowerKernel_eq_of_mulEquiv_prod
    (n : ℕ) (e : G ≃* H × U) :
    Cardinal.lift.{max uH uU, uG}
        (Cardinal.mk ((powMonoidHom n : G →* G).ker)) =
      Cardinal.lift.{uG, max uH uU} (Cardinal.mk
        ((powMonoidHom n : H →* H).ker × (powMonoidHom n : U →* U).ker))

def

nthPowerProductQuotientHom

L267 ↗

LocalFieldTheory.nthPowerProductQuotientHom

Documentation

The product map from a product group to the product of its n-th-power quotients.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · full declaration

def nthPowerProductQuotientHom (n : ℕ) :
    G × H →* (G ⧸ (powMonoidHom n : G →* G).range) × (H ⧸ (powMonoidHom n : H →* H).range) where
  toFun x :=
    (QuotientGroup.mk' ((powMonoidHom n : G →* G).range) x.1,
      QuotientGroup.mk' ((powMonoidHom n : H →* H).range) x.2)
  map_one' := rfl
  map_mul' _ _ := rfl

theorem

nthPowerProductQuotientHom_surjective

L276 ↗

LocalFieldTheory.nthPowerProductQuotientHom_surjective

Documentation

Every pair of power classes is represented by a power class in the product group.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem nthPowerProductQuotientHom_surjective (n : ℕ) :
    Function.Surjective (nthPowerProductQuotientHom G H n)

theorem

nthPowerProductQuotientHom_ker

L287 ↗

LocalFieldTheory.nthPowerProductQuotientHom_ker

Documentation

The product power-class homomorphism has trivial kernel.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem nthPowerProductQuotientHom_ker (n : ℕ) :
    (nthPowerProductQuotientHom G H n).ker =
      (powMonoidHom n : (G × H) →* (G × H)).range

def

nthPowerProductQuotientEquiv

L328 ↗

LocalFieldTheory.nthPowerProductQuotientEquiv

Documentation

Quotienting a product by n-th powers is the product of the two n-th-power quotients.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

def nthPowerProductQuotientEquiv (n : ℕ) :
    (G × H) ⧸ (powMonoidHom n : (G × H) →* (G × H)).range ≃*
      (G ⧸ (powMonoidHom n : G →* G).range) × (H ⧸ (powMonoidHom n : H →* H).range)

instance

finite_powMonoidHom_rangeQuotient_prod

L339 ↗

LocalFieldTheory.finite_powMonoidHom_rangeQuotient_prod

Documentation

Finiteness of the factor power quotients transports across the canonical product-quotient equivalence.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

instance finite_powMonoidHom_rangeQuotient_prod (n : ℕ)
    [Finite (G ⧸ (powMonoidHom n : G →* G).range)]
    [Finite (H ⧸ (powMonoidHom n : H →* H).range)] :
    Finite ((G × H) ⧸ (powMonoidHom n : (G × H) →* (G × H)).range)

theorem

cardinal_mk_nthPowerProductQuotient

L348 ↗

LocalFieldTheory.cardinal_mk_nthPowerProductQuotient

Documentation

General cardinal form of the product-quotient decomposition.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem cardinal_mk_nthPowerProductQuotient (n : ℕ) :
    Cardinal.mk ((G × H) ⧸ (powMonoidHom n : (G × H) →* (G × H)).range) =
      Cardinal.mk
        ((G ⧸ (powMonoidHom n : G →* G).range) × (H ⧸ (powMonoidHom n : H →* H).range))

theorem

card_nthPowerProductQuotient

L356 ↗

LocalFieldTheory.card_nthPowerProductQuotient

Documentation

The number of n-th power classes in a product is the product of the two factor class numbers. The number of n-th power classes in a product is the product of the two factor class numbers.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem card_nthPowerProductQuotient (n : ℕ)
    [Finite (G ⧸ (powMonoidHom n : G →* G).range)]
    [Finite (H ⧸ (powMonoidHom n : H →* H).range)] :
    Nat.card ((G × H) ⧸ (powMonoidHom n : (G × H) →* (G × H)).range) =
      Nat.card (G ⧸ (powMonoidHom n : G →* G).range) *
        Nat.card (H ⧸ (powMonoidHom n : H →* H).range)

theorem

card_nthPowerQuotient_eq_mul_of_mulEquiv_prod

L367 ↗

LocalFieldTheory.card_nthPowerQuotient_eq_mul_of_mulEquiv_prod

Documentation

A product decomposition of a commutative group splits the n-th-power quotient index as the product of the two factor indices.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem card_nthPowerQuotient_eq_mul_of_mulEquiv_prod
    (n : ℕ) (e : G ≃* H × U)
    [Finite (G ⧸ (powMonoidHom n : G →* G).range)]
    [Finite (H ⧸ (powMonoidHom n : H →* H).range)]
    [Finite (U ⧸ (powMonoidHom n : U →* U).range)] :
    Nat.card (G ⧸ (powMonoidHom n : G →* G).range) =
      Nat.card (H ⧸ (powMonoidHom n : H →* H).range) *
        Nat.card (U ⧸ (powMonoidHom n : U →* U).range)

theorem

cardinal_mk_nthPowerQuotient_eq_of_mulEquiv_prod

L387 ↗

LocalFieldTheory.cardinal_mk_nthPowerQuotient_eq_of_mulEquiv_prod

Documentation

General cardinal form of the quotient decomposition transported by a multiplicative product equivalence.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem cardinal_mk_nthPowerQuotient_eq_of_mulEquiv_prod
    (n : ℕ) (e : G ≃* H × U) :
    Cardinal.lift.{max uH uU, uG}
        (Cardinal.mk (G ⧸ (powMonoidHom n : G →* G).range)) =
      Cardinal.lift.{uG, max uH uU} (Cardinal.mk
        ((H ⧸ (powMonoidHom n : H →* H).range) × (U ⧸ (powMonoidHom n : U →* U).range)))

theorem

powMonoidHom_range_multiplicativeInt_eq_integerMultipleSubgroup

L399 ↗

LocalFieldTheory.powMonoidHom_range_multiplicativeInt_eq_integerMultipleSubgroup

Documentation

For multiplicative integers, the range of the n-th power map is the subgroup of additive multiples of n.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem powMonoidHom_range_multiplicativeInt_eq_integerMultipleSubgroup
    (n : ℕ) :
    (powMonoidHom n : (Multiplicative ℤ) →* (Multiplicative ℤ)).range =
      integerMultipleSubgroup (n : ℤ)

theorem

finite_multiplicativeInt_nthPowerQuotient

L420 ↗

LocalFieldTheory.finite_multiplicativeInt_nthPowerQuotient

Documentation

For nonzero n, multiplicative integers modulo n-th powers form a finite quotient.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem finite_multiplicativeInt_nthPowerQuotient
    {n : ℕ} (hn : n ≠ 0) :
    Finite (Multiplicative ℤ ⧸ (powMonoidHom n : (Multiplicative ℤ) →* (Multiplicative
      ℤ)).range)

theorem

finite_nthPowerQuotient_of_mulEquiv_units_prod_int

L435 ↗

LocalFieldTheory.finite_nthPowerQuotient_of_mulEquiv_units_prod_int

Documentation

An explicit G ≃ U × ℤ decomposition transports finiteness of the unit-factor power quotient to the full group. This is deliberately a constructor rather than a global instance: callers must expose the decomposition and the exact finite boundary.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem finite_nthPowerQuotient_of_mulEquiv_units_prod_int
    {n : ℕ} [NeZero n] (e : G ≃* U × Multiplicative ℤ)
    [Finite (U ⧸ (powMonoidHom n : U →* U).range)] :
    Finite (G ⧸ (powMonoidHom n : G →* G).range)

theorem

cardinal_mk_multiplicativeInt_nthPowerQuotient

L449 ↗

LocalFieldTheory.cardinal_mk_multiplicativeInt_nthPowerQuotient

Documentation

General cardinal identification of the integer-direction power quotient. For n = 0 the right side is infinite; the natural-cardinality specialization below is therefore intentionally restricted to n ≠ 0.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem cardinal_mk_multiplicativeInt_nthPowerQuotient (n : ℕ) :
    Cardinal.mk
        (Multiplicative ℤ ⧸ (powMonoidHom n : (Multiplicative ℤ) →* (Multiplicative ℤ)).range) =
      Cardinal.mk (Multiplicative (ZMod (n : ℤ).natAbs))

theorem

card_multiplicativeInt_nthPowerQuotient

L459 ↗

LocalFieldTheory.card_multiplicativeInt_nthPowerQuotient

Documentation

For nonzero n, the multiplicative-integer power quotient has cardinality n.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem card_multiplicativeInt_nthPowerQuotient
    {n : ℕ} (hn : n ≠ 0)
    [Finite (Multiplicative ℤ ⧸ (powMonoidHom n : (Multiplicative ℤ) →* (Multiplicative ℤ)).range)]
      :
    Nat.card
        (Multiplicative ℤ ⧸ (powMonoidHom n : (Multiplicative ℤ) →* (Multiplicative ℤ)).range)
          = n

theorem

powMonoidHom_ker_multiplicativeInt_eq_bot

L480 ↗

LocalFieldTheory.powMonoidHom_ker_multiplicativeInt_eq_bot

Documentation

For nonzero n, the n-th power map on multiplicative integers has trivial kernel.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem powMonoidHom_ker_multiplicativeInt_eq_bot
    {n : ℕ} (hn : n ≠ 0) :
    (powMonoidHom n : (Multiplicative ℤ) →* (Multiplicative ℤ)).ker = ⊥

theorem

finite_multiplicativeInt_nthPowerKernel

L500 ↗

LocalFieldTheory.finite_multiplicativeInt_nthPowerKernel

Documentation

The kernel of a nonzero power map on multiplicative integers is finite.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem finite_multiplicativeInt_nthPowerKernel
    {n : ℕ} (hn : n ≠ 0) :
    Finite ((powMonoidHom n : (Multiplicative ℤ) →* (Multiplicative ℤ)).ker)

theorem

card_multiplicativeInt_nthPowerKernel

L507 ↗

LocalFieldTheory.card_multiplicativeInt_nthPowerKernel

Documentation

The kernel of a nonzero power map on multiplicative integers has one element.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem card_multiplicativeInt_nthPowerKernel
    {n : ℕ} (hn : n ≠ 0)
    [Finite ((powMonoidHom n : (Multiplicative ℤ) →* (Multiplicative ℤ)).ker)] :
    Nat.card ((powMonoidHom n : (Multiplicative ℤ) →* (Multiplicative ℤ)).ker) = 1

theorem

card_nthPowerQuotient_eq_mul_of_mulEquiv_units_prod_int

L516 ↗

LocalFieldTheory.card_nthPowerQuotient_eq_mul_of_mulEquiv_units_prod_int

Documentation

If a commutative group splits as U × Multiplicative ℤ, its n-th-power quotient index is n times the corresponding quotient index for U.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem card_nthPowerQuotient_eq_mul_of_mulEquiv_units_prod_int
    {n : ℕ} (hn : n ≠ 0) (e : G ≃* U × Multiplicative ℤ)
    [Finite (G ⧸ (powMonoidHom n : G →* G).range)]
    [Finite (U ⧸ (powMonoidHom n : U →* U).range)] :
    Nat.card (G ⧸ (powMonoidHom n : G →* G).range) =
      n * Nat.card (U ⧸ (powMonoidHom n : U →* U).range)

theorem

cardinal_mk_nthPowerQuotient_eq_of_mulEquiv_units_prod_int

L541 ↗

LocalFieldTheory.cardinal_mk_nthPowerQuotient_eq_of_mulEquiv_units_prod_int

Documentation

General cardinal form of the U × Multiplicative ℤ quotient decomposition, valid without a nonzero or finiteness hypothesis.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem cardinal_mk_nthPowerQuotient_eq_of_mulEquiv_units_prod_int
    (n : ℕ) (e : G ≃* U × Multiplicative ℤ) :
    Cardinal.lift.{uU, uG} (Cardinal.mk (G ⧸ (powMonoidHom n : G →* G).range)) =
      Cardinal.lift.{uG, uU} (Cardinal.mk
        ((U ⧸ (powMonoidHom n : U →* U).range) ×
          (Multiplicative ℤ ⧸ (powMonoidHom n : (Multiplicative ℤ) →* (Multiplicative ℤ)).range)))

theorem

card_nthPowerKernel_eq_of_mulEquiv_units_prod_int

L554 ↗

LocalFieldTheory.card_nthPowerKernel_eq_of_mulEquiv_units_prod_int

Documentation

For nonzero n, a decomposition G ≃ U × ℤ identifies the n-torsion kernel of G with the n-torsion kernel of the unit factor.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem card_nthPowerKernel_eq_of_mulEquiv_units_prod_int
    {n : ℕ} (hn : n ≠ 0) (e : G ≃* U × Multiplicative ℤ)
    [Finite ((powMonoidHom n : G →* G).ker)]
    [Finite ((powMonoidHom n : U →* U).ker)] :
    Nat.card ((powMonoidHom n : G →* G).ker) =
      Nat.card ((powMonoidHom n : U →* U).ker)

theorem

cardinal_mk_nthPowerKernel_eq_of_mulEquiv_units_prod_int

L566 ↗

LocalFieldTheory.cardinal_mk_nthPowerKernel_eq_of_mulEquiv_units_prod_int

Documentation

General cardinal form of the U × Multiplicative ℤ kernel decomposition.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section NthPowers
universe uG uH uU
variable (G : Type uG) (H : Type uH) (U : Type uU)
variable [CommGroup G] [CommGroup H] [CommGroup U]

Lean source · statement

theorem cardinal_mk_nthPowerKernel_eq_of_mulEquiv_units_prod_int
    (n : ℕ) (e : G ≃* U × Multiplicative ℤ) :
    Cardinal.lift.{uU, uG}
        (Cardinal.mk ((powMonoidHom n : G →* G).ker)) =
      Cardinal.lift.{uG, uU} (Cardinal.mk
        ((powMonoidHom n : U →* U).ker ×
          (powMonoidHom n : (Multiplicative ℤ) →* (Multiplicative ℤ)).ker))

abbrev

nsmulAddHom

L586 ↗

LocalFieldTheory.nsmulAddHom

Documentation

The additive homomorphism x ↦ n • x.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]

Lean source · statement

abbrev nsmulAddHom (n : ℕ) : A →+ A

abbrev

nsmulAddSubgroup

L590 ↗

LocalFieldTheory.nsmulAddSubgroup

Documentation

The additive subgroup of n-fold multiples.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]

Lean source · statement

abbrev nsmulAddSubgroup (n : ℕ) : AddSubgroup A

abbrev

nsmulAddKernel

L594 ↗

LocalFieldTheory.nsmulAddKernel

Documentation

The additive subgroup killed by x ↦ n • x.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]

Lean source · statement

abbrev nsmulAddKernel (n : ℕ) : AddSubgroup A

theorem

mem_nsmulAddSubgroup_iff

L600 ↗

LocalFieldTheory.mem_nsmulAddSubgroup_iff

Documentation

Membership in the image of multiplication by n is equivalent to being an n-fold additive multiple.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]

Lean source · statement

theorem mem_nsmulAddSubgroup_iff {n : ℕ} {x : A} :
    x ∈ nsmulAddSubgroup A n ↔ ∃ y : A, n • y = x

theorem

mem_nsmulAddKernel_iff

L606 ↗

LocalFieldTheory.mem_nsmulAddKernel_iff

Documentation

Membership in the kernel of multiplication by n is equivalent to being annihilated by n.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]

Lean source · statement

theorem mem_nsmulAddKernel_iff {n : ℕ} {x : A} :
    x ∈ nsmulAddKernel A n ↔ n • x = 0

theorem

powMonoidHom_range_multiplicative_eq_nsmulAddSubgroup_toSubgroup

L612 ↗

LocalFieldTheory.powMonoidHom_range_multiplicative_eq_nsmulAddSubgroup_toSubgroup

Documentation

Under the Multiplicative wrapper, n-th powers are exactly additive n-fold multiples.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]

Lean source · statement

theorem powMonoidHom_range_multiplicative_eq_nsmulAddSubgroup_toSubgroup
    (n : ℕ) :
    (powMonoidHom n : (Multiplicative A) →* (Multiplicative A)).range =
      AddSubgroup.toSubgroup (nsmulAddSubgroup A n)

theorem

cardinal_mk_multiplicative_nthPowerQuotient_eq_additive_nsmulQuotient

L634 ↗

LocalFieldTheory.cardinal_mk_multiplicative_nthPowerQuotient_eq_additive_nsmulQuotient

Documentation

General cardinal form of the multiplicative/additive quotient translation.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]

Lean source · statement

theorem cardinal_mk_multiplicative_nthPowerQuotient_eq_additive_nsmulQuotient
    (n : ℕ) :
    Cardinal.mk
        (Multiplicative A ⧸ (powMonoidHom n : (Multiplicative A) →* (Multiplicative A)).range) =
      Cardinal.mk (A ⧸ nsmulAddSubgroup A n)

def

multiplicativeNthPowerQuotientEquivAdditive

L644 ↗

LocalFieldTheory.multiplicativeNthPowerQuotientEquivAdditive

Documentation

The underlying quotient types in multiplicative and additive notation are canonically equivalent.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]

Lean source · statement

def multiplicativeNthPowerQuotientEquivAdditive (n : ℕ) :
    (Multiplicative A ⧸ (powMonoidHom n : (Multiplicative A) →* (Multiplicative A)).range) ≃
      (A ⧸ nsmulAddSubgroup A n)

instance

finite_multiplicative_nthPowerQuotient

L652 ↗

LocalFieldTheory.finite_multiplicative_nthPowerQuotient

Documentation

Finiteness of the additive quotient transports to its multiplicative presentation without any choice of representatives.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]

Lean source · statement

instance finite_multiplicative_nthPowerQuotient
    (n : ℕ) [Finite (A ⧸ nsmulAddSubgroup A n)] :
    Finite
      (Multiplicative A ⧸ (powMonoidHom n : (Multiplicative A) →* (Multiplicative A)).range)

theorem

card_multiplicative_nthPowerQuotient_eq_nsmulAddSubgroup_index

L661 ↗

LocalFieldTheory.card_multiplicative_nthPowerQuotient_eq_nsmulAddSubgroup_index

Documentation

Cardinality/index form of powMonoidHom_range_multiplicative_eq_nsmulAddSubgroup_toSubgroup.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]

Lean source · statement

theorem card_multiplicative_nthPowerQuotient_eq_nsmulAddSubgroup_index
    (n : ℕ)
    [Finite (Multiplicative A ⧸ (powMonoidHom n : (Multiplicative A) →* (Multiplicative A)).range)]
      :
    Nat.card (Multiplicative A ⧸ (powMonoidHom n : (Multiplicative A) →* (Multiplicative A)).range)
      =
      (nsmulAddSubgroup A n).index

theorem

card_multiplicative_nthPowerQuotient_eq_additive_nsmulQuotient

L675 ↗

LocalFieldTheory.card_multiplicative_nthPowerQuotient_eq_additive_nsmulQuotient

Documentation

Under logarithmic/additive notation, the n-th-power quotient is the additive quotient by n-fold multiples.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]

Lean source · statement

theorem card_multiplicative_nthPowerQuotient_eq_additive_nsmulQuotient
    (n : ℕ)
    [Finite (Multiplicative A ⧸ (powMonoidHom n : (Multiplicative A) →* (Multiplicative A)).range)]
    [Finite (A ⧸ nsmulAddSubgroup A n)] :
    Nat.card (Multiplicative A ⧸ (powMonoidHom n : (Multiplicative A) →* (Multiplicative A)).range)
      =
      Nat.card (A ⧸ nsmulAddSubgroup A n)

theorem

powMonoidHom_ker_multiplicative_eq_nsmulAddKernel_toSubgroup

L687 ↗

LocalFieldTheory.powMonoidHom_ker_multiplicative_eq_nsmulAddKernel_toSubgroup

Documentation

Under the Multiplicative wrapper, n-torsion is exactly the additive kernel of x ↦ n • x.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]

Lean source · statement

theorem powMonoidHom_ker_multiplicative_eq_nsmulAddKernel_toSubgroup
    (n : ℕ) :
    (powMonoidHom n : (Multiplicative A) →* (Multiplicative A)).ker =
      AddSubgroup.toSubgroup (nsmulAddKernel A n)

theorem

cardinal_mk_multiplicative_nthPowerKernel_eq_nsmulAddKernel

L709 ↗

LocalFieldTheory.cardinal_mk_multiplicative_nthPowerKernel_eq_nsmulAddKernel

Documentation

General cardinal form of the multiplicative/additive kernel translation.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]

Lean source · statement

theorem cardinal_mk_multiplicative_nthPowerKernel_eq_nsmulAddKernel
    (n : ℕ) :
    Cardinal.mk ((powMonoidHom n : (Multiplicative A) →* (Multiplicative A)).ker) =
      Cardinal.mk (nsmulAddKernel A n)

def

multiplicativeNthPowerKernelEquivAdditive

L718 ↗

LocalFieldTheory.multiplicativeNthPowerKernelEquivAdditive

Documentation

The multiplicative power kernel and additive scalar kernel have the same underlying type.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]

Lean source · statement

def multiplicativeNthPowerKernelEquivAdditive (n : ℕ) :
    (powMonoidHom n : (Multiplicative A) →* (Multiplicative A)).ker ≃ nsmulAddKernel A n

instance

finite_multiplicative_nthPowerKernel

L725 ↗

LocalFieldTheory.finite_multiplicative_nthPowerKernel

Documentation

Finiteness of the additive scalar kernel transports to multiplicative notation without introducing a noncanonical enumeration.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]

Lean source · statement

instance finite_multiplicative_nthPowerKernel
    (n : ℕ) [Finite (nsmulAddKernel A n)] :
    Finite ((powMonoidHom n : (Multiplicative A) →* (Multiplicative A)).ker)

instance

finite_nsmulAddQuotient_prod

L736 ↗

LocalFieldTheory.finite_nsmulAddQuotient_prod

Documentation

Finiteness of additive scalar quotients is stable under binary products.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]
section AdditiveProducts
variable (B : Type uB) [AddCommGroup B]

Lean source · statement

instance finite_nsmulAddQuotient_prod (n : ℕ)
    [Finite (A ⧸ nsmulAddSubgroup A n)]
    [Finite (B ⧸ nsmulAddSubgroup B n)] :
    Finite ((A × B) ⧸ nsmulAddSubgroup (A × B) n)

instance

finite_nsmulAddKernel_prod

L753 ↗

LocalFieldTheory.finite_nsmulAddKernel_prod

Documentation

Finiteness of additive scalar kernels is stable under binary products.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]
section AdditiveProducts
variable (B : Type uB) [AddCommGroup B]

Lean source · statement

instance finite_nsmulAddKernel_prod (n : ℕ)
    [Finite (nsmulAddKernel A n)]
    [Finite (nsmulAddKernel B n)] :
    Finite (nsmulAddKernel (A × B) n)

theorem

card_multiplicative_nthPowerKernel_eq_nsmulAddKernel

L773 ↗

LocalFieldTheory.card_multiplicative_nthPowerKernel_eq_nsmulAddKernel

Documentation

Cardinality form of the multiplicative/additive kernel translation.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]

Lean source · statement

theorem card_multiplicative_nthPowerKernel_eq_nsmulAddKernel
    (n : ℕ)
    [Finite ((powMonoidHom n : (Multiplicative A) →* (Multiplicative A)).ker)]
    [Finite (nsmulAddKernel A n)] :
    Nat.card ((powMonoidHom n : (Multiplicative A) →* (Multiplicative A)).ker) =
      Nat.card (nsmulAddKernel A n)

theorem

card_additive_nsmulQuotient_eq_nsmulKernel

L784 ↗

LocalFieldTheory.card_additive_nsmulQuotient_eq_nsmulKernel

Documentation

Finite additive kernel/cokernel equality for the map x ↦ n • x, proved through the multiplicative n-th-power translation.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]

Lean source · statement

theorem card_additive_nsmulQuotient_eq_nsmulKernel
    [Finite A] (n : ℕ) :
    Nat.card (A ⧸ nsmulAddSubgroup A n) =
      Nat.card (nsmulAddKernel A n)

theorem

cardinal_mk_nthPowerQuotient_eq_additive_nsmulQuotient_of_mulEquiv

L796 ↗

LocalFieldTheory.cardinal_mk_nthPowerQuotient_eq_additive_nsmulQuotient_of_mulEquiv

Documentation

General cardinal form of a logarithmic quotient transport.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]
variable (G : Type uG) [CommGroup G]

Lean source · statement

theorem cardinal_mk_nthPowerQuotient_eq_additive_nsmulQuotient_of_mulEquiv
    (n : ℕ) (e : G ≃* Multiplicative A) :
    Cardinal.lift.{uA, uG} (Cardinal.mk (G ⧸ (powMonoidHom n : G →* G).range)) =
      Cardinal.lift.{uG, uA} (Cardinal.mk (A ⧸ nsmulAddSubgroup A n))

theorem

card_nthPowerQuotient_eq_additive_nsmulQuotient_of_mulEquiv

L814 ↗

LocalFieldTheory.card_nthPowerQuotient_eq_additive_nsmulQuotient_of_mulEquiv

Documentation

A logarithmic multiplicative equivalence transports an n-th-power quotient to the additive quotient by n-fold multiples.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]
variable (G : Type uG) [CommGroup G]

Lean source · statement

theorem card_nthPowerQuotient_eq_additive_nsmulQuotient_of_mulEquiv
    (n : ℕ) (e : G ≃* Multiplicative A)
    [Finite (G ⧸ (powMonoidHom n : G →* G).range)]
    [Finite (A ⧸ nsmulAddSubgroup A n)] :
    Nat.card (G ⧸ (powMonoidHom n : G →* G).range) =
      Nat.card (A ⧸ nsmulAddSubgroup A n)

theorem

card_nthPowerKernel_eq_additive_nsmulKernel_of_mulEquiv

L826 ↗

LocalFieldTheory.card_nthPowerKernel_eq_additive_nsmulKernel_of_mulEquiv

Documentation

A logarithmic multiplicative equivalence transports the n-torsion kernel to the additive kernel of x ↦ n • x.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]
variable (G : Type uG) [CommGroup G]

Lean source · statement

theorem card_nthPowerKernel_eq_additive_nsmulKernel_of_mulEquiv
    (n : ℕ) (e : G ≃* Multiplicative A)
    [Finite ((powMonoidHom n : G →* G).ker)]
    [Finite (nsmulAddKernel A n)] :
    Nat.card ((powMonoidHom n : G →* G).ker) =
      Nat.card (nsmulAddKernel A n)

theorem

cardinal_mk_nthPowerKernel_eq_additive_nsmulKernel_of_mulEquiv

L837 ↗

LocalFieldTheory.cardinal_mk_nthPowerKernel_eq_additive_nsmulKernel_of_mulEquiv

Documentation

General cardinal form of a logarithmic kernel transport.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]
variable (G : Type uG) [CommGroup G]

Lean source · statement

theorem cardinal_mk_nthPowerKernel_eq_additive_nsmulKernel_of_mulEquiv
    (n : ℕ) (e : G ≃* Multiplicative A) :
    Cardinal.lift.{uA, uG}
        (Cardinal.mk ((powMonoidHom n : G →* G).ker)) =
      Cardinal.lift.{uG, uA} (Cardinal.mk (nsmulAddKernel A n))

theorem

powMonoidHom_range_eq_comap_nsmulAddSubgroup_toSubgroup_of_mulEquiv

L855 ↗

LocalFieldTheory.powMonoidHom_range_eq_comap_nsmulAddSubgroup_toSubgroup_of_mulEquiv

Documentation

Under a logarithmic multiplicative equivalence, the n-th-power subgroup is the inverse image of the additive n-fold-multiple subgroup.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]
variable (G : Type uG) [CommGroup G]

Lean source · statement

theorem powMonoidHom_range_eq_comap_nsmulAddSubgroup_toSubgroup_of_mulEquiv
    (n : ℕ) (e : G ≃* Multiplicative A) :
    (powMonoidHom n : G →* G).range =
      (AddSubgroup.toSubgroup (nsmulAddSubgroup A n)).comap e.toMonoidHom

theorem

powMonoidHom_ker_eq_comap_nsmulAddKernel_toSubgroup_of_mulEquiv

L886 ↗

LocalFieldTheory.powMonoidHom_ker_eq_comap_nsmulAddKernel_toSubgroup_of_mulEquiv

Documentation

Kernel version of powMonoidHom_range_eq_comap_nsmulAddSubgroup_toSubgroup_of_mulEquiv.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]
variable (G : Type uG) [CommGroup G]

Lean source · statement

theorem powMonoidHom_ker_eq_comap_nsmulAddKernel_toSubgroup_of_mulEquiv
    (n : ℕ) (e : G ≃* Multiplicative A) :
    (powMonoidHom n : G →* G).ker =
      (AddSubgroup.toSubgroup (nsmulAddKernel A n)).comap e.toMonoidHom

theorem

powMonoidHom_range_eq_comap_toSubgroup_of_nsmulAddSubgroup_eq

L915 ↗

LocalFieldTheory.powMonoidHom_range_eq_comap_toSubgroup_of_nsmulAddSubgroup_eq

Documentation

If the additive n-fold multiples have already been identified with a specific additive subgroup, a logarithmic equivalence transports that equality back to the original multiplicative group.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]
variable (G : Type uG) [CommGroup G]

Lean source · statement

theorem powMonoidHom_range_eq_comap_toSubgroup_of_nsmulAddSubgroup_eq
    (n : ℕ) (e : G ≃* Multiplicative A) (B : AddSubgroup A)
    (hB : nsmulAddSubgroup A n = B) :
    (powMonoidHom n : G →* G).range =
      (AddSubgroup.toSubgroup B).comap e.toMonoidHom

theorem

powMonoidHom_ker_eq_comap_toSubgroup_of_nsmulAddKernel_eq

L926 ↗

LocalFieldTheory.powMonoidHom_ker_eq_comap_toSubgroup_of_nsmulAddKernel_eq

Documentation

Kernel analogue of powMonoidHom_range_eq_comap_toSubgroup_of_nsmulAddSubgroup_eq.

Source context 8 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped Int
section AdditivePowers
universe uA uB uG
variable (A : Type uA) [AddCommGroup A]
variable (G : Type uG) [CommGroup G]

Lean source · statement

theorem powMonoidHom_ker_eq_comap_toSubgroup_of_nsmulAddKernel_eq
    (n : ℕ) (e : G ≃* Multiplicative A) (B : AddSubgroup A)
    (hB : nsmulAddKernel A n = B) :
    (powMonoidHom n : G →* G).ker =
      (AddSubgroup.toSubgroup B).comap e.toMonoidHom

Module documentation

Power indices in commutative groups

Declarations