NYLL
Module

Tensor.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.ClassFormation.LocalBlocks.Tensor
45 declarations indexed from sourceView source ↗

Module documentation

The tensor-product realization of a local induced block

This file connects the induced module in LocalBlock with the actual local factor of the scalar-extended adele algebra. The natural Galois action on K_v ⊗[K] L is conjugation on the second tensor factor. The completion tensor-product theorem identifies this algebra with the product of the completions above v.

The first part records the natural tensor action and the canonical identifications between completions at conjugate absolute values. These identifications are the concrete source of the induced-module covariance in the induced local-block calculation.

Imports5
Imported by9

Declarations

abbrev

LocalTensorAlgebra

L46 ↗
LocalClassFieldTheory.LocalTensorAlgebra
Documentation

The local tensor algebra occurring as the factor of 𝔸_K ⊗[K] L at v.

Source context 8 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
Lean source · statement
abbrev LocalTensorAlgebra (vK : AbsoluteValue K ℝ)
def

localTensorConjugation

L50 ↗
LocalClassFieldTheory.localTensorConjugation
Documentation

Galois conjugation on the second factor of the local tensor algebra.

Source context 8 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
Lean source · statement
def localTensorConjugation
    (vK : AbsoluteValue K ℝ) (σ : L ≃ₐ[K] L) :
    LocalTensorAlgebra (L := L) vK ≃ₐ[vK.Completion]
      LocalTensorAlgebra (L := L) vK
theorem

localTensorConjugation_tmul

L70 ↗
LocalClassFieldTheory.localTensorConjugation_tmul
Source context 9 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem localTensorConjugation_tmul
    (vK : AbsoluteValue K ℝ) (σ : L ≃ₐ[K] L)
    (b : vK.Completion) (x : L) :
    localTensorConjugation vK σ (b ⊗ₜ[K] x) =
      b ⊗ₜ[K] σ x
theorem

localTensorConjugation_one

L78 ↗
LocalClassFieldTheory.localTensorConjugation_one
Source context 9 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem localTensorConjugation_one
    (vK : AbsoluteValue K ℝ)
    (z : LocalTensorAlgebra (L := L) vK) :
    localTensorConjugation vK (1 : L ≃ₐ[K] L) z = z
theorem

localTensorConjugation_mul

L87 ↗
LocalClassFieldTheory.localTensorConjugation_mul
Source context 9 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem localTensorConjugation_mul
    (vK : AbsoluteValue K ℝ) (σ τ : L ≃ₐ[K] L)
    (z : LocalTensorAlgebra (L := L) vK) :
    localTensorConjugation vK (σ * τ) z =
      localTensorConjugation vK σ
        (localTensorConjugation vK τ z)
def

localTensorUnitsAction

L100 ↗
LocalClassFieldTheory.localTensorUnitsAction
Documentation

The natural Galois action on the unit group of the local tensor algebra.

Source context 8 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
Lean source · full declaration
def localTensorUnitsAction
    (vK : AbsoluteValue K ℝ) :
    MulDistribMulAction
      (L ≃ₐ[K] L) (LocalTensorAlgebra (L := L) vK)ˣ where
  smul σ z :=
    Units.mapEquiv (localTensorConjugation vK σ).toMulEquiv z
  one_smul z := by
    apply Units.ext
    exact localTensorConjugation_one vK
      (z : LocalTensorAlgebra (L := L) vK)
  mul_smul σ τ z := by
    apply Units.ext
    exact localTensorConjugation_mul vK σ τ
      (z : LocalTensorAlgebra (L := L) vK)
  smul_mul σ x y := by
    apply Units.ext
    exact (localTensorConjugation vK σ).map_mul
      (x : LocalTensorAlgebra (L := L) vK)
      (y : LocalTensorAlgebra (L := L) vK)
  smul_one σ := by
    apply Units.ext
    exact (localTensorConjugation vK σ).map_one
theorem

localTensorUnitsAction_smul_coe

L125 ↗
LocalClassFieldTheory.localTensorUnitsAction_smul_coe
Source context 9 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · full declaration
theorem localTensorUnitsAction_smul_coe
    (vK : AbsoluteValue K ℝ) (σ : L ≃ₐ[K] L)
    (z : (LocalTensorAlgebra (L := L) vK)ˣ) :
    letI := localTensorUnitsAction (K := K) (L := L) vK
    ((σ • z : (LocalTensorAlgebra (L := L) vK)ˣ) :
        LocalTensorAlgebra (L := L) vK) =
      localTensorConjugation vK σ
        (z : LocalTensorAlgebra (L := L) vK) :=
  rfl
def

conjugateWithAbsRingEquiv

L137 ↗
LocalClassFieldTheory.conjugateWithAbsRingEquiv
Documentation

The isometric ring equivalence from the normed copy attached to w ∘ σ to the normed copy attached to w.

Source context 8 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
Lean source · statement
def conjugateWithAbsRingEquiv
    (w : AbsoluteValue L ℝ) (σ : L ≃ₐ[K] L) :
    WithAbs (absoluteValueConjugate w σ) ≃+* WithAbs w
theorem

conjugateWithAbsRingEquiv_isometry

L144 ↗
LocalClassFieldTheory.conjugateWithAbsRingEquiv_isometry
Source context 9 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem conjugateWithAbsRingEquiv_isometry
    (w : AbsoluteValue L ℝ) (σ : L ≃ₐ[K] L) :
    Isometry (conjugateWithAbsRingEquiv w σ)
theorem

conjugateWithAbsRingEquiv_symm_isometry

