Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FiniteAbelianFamilySubgroupKernel

Module documentation

Subgroup data of coherent finite local reciprocity families

At a fixed finite abelian stage, every Galois subgroup is the fixing subgroup of an intermediate field. Transporting that field into the chosen separable closure lets the common norm-kernel and tower conditions compare two Artin families on every Galois subgroup.

theorem

finiteAbelianArtinFamilies_subgroup_preimage_le

L30 ↗

LocalClassFieldTheory.finiteAbelianArtinFamilies_subgroup_preimage_le

Documentation

If two coherent families have the same norm kernels, membership in any Galois subgroup for one family implies membership for the other. Applying the result with the two families swapped gives equality of preimages.

Source context 3 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFieldTheory

Lean source · statement

theorem finiteAbelianArtinFamilies_subgroup_preimage_le
    (K : Type) [Field K] [TopologicalSpace K]
    (f g : (E : FiniteAbelianLocalExtension K) →
      Kˣ →ₜ* (E.1 ≃ₐ[K] E.1))
    (hfker : ∀ E : FiniteAbelianLocalExtension K,
      (f E).toMonoidHom.ker = E.normSubgroup)
    (hgker : ∀ E : FiniteAbelianLocalExtension K,
      (g E).toMonoidHom.ker = E.normSubgroup)
    (hfcoh : ∀ (E F : FiniteAbelianLocalExtension K)
      (hEF : E.1 ≤ F.1) (x : Kˣ) (y : E.1),
      IntermediateField.inclusion hEF ((f E x) y) =
        (f F x) (IntermediateField.inclusion hEF y))
    (hgcoh : ∀ (E F : FiniteAbelianLocalExtension K)
      (hEF : E.1 ≤ F.1) (x : Kˣ) (y : E.1),
      IntermediateField.inclusion hEF ((g E x) y) =
        (g F x) (IntermediateField.inclusion hEF y))
    (F : FiniteAbelianLocalExtension K)
    (S : Subgroup (F.1 ≃ₐ[K] F.1)) (x : Kˣ) :
    f F x ∈ S → g F x ∈ S

Module documentation

Subgroup data of coherent finite local reciprocity families

Declarations

finiteAbelianArtinFamilies_subgroup_preimage_le