L153 ↗
LocalClassFieldTheory.conjugateWithAbsRingEquiv_symm_isometry
Source context 9 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem conjugateWithAbsRingEquiv_symm_isometry
    (w : AbsoluteValue L ℝ) (σ : L ≃ₐ[K] L) :
    Isometry (conjugateWithAbsRingEquiv w σ).symm
def

conjugateCompletionRingEquiv

L164 ↗
LocalClassFieldTheory.conjugateCompletionRingEquiv
Documentation

The canonical equivalence between the completions at w ∘ σ and w, induced by σ : L → L.

Source context 8 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
Lean source · statement
def conjugateCompletionRingEquiv
    (w : AbsoluteValue L ℝ) (σ : L ≃ₐ[K] L) :
    (absoluteValueConjugate w σ).Completion ≃+*
      w.Completion
theorem

conjugateCompletionRingEquiv_toCompletion

L175 ↗
LocalClassFieldTheory.conjugateCompletionRingEquiv_toCompletion
Source context 9 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem conjugateCompletionRingEquiv_toCompletion
    (w : AbsoluteValue L ℝ) (σ : L ≃ₐ[K] L) (x : L) :
    conjugateCompletionRingEquiv w σ
        (AbsoluteValue.toCompletion
          (absoluteValueConjugate w σ) x) =
      AbsoluteValue.toCompletion w (σ x)
theorem

conjugateCompletionRingEquiv_completionMap

L197 ↗
LocalClassFieldTheory.conjugateCompletionRingEquiv_completionMap
Documentation

Conjugation fixes the embedded completed base field.

Source context 9 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem conjugateCompletionRingEquiv_completionMap
    (vK : AbsoluteValue K ℝ)
    (w : AbsoluteValueExtension vK L)
    (σ : L ≃ₐ[K] L) (b : vK.Completion) :
    conjugateCompletionRingEquiv w.1 σ
        (AbsoluteValue.completionMap vK
          (absoluteValueConjugate w.1 σ)
          (absoluteValueConjugate_extends vK w σ) b) =
      AbsoluteValue.completionMap vK w.1 w.2 b
theorem

conjugateCompletionRingEquiv_algebraMap

L233 ↗
LocalClassFieldTheory.conjugateCompletionRingEquiv_algebraMap
Source context 9 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · full declaration
theorem conjugateCompletionRingEquiv_algebraMap
    (vK : AbsoluteValue K ℝ)
    (w : AbsoluteValueExtension vK L)
    (σ : L ≃ₐ[K] L) (b : vK.Completion) :
    letI :
        Algebra vK.Completion
          (absoluteValueConjugate w.1 σ).Completion :=
      AbsoluteValue.completionAlgebra vK
        (absoluteValueConjugate w.1 σ)
        (absoluteValueConjugate_extends vK w σ)
    letI : Algebra vK.Completion w.1.Completion :=
      AbsoluteValue.completionAlgebra vK w.1 w.2
    conjugateCompletionRingEquiv w.1 σ
        (algebraMap vK.Completion
          (absoluteValueConjugate w.1 σ).Completion b) =
      algebraMap vK.Completion w.1.Completion b :=
  conjugateCompletionRingEquiv_completionMap vK w σ b
def

conjugateExtensionCompletionRingEquiv

L254 ↗
LocalClassFieldTheory.conjugateExtensionCompletionRingEquiv
Documentation

The conjugate-completion equivalence with its source indexed by the corresponding element of AbsoluteValueExtension. This wrapper keeps dependent product components definitionally aligned.

Source context 8 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
Lean source · statement
def conjugateExtensionCompletionRingEquiv
    (vK : AbsoluteValue K ℝ)
    (w : AbsoluteValueExtension vK L)
    (σ : L ≃ₐ[K] L) :
    (absoluteValueExtensionConjugate vK w σ).1.Completion ≃+*
      w.1.Completion
theorem

conjugateExtensionCompletionRingEquiv_toCompletion

L267 ↗
LocalClassFieldTheory.conjugateExtensionCompletionRingEquiv_toCompletion
Source context 9 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem conjugateExtensionCompletionRingEquiv_toCompletion
    (vK : AbsoluteValue K ℝ)
    (w : AbsoluteValueExtension vK L)
    (σ : L ≃ₐ[K] L) (x : L) :
    conjugateExtensionCompletionRingEquiv vK w σ
        (AbsoluteValue.toCompletion
          (absoluteValueExtensionConjugate vK w σ).1 x) =
      AbsoluteValue.toCompletion w.1 (σ x)
theorem

conjugateExtensionCompletionRingEquiv_algebraMap

L283 ↗
LocalClassFieldTheory.conjugateExtensionCompletionRingEquiv_algebraMap
Source context 9 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · full declaration
theorem conjugateExtensionCompletionRingEquiv_algebraMap
    (vK : AbsoluteValue K ℝ)
    (w : AbsoluteValueExtension vK L)
    (σ : L ≃ₐ[K] L) (b : vK.Completion) :
    letI :
        Algebra vK.Completion
          (absoluteValueExtensionConjugate vK w σ).1.Completion :=
      AbsoluteValue.completionAlgebra vK
        (absoluteValueExtensionConjugate vK w σ).1
        (absoluteValueExtensionConjugate vK w σ).2
    letI : Algebra vK.Completion w.1.Completion :=
      AbsoluteValue.completionAlgebra vK w.1 w.2
    conjugateExtensionCompletionRingEquiv vK w σ
        (algebraMap vK.Completion
          (absoluteValueExtensionConjugate vK w σ).1.Completion b) =
      algebraMap vK.Completion w.1.Completion b := by
  let _ :
      Algebra vK.Completion
        (absoluteValueConjugate w.1 σ).Completion :=
    AbsoluteValue.completionAlgebra vK
      (absoluteValueConjugate w.1 σ)
      (absoluteValueConjugate_extends vK w σ)
  let _ : Algebra vK.Completion w.1.Completion :=
    AbsoluteValue.completionAlgebra vK w.1 w.2
  change
    conjugateCompletionRingEquiv w.1 σ
        (algebraMap vK.Completion
          (absoluteValueConjugate w.1 σ).Completion b) =
      algebraMap vK.Completion w.1.Completion b
  exact conjugateCompletionRingEquiv_algebraMap vK w σ b
def

localTensorEvaluation

L317 ↗
LocalClassFieldTheory.localTensorEvaluation
Documentation

Evaluation of the local tensor algebra in the chosen completion, with codomain written in the algebraic-localization model used by LocalPlaceBlock.

Source context 8 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
Lean source · full declaration
def localTensorEvaluation
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    LocalTensorAlgebra (L := L) vK →ₐ[vK.Completion]
      LocalizedCompletion vK w := by
  letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  letI : SMul K w.1.Completion := hK.toSMul
  letI := AbsoluteValue.completionAlgebra vK w.1 w.2
  exact
    (localizedCompletionEquivCompletion vK hvK w).symm.toAlgHom.comp
      (absoluteValueExtension_localizationTensorHom vK w)
theorem

localTensorEvaluation_tmul

L334 ↗
LocalClassFieldTheory.localTensorEvaluation_tmul
Source context 9 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
omit [IsGalois K L] in
Lean source · full declaration
theorem localTensorEvaluation_tmul
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
    (b : vK.Completion) (x : L) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    localTensorEvaluation vK hvK w (b ⊗ₜ[K] x) =
      algebraMap vK.Completion (LocalizedCompletion vK w) b *
        AbsoluteValue.toAlgebraicLocalization
          vK w.1 w.2 x := by
  let hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  let _ : SMul K w.1.Completion := hK.toSMul
  let _ := AbsoluteValue.completionAlgebra vK w.1 w.2
  apply (localizedCompletionEquivCompletion vK hvK w).injective
  rw [map_mul]
  simp only [localTensorEvaluation, AlgHom.coe_comp, Function.comp_apply,
    absoluteValueExtension_localizationTensorHom_tmul]
  rfl
theorem

localTensorEvaluation_conjugation_decomposition

L358 ↗
LocalClassFieldTheory.localTensorEvaluation_conjugation_decomposition
Documentation

Evaluation at the chosen extension is covariant for left multiplication by the decomposition group. This is the defining covariance relation of the induced module, obtained directly from the localization Galois-group equivalence.

Source context 8 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
Lean source · full declaration
theorem localTensorEvaluation_conjugation_decomposition
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
    (h : absoluteValueDecompositionGroup K w.1)
    (g : L ≃ₐ[K] L)
    (z : LocalTensorAlgebra (L := L) vK) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    localTensorEvaluation vK hvK w
        (localTensorConjugation vK (h.1 * g) z) =
      decompositionGroupEquivAlgebraicLocalizationAut
        vK hvK w h
        (localTensorEvaluation vK hvK w
          (localTensorConjugation vK g z)) := by
  let hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  let _ : SMul K w.1.Completion := hK.toSMul
  let _ := AbsoluteValue.completionAlgebra vK w.1 w.2
  induction z using TensorProduct.inductionOn with
  | add x y hx hy =>
      simpa only [map_add] using congrArg₂ (· + ·) hx hy
  | tmul b x =>
      rw [localTensorConjugation_tmul,
        localTensorConjugation_tmul,
        localTensorEvaluation_tmul,
        localTensorEvaluation_tmul,
        map_mul,
        (decompositionGroupEquivAlgebraicLocalizationAut
          vK hvK w h).commutes,
        localizationRamificationGroups_decompositionGroupEquiv_toLocalization]
      rfl
def

localTensorOrbitHom

L393 ↗
LocalClassFieldTheory.localTensorOrbitHom
Documentation

The canonical orbit-evaluation map from local tensor units to the induced local block. Its covariance is exactly localTensorEvaluation_conjugation_decomposition.

Source context 8 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
Lean source · full declaration
def localTensorOrbitHom
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L) :
    letI :=
      decompositionGroupLocalUnitsAction vK hvK w
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    (LocalTensorAlgebra (L := L) vK)ˣ →*
      LocalPlaceBlock vK hvK w := by
  letI :=
    decompositionGroupLocalUnitsAction vK hvK w
  letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  letI : SMul K w.1.Completion := hK.toSMul
  letI := AbsoluteValue.completionAlgebra vK w.1 w.2
  exact
    { toFun := fun z =>
        ⟨fun g =>
          Units.map
            (localTensorEvaluation vK hvK w).toMonoidHom
            (Units.map
              (localTensorConjugation vK g).toMonoidHom z),
          by
            intro h g
            apply Units.ext
            change
              localTensorEvaluation vK hvK w
                    (localTensorConjugation vK (h.1 * g)
                      (z : LocalTensorAlgebra (L := L) vK)) =
                decompositionGroupEquivAlgebraicLocalizationAut
                  vK hvK w h
                  (localTensorEvaluation vK hvK w
                    (localTensorConjugation vK g
                      (z : LocalTensorAlgebra (L := L) vK)))
            exact
              localTensorEvaluation_conjugation_decomposition
                vK hvK w h g z⟩
      map_one' := by
        apply Subtype.ext
        funext g
        apply Units.ext
        simp
      map_mul' := by
        intro x y
        apply Subtype.ext
        funext g
        apply Units.ext
        simp }
theorem

localTensorOrbitHom_smul

L444 ↗
LocalClassFieldTheory.localTensorOrbitHom_smul
Documentation

Orbit evaluation intertwines natural conjugation on the tensor factor with right translation on the induced module.

Source context 8 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
Lean source · full declaration
theorem localTensorOrbitHom_smul
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
    (τ : L ≃ₐ[K] L)
    (z : (LocalTensorAlgebra (L := L) vK)ˣ) :
    letI :=
      decompositionGroupLocalUnitsAction vK hvK w
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    letI := localTensorUnitsAction (K := K) (L := L) vK
    localTensorOrbitHom vK hvK w (τ • z) =
      τ • localTensorOrbitHom vK hvK w z := by
  let _ :=
    decompositionGroupLocalUnitsAction vK hvK w
  let hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  let _ : SMul K w.1.Completion := hK.toSMul
  let _ := AbsoluteValue.completionAlgebra vK w.1 w.2
  let _ := localTensorUnitsAction (K := K) (L := L) vK
  apply Subtype.ext
  funext g
  apply Units.ext
  change
    localTensorEvaluation vK hvK w
        (localTensorConjugation vK g
          (localTensorConjugation vK τ
            (z : LocalTensorAlgebra (L := L) vK))) =
      localTensorEvaluation vK hvK w
        (localTensorConjugation vK (g * τ)
          (z : LocalTensorAlgebra (L := L) vK))
  rw [localTensorConjugation_mul]
theorem

conjugateExtensionCompletionRingEquiv_completionTensorDecomposition_left

L479 ↗
LocalClassFieldTheory.conjugateExtensionCompletionRingEquiv_completionTensorDecomposition_left
Documentation

After transporting the completion at w ∘ g back to the chosen completion at w, the corresponding component of the tensor-product decomposition is evaluation of the g-conjugate tensor.

Source context 8 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
Lean source · full declaration
theorem conjugateExtensionCompletionRingEquiv_completionTensorDecomposition_left
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
    (g : L ≃ₐ[K] L)
    (z : LocalTensorAlgebra (L := L) vK) :
    letI : ∀ w' : AbsoluteValueExtension vK L,
        Algebra vK.Completion w'.1.Completion :=
      fun w' ↦ AbsoluteValue.completionAlgebra vK w'.1 w'.2
    conjugateExtensionCompletionRingEquiv vK w g
        (completionTensorDecomposition_left (K := K) (L := L) vK hvK z
          (absoluteValueExtensionConjugate vK w g)) =
      absoluteValueExtension_localizationTensorHom vK w
        (localTensorConjugation vK g z) := by
  let _ : ∀ w' : AbsoluteValueExtension vK L,
      Algebra vK.Completion w'.1.Completion :=
    fun w' ↦ AbsoluteValue.completionAlgebra vK w'.1 w'.2
  induction z using TensorProduct.inductionOn with
  | add x y hx hy =>
      simpa only [map_add, Pi.add_apply] using
        congrArg₂ (· + ·) hx hy
  | tmul b x =>
      rw [completionTensorDecomposition_left_tmul_apply,
        map_mul,
        conjugateExtensionCompletionRingEquiv_algebraMap]
      change
        algebraMap vK.Completion w.1.Completion b *
            conjugateExtensionCompletionRingEquiv vK w g
              (AbsoluteValue.toCompletion
                (absoluteValueExtensionConjugate vK w g).1 x) =
          absoluteValueExtension_localizationTensorHom vK w
            (localTensorConjugation vK g (b ⊗ₜ[K] x))
      rw [conjugateExtensionCompletionRingEquiv_toCompletion,
        localTensorConjugation_tmul,
        absoluteValueExtension_localizationTensorHom_tmul]
      change
        algebraMap vK.Completion w.1.Completion b *
            AbsoluteValue.toCompletion w.1 (g x) =
          algebraMap vK.Completion w.1.Completion b *
            AbsoluteValue.toCompletion w.1 (g x)
      rfl
abbrev

InducedRightCosets

L530 ↗
LocalClassFieldTheory.InducedRightCosets
Documentation

Right cosets H \ G, appropriate for the convention f (h * g) = h • f g used by InducedModule.

Source context 11 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section RightCosetCoordinates
universe uG uB
variable {G : Type uG} {B : Type uB}
    [Group G] [CommGroup B]
    (H : Subgroup G) [MulDistribMulAction H B]
Lean source · statement
abbrev InducedRightCosets
def

rightCosetCoefficient

L535 ↗
LocalClassFieldTheory.rightCosetCoefficient
Documentation

The element carrying the chosen representative of the right coset of g to g.

Source context 11 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section RightCosetCoordinates
universe uG uB
variable {G : Type uG} {B : Type uB}
    [Group G] [CommGroup B]
    (H : Subgroup G) [MulDistribMulAction H B]
Lean source · statement
def rightCosetCoefficient (g : G) : H
theorem

rightCosetCoefficient_mul_out

L542 ↗
LocalClassFieldTheory.rightCosetCoefficient_mul_out
Source context 11 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section RightCosetCoordinates
universe uG uB
variable {G : Type uG} {B : Type uB}
    [Group G] [CommGroup B]
    (H : Subgroup G) [MulDistribMulAction H B]
Lean source · statement
theorem rightCosetCoefficient_mul_out (g : G) :
    (rightCosetCoefficient H g : G) *
        Quotient.out (Quotient.mk'' g :
          InducedRightCosets H) = g
theorem

rightCoset_mk_mul_left

L548 ↗
LocalClassFieldTheory.rightCoset_mk_mul_left
Source context 11 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section RightCosetCoordinates
universe uG uB
variable {G : Type uG} {B : Type uB}
    [Group G] [CommGroup B]
    (H : Subgroup G) [MulDistribMulAction H B]
Lean source · statement
theorem rightCoset_mk_mul_left
    (h : H) (g : G) :
    (Quotient.mk'' (h.1 * g) : InducedRightCosets H) =
      Quotient.mk'' g
theorem

rightCosetCoefficient_mul_left

L557 ↗
LocalClassFieldTheory.rightCosetCoefficient_mul_left
Source context 11 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section RightCosetCoordinates
universe uG uB
variable {G : Type uG} {B : Type uB}
    [Group G] [CommGroup B]
    (H : Subgroup G) [MulDistribMulAction H B]
Lean source · statement
theorem rightCosetCoefficient_mul_left
    (h : H) (g : G) :
    rightCosetCoefficient H (h.1 * g) =
      h * rightCosetCoefficient H g
def

inducedRightCosetCoordinates

L569 ↗
LocalClassFieldTheory.inducedRightCosetCoordinates
Documentation

Restriction to one representative of each right coset identifies an induced module with a product indexed by H \ G. No commutativity or cyclicity assumption on G is used.

Source context 11 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section RightCosetCoordinates
universe uG uB
variable {G : Type uG} {B : Type uB}
    [Group G] [CommGroup B]
    (H : Subgroup G) [MulDistribMulAction H B]
Lean source · full declaration
def inducedRightCosetCoordinates :
    InducedModule (B := B) H ≃*
      (InducedRightCosets H → B) where
  toFun f q := f.1 (Quotient.out q)
  invFun b := ⟨fun g =>
      rightCosetCoefficient H g •
        b (Quotient.mk'' g), by
    intro h g
    change
      rightCosetCoefficient H (h.1 * g) •
          b (Quotient.mk'' (h.1 * g)) =
        h •
          (rightCosetCoefficient H g •
            b (Quotient.mk'' g))
    rw [rightCosetCoefficient_mul_left H h g,
      rightCoset_mk_mul_left H h g, mul_smul]⟩
  left_inv f := by
    apply Subtype.ext
    funext g
    change
      rightCosetCoefficient H g •
          f.1 (Quotient.out
            (Quotient.mk'' g : InducedRightCosets H)) =
        f.1 g
    calc
      rightCosetCoefficient H g •
          f.1 (Quotient.out
            (Quotient.mk'' g : InducedRightCosets H)) =
          f.1 ((rightCosetCoefficient H g : G) *
            Quotient.out
              (Quotient.mk'' g : InducedRightCosets H)) :=
        (f.2 (rightCosetCoefficient H g)
          (Quotient.out
            (Quotient.mk'' g : InducedRightCosets H))).symm
      _ = f.1 g := congrArg f.1
        (rightCosetCoefficient_mul_out H g)
  right_inv b := by
    funext q
    change
      rightCosetCoefficient H (Quotient.out q) •
          b (Quotient.mk'' (Quotient.out q)) =
        b q
    have hq :
        (Quotient.mk'' (Quotient.out q) :
          InducedRightCosets H) = q :=
      Quotient.out_eq' q
    rw [hq]
    have hc :
        rightCosetCoefficient H (Quotient.out q) = 1 := by
      apply Subtype.ext
      simp [rightCosetCoefficient, hq]
    rw [hc, one_smul]
  map_mul' f g := by
    funext q
    rfl
theorem

inducedRightCosetCoordinates_apply

L626 ↗
LocalClassFieldTheory.inducedRightCosetCoordinates_apply
Source context 11 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section RightCosetCoordinates
universe uG uB
variable {G : Type uG} {B : Type uB}
    [Group G] [CommGroup B]
    (H : Subgroup G) [MulDistribMulAction H B]
Lean source · statement
theorem inducedRightCosetCoordinates_apply
    (f : InducedModule (B := B) H)
    (q : InducedRightCosets H) :
    inducedRightCosetCoordinates H f q =
      f.1 (Quotient.out q)
def

rightCosetExtension

L644 ↗
LocalClassFieldTheory.rightCosetExtension
Documentation

The chosen representative of a right coset sends w to a well-defined extension above v.

Source context 11 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section ExtensionOrbit
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
local notation "G" => L ≃ₐ[K] L
Lean source · statement
def rightCosetExtension
    (q : InducedRightCosets
      (absoluteValueDecompositionGroup K w.1)) :
    AbsoluteValueExtension vK L
theorem

rightCosetExtension_eq_of_mk

L652 ↗
LocalClassFieldTheory.rightCosetExtension_eq_of_mk
Source context 13 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section ExtensionOrbit
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
local notation "G" => L ≃ₐ[K] L
omit [FiniteDimensional K L] [IsGalois K L] in
include hvK in
Lean source · statement
theorem rightCosetExtension_eq_of_mk
    (g : G) :
    rightCosetExtension vK w
        (Quotient.mk'' g : InducedRightCosets
          (absoluteValueDecompositionGroup K w.1)) =
      absoluteValueExtensionConjugate vK w g
def

rightCosetExtensionEquiv

L690 ↗
LocalClassFieldTheory.rightCosetExtensionEquiv
Documentation

Transitivity of extensions, sharpened to the orbit equivalence H \ G ≃ {w' | w' ∣ v}.

Source context 11 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section ExtensionOrbit
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
local notation "G" => L ≃ₐ[K] L
Lean source · statement
def rightCosetExtensionEquiv :
    InducedRightCosets (absoluteValueDecompositionGroup K w.1) ≃
      AbsoluteValueExtension vK L
theorem

rightCosetExtensionEquiv_apply

L737 ↗
LocalClassFieldTheory.rightCosetExtensionEquiv_apply
Source context 12 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section ExtensionOrbit
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
local notation "G" => L ≃ₐ[K] L
omit [FiniteDimensional K L] in
Lean source · statement
theorem rightCosetExtensionEquiv_apply
    (q : InducedRightCosets
      (absoluteValueDecompositionGroup K w.1)) :
    rightCosetExtensionEquiv vK hvK w q =
      absoluteValueExtensionConjugate
        vK w (Quotient.out q)
def

completionProductReindexRightCosets

L754 ↗
LocalClassFieldTheory.completionProductReindexRightCosets
Documentation

Reindex the product of all completion unit groups by the right cosets of the decomposition group.

Source context 10 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section ProductEquivalences
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
Lean source · statement
def completionProductReindexRightCosets :
    (∀ w' : AbsoluteValueExtension vK L, w'.1.Completionˣ) ≃*
      (∀ q : InducedRightCosets
          (absoluteValueDecompositionGroup K w.1),
        ((rightCosetExtensionEquiv vK hvK w q).1.Completion)ˣ)
def

rightCosetCompletionUnitsEquiv

L773 ↗
LocalClassFieldTheory.rightCosetCompletionUnitsEquiv
Documentation

For a right coset, conjugation by its chosen representative identifies the corresponding completion with the fixed completion at w.

Source context 10 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section ProductEquivalences
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
Lean source · statement
def rightCosetCompletionUnitsEquiv
    (q : InducedRightCosets
      (absoluteValueDecompositionGroup K w.1)) :
    ((rightCosetExtensionEquiv vK hvK w q).1.Completion)ˣ ≃*
      w.1.Completionˣ
theorem

rightCosetCompletionUnitsEquiv_apply_coe

L784 ↗
LocalClassFieldTheory.rightCosetCompletionUnitsEquiv_apply_coe
Source context 11 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section ProductEquivalences
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
omit [FiniteDimensional K L] in
Lean source · statement
theorem rightCosetCompletionUnitsEquiv_apply_coe
    (q : InducedRightCosets
      (absoluteValueDecompositionGroup K w.1))
    (z :
      ((rightCosetExtensionEquiv vK hvK w q).1.Completion)ˣ) :
    ((rightCosetCompletionUnitsEquiv vK hvK w q z :
        w.1.Completionˣ) : w.1.Completion) =
      conjugateExtensionCompletionRingEquiv
        vK w (Quotient.out q)
        (z :
          (rightCosetExtensionEquiv vK hvK w q).1.Completion)
def

completionProductUnitsEquivRightCosets

L800 ↗
LocalClassFieldTheory.completionProductUnitsEquivRightCosets
Documentation

The product supplied by the completion tensor-product decomposition, rewritten as one copy of the chosen local multiplicative group for every right coset.

Source context 10 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section ProductEquivalences
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
Lean source · full declaration
def completionProductUnitsEquivRightCosets :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    (∀ w' : AbsoluteValueExtension vK L, w'.1.Completionˣ) ≃*
      (InducedRightCosets
          (absoluteValueDecompositionGroup K w.1) →
        (LocalizedCompletion vK w)ˣ) := by
  letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  letI : SMul K w.1.Completion := hK.toSMul
  letI := AbsoluteValue.completionAlgebra vK w.1 w.2
  exact
    (completionProductReindexRightCosets vK hvK w).trans
      ((MulEquiv.piCongrRight fun q : InducedRightCosets
          (absoluteValueDecompositionGroup K w.1) =>
        rightCosetCompletionUnitsEquiv vK hvK w q).trans
        (MulEquiv.piCongrRight fun _ : InducedRightCosets
            (absoluteValueDecompositionGroup K w.1) =>
          (Units.mapEquiv
            (localizedCompletionEquivCompletion
              vK hvK w).toMulEquiv).symm))
theorem

completionProductUnitsEquivRightCosets_apply_coe

L823 ↗
LocalClassFieldTheory.completionProductUnitsEquivRightCosets_apply_coe
Source context 10 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section ProductEquivalences
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
Lean source · full declaration
theorem completionProductUnitsEquivRightCosets_apply_coe
    (p : ∀ w' : AbsoluteValueExtension vK L,
      w'.1.Completionˣ)
    (q : InducedRightCosets
      (absoluteValueDecompositionGroup K w.1)) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    ((completionProductUnitsEquivRightCosets vK hvK w p q :
        (LocalizedCompletion vK w)ˣ) :
      LocalizedCompletion vK w) =
      (localizedCompletionEquivCompletion vK hvK w).symm
        (conjugateExtensionCompletionRingEquiv
          vK w (Quotient.out q)
          ((p (rightCosetExtensionEquiv vK hvK w q) :
              (rightCosetExtensionEquiv vK hvK w q).1.Completionˣ) :
            (rightCosetExtensionEquiv vK hvK w q).1.Completion)) := by
  rfl
def

completionProductUnitsEquivLocalPlaceBlock

L845 ↗
LocalClassFieldTheory.completionProductUnitsEquivLocalPlaceBlock
Documentation

The product of completions above v is the induced block from the decomposition group. This form is valid for an arbitrary finite Galois extension; the decomposition group need not be normal.

Source context 10 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section ProductEquivalences
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
Lean source · full declaration
def completionProductUnitsEquivLocalPlaceBlock :
    letI :=
      decompositionGroupLocalUnitsAction vK hvK w
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    (∀ w' : AbsoluteValueExtension vK L, w'.1.Completionˣ) ≃*
      LocalPlaceBlock vK hvK w := by
  letI :=
    decompositionGroupLocalUnitsAction vK hvK w
  letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  letI : SMul K w.1.Completion := hK.toSMul
  letI := AbsoluteValue.completionAlgebra vK w.1 w.2
  exact
    (completionProductUnitsEquivRightCosets vK hvK w).trans
      (inducedRightCosetCoordinates
        (absoluteValueDecompositionGroup K w.1)).symm
def

localTensorUnitsEquivLocalPlaceBlock

L866 ↗
LocalClassFieldTheory.localTensorUnitsEquivLocalPlaceBlock
Documentation

Concrete tensor realization of the induced local block: the actual local unit group (K_v ⊗[K] L)ˣ is multiplicatively equivalent to the induced block from the decomposition group at a chosen extension w.

Source context 10 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section ProductEquivalences
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
Lean source · full declaration
def localTensorUnitsEquivLocalPlaceBlock :
    letI :=
      decompositionGroupLocalUnitsAction vK hvK w
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    letI : ∀ w' : AbsoluteValueExtension vK L,
        Algebra vK.Completion w'.1.Completion :=
      fun w' ↦ AbsoluteValue.completionAlgebra vK w'.1 w'.2
    (LocalTensorAlgebra (L := L) vK)ˣ ≃*
      LocalPlaceBlock vK hvK w := by
  letI :=
    decompositionGroupLocalUnitsAction vK hvK w
  letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  letI : SMul K w.1.Completion := hK.toSMul
  letI := AbsoluteValue.completionAlgebra vK w.1 w.2
  letI : ∀ w' : AbsoluteValueExtension vK L,
      Algebra vK.Completion w'.1.Completion :=
    fun w' ↦ AbsoluteValue.completionAlgebra vK w'.1 w'.2
  exact
    (localTensorUnitsEquivCompletionProduct vK hvK).trans
      (completionProductUnitsEquivLocalPlaceBlock vK hvK w)
theorem

localTensorUnitsEquivLocalPlaceBlock_apply_out_coe

L891 ↗
LocalClassFieldTheory.localTensorUnitsEquivLocalPlaceBlock_apply_out_coe
Documentation

On the chosen representative of a right coset, the concrete The tensor-product equivalence is the canonical orbit-evaluation map.

Source context 10 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section ProductEquivalences
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
Lean source · full declaration
theorem localTensorUnitsEquivLocalPlaceBlock_apply_out_coe
    (z : (LocalTensorAlgebra (L := L) vK)ˣ)
    (q : InducedRightCosets
      (absoluteValueDecompositionGroup K w.1)) :
    letI :=
      decompositionGroupLocalUnitsAction vK hvK w
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    letI : ∀ w' : AbsoluteValueExtension vK L,
        Algebra vK.Completion w'.1.Completion :=
      fun w' ↦ AbsoluteValue.completionAlgebra vK w'.1 w'.2
    (((localTensorUnitsEquivLocalPlaceBlock vK hvK w z).1
        (Quotient.out q) :
          (LocalizedCompletion vK w)ˣ) :
      LocalizedCompletion vK w) =
      localTensorEvaluation vK hvK w
        (localTensorConjugation vK (Quotient.out q)
          (z : LocalTensorAlgebra (L := L) vK)) := by
  let _ :=
    decompositionGroupLocalUnitsAction vK hvK w
  let hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  let _ : SMul K w.1.Completion := hK.toSMul
  let _ := AbsoluteValue.completionAlgebra vK w.1 w.2
  let _ : ∀ w' : AbsoluteValueExtension vK L,
      Algebra vK.Completion w'.1.Completion :=
    fun w' ↦ AbsoluteValue.completionAlgebra vK w'.1 w'.2
  have hcoord :
      inducedRightCosetCoordinates
          (absoluteValueDecompositionGroup K w.1)
          (localTensorUnitsEquivLocalPlaceBlock vK hvK w z) q =
        completionProductUnitsEquivRightCosets vK hvK w
          (localTensorUnitsEquivCompletionProduct vK hvK z) q := by
    change
      inducedRightCosetCoordinates
          (absoluteValueDecompositionGroup K w.1)
          ((inducedRightCosetCoordinates
            (absoluteValueDecompositionGroup K w.1)).symm
            (completionProductUnitsEquivRightCosets vK hvK w
              (localTensorUnitsEquivCompletionProduct vK hvK z))) q =
        completionProductUnitsEquivRightCosets vK hvK w
          (localTensorUnitsEquivCompletionProduct vK hvK z) q
    rw [MulEquiv.apply_symm_apply]
  have hval := congrArg
    (fun u : (LocalizedCompletion vK w)ˣ =>
      (u : LocalizedCompletion vK w)) hcoord
  change
    (((localTensorUnitsEquivLocalPlaceBlock vK hvK w z).1
        (Quotient.out q) :
          (LocalizedCompletion vK w)ˣ) :
      LocalizedCompletion vK w) =
      ((completionProductUnitsEquivRightCosets vK hvK w
          (localTensorUnitsEquivCompletionProduct vK hvK z) q :
            (LocalizedCompletion vK w)ˣ) :
        LocalizedCompletion vK w) at hval
  rw [hval,
    completionProductUnitsEquivRightCosets_apply_coe,
    localTensorUnitsEquivCompletionProduct_apply_coe]
  change
    (localizedCompletionEquivCompletion vK hvK w).symm
        (conjugateExtensionCompletionRingEquiv
          vK w (Quotient.out q)
          (completionTensorDecomposition_left (K := K) (L := L) vK hvK
            (z : LocalTensorAlgebra (L := L) vK)
            (absoluteValueExtensionConjugate
              vK w (Quotient.out q)))) =
      localTensorEvaluation vK hvK w
        (localTensorConjugation vK (Quotient.out q)
          (z : LocalTensorAlgebra (L := L) vK))
  rw [conjugateExtensionCompletionRingEquiv_completionTensorDecomposition_left]
  rfl
theorem

localTensorUnitsEquivLocalPlaceBlock_eq_orbitHom_apply

L965 ↗
LocalClassFieldTheory.localTensorUnitsEquivLocalPlaceBlock_eq_orbitHom_apply
Documentation

The multiplicative equivalence obtained from the tensor-product decomposition is literally the canonical orbit-evaluation homomorphism.

Source context 10 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section ProductEquivalences
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
Lean source · full declaration
theorem localTensorUnitsEquivLocalPlaceBlock_eq_orbitHom_apply
    (z : (LocalTensorAlgebra (L := L) vK)ˣ) :
    letI :=
      decompositionGroupLocalUnitsAction vK hvK w
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    letI : ∀ w' : AbsoluteValueExtension vK L,
        Algebra vK.Completion w'.1.Completion :=
      fun w' ↦ AbsoluteValue.completionAlgebra vK w'.1 w'.2
    localTensorUnitsEquivLocalPlaceBlock vK hvK w z =
      localTensorOrbitHom vK hvK w z := by
  let _ :=
    decompositionGroupLocalUnitsAction vK hvK w
  let hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  let _ : SMul K w.1.Completion := hK.toSMul
  let _ := AbsoluteValue.completionAlgebra vK w.1 w.2
  let _ : ∀ w' : AbsoluteValueExtension vK L,
      Algebra vK.Completion w'.1.Completion :=
    fun w' ↦ AbsoluteValue.completionAlgebra vK w'.1 w'.2
  apply
    (inducedRightCosetCoordinates
      (absoluteValueDecompositionGroup K w.1)).injective
  funext q
  apply Units.ext
  change
    (((localTensorUnitsEquivLocalPlaceBlock vK hvK w z).1
        (Quotient.out q) :
          (LocalizedCompletion vK w)ˣ) :
      LocalizedCompletion vK w) =
      localTensorEvaluation vK hvK w
        (localTensorConjugation vK (Quotient.out q)
          (z : LocalTensorAlgebra (L := L) vK))
  exact
    localTensorUnitsEquivLocalPlaceBlock_apply_out_coe
      vK hvK w z q
theorem

localTensorUnitsEquivLocalPlaceBlock_smul

L1005 ↗
LocalClassFieldTheory.localTensorUnitsEquivLocalPlaceBlock_smul
Documentation

Equivariant concrete form: the actual tensor local factor and the induced local block are equivalent compatibly with the full Galois action.

Source context 10 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section ProductEquivalences
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
Lean source · full declaration
theorem localTensorUnitsEquivLocalPlaceBlock_smul
    (τ : L ≃ₐ[K] L)
    (z : (LocalTensorAlgebra (L := L) vK)ˣ) :
    letI :=
      decompositionGroupLocalUnitsAction vK hvK w
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    letI : ∀ w' : AbsoluteValueExtension vK L,
        Algebra vK.Completion w'.1.Completion :=
      fun w' ↦ AbsoluteValue.completionAlgebra vK w'.1 w'.2
    letI := localTensorUnitsAction (K := K) (L := L) vK
    localTensorUnitsEquivLocalPlaceBlock vK hvK w (τ • z) =
      τ • localTensorUnitsEquivLocalPlaceBlock vK hvK w z := by
  let _ :=
    decompositionGroupLocalUnitsAction vK hvK w
  let hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  let _ : SMul K w.1.Completion := hK.toSMul
  let _ := AbsoluteValue.completionAlgebra vK w.1 w.2
  let _ : ∀ w' : AbsoluteValueExtension vK L,
      Algebra vK.Completion w'.1.Completion :=
    fun w' ↦ AbsoluteValue.completionAlgebra vK w'.1 w'.2
  let _ := localTensorUnitsAction (K := K) (L := L) vK
  rw [localTensorUnitsEquivLocalPlaceBlock_eq_orbitHom_apply,
    localTensorUnitsEquivLocalPlaceBlock_eq_orbitHom_apply]
  exact localTensorOrbitHom_smul vK hvK w τ z
theorem

localTensorUnitsEquivLocalPlaceBlock_symm_smul

L1033 ↗
LocalClassFieldTheory.localTensorUnitsEquivLocalPlaceBlock_symm_smul
Documentation

The inverse of the induced local-block equivalence is equivariant as well.

Source context 10 commands

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

open scoped TensorProduct
noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
universe u v
variable {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    [IsGalois K L]
section ProductEquivalences
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
Lean source · full declaration
theorem localTensorUnitsEquivLocalPlaceBlock_symm_smul
    (τ : L ≃ₐ[K] L)
    (f : LocalPlaceBlock vK hvK w) :
    letI :=
      decompositionGroupLocalUnitsAction vK hvK w
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    letI : ∀ w' : AbsoluteValueExtension vK L,
        Algebra vK.Completion w'.1.Completion :=
      fun w' ↦ AbsoluteValue.completionAlgebra vK w'.1 w'.2
    letI := localTensorUnitsAction (K := K) (L := L) vK
    (localTensorUnitsEquivLocalPlaceBlock vK hvK w).symm
        (τ • f) =
      τ •
        (localTensorUnitsEquivLocalPlaceBlock vK hvK w).symm f := by
  let _ :=
    decompositionGroupLocalUnitsAction vK hvK w
  let hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  let _ : SMul K w.1.Completion := hK.toSMul
  let _ := AbsoluteValue.completionAlgebra vK w.1 w.2
  let _ : ∀ w' : AbsoluteValueExtension vK L,
      Algebra vK.Completion w'.1.Completion :=
    fun w' ↦ AbsoluteValue.completionAlgebra vK w'.1 w'.2
  let _ := localTensorUnitsAction (K := K) (L := L) vK
  apply
    (localTensorUnitsEquivLocalPlaceBlock
      vK hvK w).injective
  rw [MulEquiv.apply_symm_apply,
    localTensorUnitsEquivLocalPlaceBlock_smul,
    MulEquiv.apply_symm_apply]

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