ConcreteReciprocityCanonical.lean

abbrev G (K : Type) [Field K]

abbrev AG (K : Type) [Field K] : Rep ℤ (G K)

abbrev B (K : Type) [Field K] : ClosedSubgroup (G K)

def finiteGaloisEmbeddingConjugator
    (i j : L →ₐ[K] SeparableClosure K) : G K

theorem finiteGaloisEmbeddingConjugator_apply
    (i j : L →ₐ[K] SeparableClosure K) (x : L) :
    finiteGaloisEmbeddingConjugator K L i j (i x) = j x

theorem finiteGaloisEmbeddingConjugator_comp
    (i j : L →ₐ[K] SeparableClosure K) :
    (finiteGaloisEmbeddingConjugator K L i j).toAlgHom.comp i = j

theorem finiteGaloisFieldRange_conjugator
    (i j : L →ₐ[K] SeparableClosure K) :
    finiteGaloisFieldRangeOfEmbedding K L j =
      (finiteGaloisFieldRangeOfEmbedding K L i).map
        (finiteGaloisEmbeddingConjugator K L i j).toAlgHom

theorem finiteGaloisClosedFixingSubgroup_conjugator
    (i j : L →ₐ[K] SeparableClosure K) :
    conjugateClosedSubgroup
        (finiteGaloisClosedFixingSubgroupOfEmbedding K L i)
        (finiteGaloisEmbeddingConjugator K L i j)⁻¹ =
      finiteGaloisClosedFixingSubgroupOfEmbedding K L j

theorem finiteGaloisBase_conjugator
    (σ : G K) : conjugateClosedSubgroup (B K) σ = B K

instance
    finiteGaloisAbstractExtensionOfEmbedding_bundle_finite
    (i : L →ₐ[K] SeparableClosure K) :
    Finite ((B K).toSubgroup ⧸
      extensionSubgroup (B K)
        (finiteGaloisAbstractExtensionOfEmbedding K L i).field
        (finiteGaloisAbstractExtensionOfEmbedding K L i).below)

instance finiteGaloisExtensionQuotientOfEmbedding_finite
    (i : L →ₐ[K] SeparableClosure K) :
    Finite ((B K).toSubgroup ⧸
      extensionSubgroup (B K)
        (finiteGaloisClosedFixingSubgroupOfEmbedding K L i)
        (fixingSubgroupLeBase K (SeparableClosure K)
          (finiteGaloisFieldRangeOfEmbedding K L i)))

def finiteGaloisConjugateBaseElement
    (i j : L →ₐ[K] SeparableClosure K) (τ : (B K).toSubgroup) :
    (B K).toSubgroup

def extensionQuotientCongr
    {Γ : Type} [Group Γ] [TopologicalSpace Γ]
    {K L K' L' : ClosedSubgroup Γ}
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ K'.toSubgroup)
    [hN : (extensionSubgroup K L hLK).Normal]
    [hN' : (extensionSubgroup K' L' hL'K').Normal]
    (hK : K = K') (hL : L = L') :
    (K.toSubgroup ⧸ extensionSubgroup K L hLK) ≃*
      (K'.toSubgroup ⧸ extensionSubgroup K' L' hL'K')

theorem extensionQuotientCongr_mk
    {Γ : Type} [Group Γ] [TopologicalSpace Γ]
    {K L K' L' : ClosedSubgroup Γ}
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ K'.toSubgroup)
    [hN : (extensionSubgroup K L hLK).Normal]
    [hN' : (extensionSubgroup K' L' hL'K').Normal]
    (hK : K = K') (hL : L = L') (x : K.toSubgroup) :
    extensionQuotientCongr hLK hL'K' hK hL (QuotientGroup.mk x) =
      QuotientGroup.mk
        (MulEquiv.subgroupCongr
          (congrArg (fun H : ClosedSubgroup Γ => H.toSubgroup) hK) x) := by
  subst K'
  subst L'
  have hp : hLK = hL'K' := Subsingleton.elim _ _
  subst hL'K'
  have hn : hN = hN' := Subsingleton.elim _ _
  subst hN'
  rfl

def finiteNormQuotientCongr
    {Γ : Type} [Group Γ] [TopologicalSpace Γ]
    (A : Rep ℤ Γ) {K L K' L' : ClosedSubgroup Γ}
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ K'.toSubgroup)
    [hFinite : Finite (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    [hFinite' : Finite (K'.toSubgroup ⧸ extensionSubgroup K' L' hL'K')]
    (hK : K = K') (hL : L = L') :
    FiniteNormQuotient A K L hLK ≃+
      FiniteNormQuotient A K' L' hL'K'

theorem finiteNormQuotientCongr_finiteNormClass
    {Γ : Type} [Group Γ] [TopologicalSpace Γ]
    (A : Rep ℤ Γ) {K L K' L' : ClosedSubgroup Γ}
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ K'.toSubgroup)
    [hFinite : Finite (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    [hFinite' : Finite (K'.toSubgroup ⧸ extensionSubgroup K' L' hL'K')]
    (hK : K = K') (hL : L = L')
    (a : ambientFixedAddSubgroup A K) :
    finiteNormQuotientCongr A hLK hL'K' hK hL
        (finiteNormClass A K L hLK a) =
      finiteNormClass A K' L' hL'K'
        (AddEquiv.addSubgroupCongr
          (congrArg (ambientFixedAddSubgroup A) hK) a)

theorem normResidueSymbol_congr
    {Γ : Type} [Group Γ] [TopologicalSpace Γ]
    (D : DegreeData Γ) (A : Rep ℤ Γ) (v : ValuationData D A)
    (hcf : SatisfiesClassFieldAxiom A)
    [IsTopologicalGroup Γ] [CompactSpace Γ] [T2Space Γ]
    [TotallyDisconnectedSpace Γ]
    (K L K' L' : ClosedSubgroup Γ)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ K'.toSubgroup)
    [hNormal : (extensionSubgroup K L hLK).Normal]
    [hNormal' : (extensionSubgroup K' L' hL'K').Normal]
    [hFinite : Finite (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    [hFinite' : Finite (K'.toSubgroup ⧸ extensionSubgroup K' L' hL'K')]
    [hAbsolute : Finite ((baseField Γ).toSubgroup ⧸
      extensionSubgroup (baseField Γ) K (le_baseField K))]
    [hAbsolute' : Finite ((baseField Γ).toSubgroup ⧸
      extensionSubgroup (baseField Γ) K' (le_baseField K'))]
    (hK : K = K') (hL : L = L') :
    let E : FiniteGaloisSubextension K :=
      ⟨L, hLK, hNormal, hFinite⟩
    let E' : FiniteGaloisSubextension K' :=
      ⟨L', hL'K', hNormal', hFinite'⟩
    let KF : FiniteAbstractField Γ := ⟨K, hAbsolute⟩
    let K'F : FiniteAbstractField Γ := ⟨K', hAbsolute'⟩
    let q := MulEquiv.toAdditive
      ((extensionQuotientCongr hLK hL'K' hK hL).abelianizationCongr)
    let b := finiteNormQuotientCongr A
      (hFinite := hFinite) (hFinite' := hFinite')
      hLK hL'K' hK hL
    q.toAddMonoidHom.comp
        (D.normResidueSymbol A v hcf KF E).toAddMonoidHom =
      (D.normResidueSymbol A v hcf K'F E').toAddMonoidHom.comp
        b.toAddMonoidHom := by
  subst K'
  subst L'
  have hp : hLK = hL'K' := Subsingleton.elim _ _
  subst hL'K'
  have hn : hNormal = hNormal' := Subsingleton.elim _ _
  subst hNormal'
  have hf : hFinite = hFinite' := Subsingleton.elim _ _
  subst hFinite'
  have ha : hAbsolute = hAbsolute' := Subsingleton.elim _ _
  subst hAbsolute'
  dsimp only [extensionQuotientCongr, finiteNormQuotientCongr]
  apply AddMonoidHom.ext
  intro x
  rw [abelianizationCongr_refl]
  rfl

theorem finiteGaloisEmbeddingConjugate_normal
    (i : L →ₐ[K] SeparableClosure K) (s : G K) :
    (extensionSubgroup (conjugateClosedSubgroup (B K) s)
      (conjugateClosedSubgroup
        (finiteGaloisClosedFixingSubgroupOfEmbedding K L i) s)
      (conjugateClosedSubgroup_mono
        (fixingSubgroupLeBase K (SeparableClosure K)
          (finiteGaloisFieldRangeOfEmbedding K L i)) s)).Normal

def finiteGaloisConjugationOfEmbeddings
    (i j : L →ₐ[K] SeparableClosure K) :
    (finiteGaloisAbstractExtensionOfEmbedding K L i).extensionQuotient ≃*
      (finiteGaloisAbstractExtensionOfEmbedding K L j).extensionQuotient

theorem finiteGaloisConjugationOfEmbeddings_mk
    (i j : L →ₐ[K] SeparableClosure K) (τ : (B K).toSubgroup) :
    finiteGaloisConjugationOfEmbeddings K L i j (QuotientGroup.mk τ) =
      QuotientGroup.mk (finiteGaloisConjugateBaseElement K L i j τ)

theorem finiteGaloisConjugationOfEmbeddings_apply_factor
    (i j : L →ₐ[K] SeparableClosure K)
    (z : (finiteGaloisAbstractExtensionOfEmbedding K L i).extensionQuotient) :
    let hLK := fixingSubgroupLeBase K (SeparableClosure K)
      (finiteGaloisFieldRangeOfEmbedding K L i)
    let s := (finiteGaloisEmbeddingConjugator K L i j)⁻¹
    let hB := finiteGaloisBase_conjugator K s
    let hH := finiteGaloisClosedFixingSubgroup_conjugator K L i j
    finiteGaloisConjugationOfEmbeddings K L i j z =
      extensionQuotientCongr
        (conjugateClosedSubgroup_mono hLK s)
        (fixingSubgroupLeBase K (SeparableClosure K)
          (finiteGaloisFieldRangeOfEmbedding K L j)) hB hH
        (finiteReciprocityNaturalityConjugation (B K)
          (finiteGaloisClosedFixingSubgroupOfEmbedding K L i) hLK s z) := by
  dsimp only
  unfold finiteGaloisConjugationOfEmbeddings
  rfl

theorem finiteGaloisConjugationOfEmbeddings_abelianization_factor
    (i j : L →ₐ[K] SeparableClosure K)
    (z : Abelianization
      (finiteGaloisAbstractExtensionOfEmbedding K L i).extensionQuotient) :
    let hLK := fixingSubgroupLeBase K (SeparableClosure K)
      (finiteGaloisFieldRangeOfEmbedding K L i)
    let s := (finiteGaloisEmbeddingConjugator K L i j)⁻¹
    let hB := finiteGaloisBase_conjugator K s
    let hH := finiteGaloisClosedFixingSubgroup_conjugator K L i j
    (finiteGaloisConjugationOfEmbeddings K L i j).abelianizationCongr z =
      (extensionQuotientCongr
        (conjugateClosedSubgroup_mono hLK s)
        (fixingSubgroupLeBase K (SeparableClosure K)
          (finiteGaloisFieldRangeOfEmbedding K L j)) hB hH).abelianizationCongr
        ((finiteReciprocityNaturalityConjugation (B K)
          (finiteGaloisClosedFixingSubgroupOfEmbedding K L i)
          hLK s).abelianizationCongr z) := by
  dsimp only
  let hLK : (finiteGaloisClosedFixingSubgroupOfEmbedding K L i).toSubgroup ≤
      (B K).toSubgroup :=
    fixingSubgroupLeBase K (SeparableClosure K)
      (finiteGaloisFieldRangeOfEmbedding K L i)
  let hLjK : (finiteGaloisClosedFixingSubgroupOfEmbedding K L j).toSubgroup ≤
      (B K).toSubgroup :=
    fixingSubgroupLeBase K (SeparableClosure K)
      (finiteGaloisFieldRangeOfEmbedding K L j)
  let s := (finiteGaloisEmbeddingConjugator K L i j)⁻¹
  let e := finiteReciprocityNaturalityConjugation (B K)
    (finiteGaloisClosedFixingSubgroupOfEmbedding K L i) hLK s
  let c := extensionQuotientCongr
    (K := conjugateClosedSubgroup (B K) s)
    (L := conjugateClosedSubgroup
      (finiteGaloisClosedFixingSubgroupOfEmbedding K L i) s)
    (K' := B K) (L' := finiteGaloisClosedFixingSubgroupOfEmbedding K L j)
    (conjugateClosedSubgroup_mono hLK s) hLjK
    (finiteGaloisBase_conjugator K s)
    (finiteGaloisClosedFixingSubgroup_conjugator K L i j)
  refine QuotientGroup.induction_on z ?_
  intro x
  change
    (finiteGaloisConjugationOfEmbeddings K L i j).abelianizationCongr
        (Abelianization.of x) =
      c.abelianizationCongr (e.abelianizationCongr (Abelianization.of x))
  exact (abelianizationCongr_of
      (finiteGaloisConjugationOfEmbeddings K L i j) x).trans
    ((congrArg Abelianization.of
      (finiteGaloisConjugationOfEmbeddings_apply_factor K L i j x)).trans
      ((abelianizationCongr_of c (e x)).symm.trans
        (congrArg c.abelianizationCongr (abelianizationCongr_of e x).symm)))

def finiteGaloisEmbeddingNormAddZeroClass
    (i : L →ₐ[K] SeparableClosure K)

def finiteGaloisNormConjugationOfEmbeddings
    (i j : L →ₐ[K] SeparableClosure K) :
    FiniteNormQuotient (AG K) (B K)
        (finiteGaloisAbstractExtensionOfEmbedding K L i).field
        (finiteGaloisAbstractExtensionOfEmbedding K L i).below →+
      FiniteNormQuotient (AG K) (B K)
        (finiteGaloisAbstractExtensionOfEmbedding K L j).field
        (finiteGaloisAbstractExtensionOfEmbedding K L j).below

theorem finiteGaloisNormConjugationOfEmbeddings_apply_factor
    (i j : L →ₐ[K] SeparableClosure K)
    (a : FiniteNormQuotient (AG K) (B K)
      (finiteGaloisAbstractExtensionOfEmbedding K L i).field
      (finiteGaloisAbstractExtensionOfEmbedding K L i).below) :
    let hLK := fixingSubgroupLeBase K (SeparableClosure K)
      (finiteGaloisFieldRangeOfEmbedding K L i)
    let s := (finiteGaloisEmbeddingConjugator K L i j)⁻¹
    let hB := finiteGaloisBase_conjugator K s
    let hH := finiteGaloisClosedFixingSubgroup_conjugator K L i j
    finiteGaloisNormConjugationOfEmbeddings K L i j a =
      finiteNormQuotientCongr (AG K)
        (hFinite := finite_conjugateExtension (B K)
          (finiteGaloisClosedFixingSubgroupOfEmbedding K L i) hLK s)
        (hFinite' := finiteGaloisExtensionQuotientOfEmbedding_finite K L j)
        (conjugateClosedSubgroup_mono hLK s)
        (fixingSubgroupLeBase K (SeparableClosure K)
          (finiteGaloisFieldRangeOfEmbedding K L j)) hB hH
        (finiteReciprocityNaturalityConjugationNormMap (AG K) (B K)
          (finiteGaloisClosedFixingSubgroupOfEmbedding K L i) hLK s a) := by
  dsimp only
  unfold finiteGaloisNormConjugationOfEmbeddings
  rfl

theorem baseFixingExtensionQuotientEquivGaloisGroup_mk_apply
    (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω] [IsGalois K Ω]
    (E : IntermediateField K Ω) [FiniteDimensional K E] [IsGalois K E]
    (τ : (closedFixingSubgroup K Ω
      (⊥ : IntermediateField K Ω)).toSubgroup) (x : E) :
    E.val ((baseFixingExtensionQuotientEquivGaloisGroup K Ω E
      (QuotientGroup.mk τ)) x) = τ.1 (E.val x)

theorem finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding_mk_apply
    (i : L →ₐ[K] SeparableClosure K) (τ : (B K).toSubgroup) (x : L) :
    i ((finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding K L i
      (QuotientGroup.mk τ)) x) = τ.1 (i x)

theorem finiteNormQuotientEquivEmbeddedNormQuotient_finiteNormClass_baseUnit
    (i : L →ₐ[K] SeparableClosure K) (x : Kˣ) :
    finiteNormQuotientEquivEmbeddedNormQuotient
        K (SeparableClosure K) L i
        (finiteNormClass (AG K) (B K)
          (finiteGaloisClosedFixingSubgroupOfEmbedding K L i)
          (fixingSubgroupLeBase K (SeparableClosure K)
            (finiteGaloisFieldRangeOfEmbedding K L i))
          (baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)
            (Additive.ofMul x))) =
      (MonoidHom.toAdditive (normClass K L))
        (Additive.ofMul x)

theorem finiteGaloisNormConjugationOfEmbeddings_finiteNormClass_baseUnit
    (i j : L →ₐ[K] SeparableClosure K) (x : Kˣ) :
    finiteGaloisNormConjugationOfEmbeddings K L i j
        (finiteNormClass (AG K) (B K)
          (finiteGaloisClosedFixingSubgroupOfEmbedding K L i)
          (fixingSubgroupLeBase K (SeparableClosure K)
            (finiteGaloisFieldRangeOfEmbedding K L i))
          (baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)
            (Additive.ofMul x))) =
      finiteNormClass (AG K) (B K)
        (finiteGaloisClosedFixingSubgroupOfEmbedding K L j)
        (fixingSubgroupLeBase K (SeparableClosure K)
          (finiteGaloisFieldRangeOfEmbedding K L j))
        (baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)
          (Additive.ofMul x))

theorem finiteGaloisAbstractQuotientEquivGaloisGroup_conjugation
    (i j : L →ₐ[K] SeparableClosure K)
    (z : Abelianization
      (finiteGaloisAbstractExtensionOfEmbedding K L i).extensionQuotient) :
    (finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding K L j).abelianizationCongr
        ((finiteGaloisConjugationOfEmbeddings K L i j).abelianizationCongr z) =
      (finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding K L i).abelianizationCongr z

theorem finiteGaloisAbstractQuotientEquivGaloisGroup_conjugation_additive
    (i j : L →ₐ[K] SeparableClosure K)
    (z : Additive (Abelianization
      (finiteGaloisAbstractExtensionOfEmbedding K L i).extensionQuotient)) :
    MulEquiv.toAdditive
        ((finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding K L j).abelianizationCongr)
        (MulEquiv.toAdditive
          ((finiteGaloisConjugationOfEmbeddings K L i j).abelianizationCongr) z) =
      MulEquiv.toAdditive
        ((finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding K L i).abelianizationCongr)
          z

theorem finiteNormQuotientEquivEmbeddedNormQuotient_conjugation
    (i j : L →ₐ[K] SeparableClosure K)
    (a : FiniteNormQuotient (AG K) (B K)
      (finiteGaloisAbstractExtensionOfEmbedding K L i).field
      (finiteGaloisAbstractExtensionOfEmbedding K L i).below) :
    finiteNormQuotientEquivEmbeddedNormQuotient
        K (SeparableClosure K) L j
        (finiteGaloisNormConjugationOfEmbeddings K L i j a) =
      finiteNormQuotientEquivEmbeddedNormQuotient
        K (SeparableClosure K) L i a

theorem reciprocityTransport_pointwise
    {A B C D E F : Type}
    (q : A → B) (b : C → D)
    (ri : A ≃ C) (rj : B ≃ D)
    (ni : C → E) (nj : D → E)
    (si : A ≃ F) (sj : B ≃ F)
    (hsource : ∀ z, sj (q z) = si z)
    (hnorm : ∀ a, nj (b a) = ni a)
    (hforward : ∀ z, b (ri z) = rj (q z))
    (x : F) :
    ni (ri (si.symm x)) = nj (rj (sj.symm x))

theorem concreteReciprocityAddEquivOfEmbedding_eq
    (i j : L →ₐ[K] SeparableClosure K)
    (D : DegreeData (G K)) (v : ValuationData D (AG K))
    (hcf : SatisfiesClassFieldAxiom (AG K)) :
    concreteReciprocityAddEquivOfEmbedding K L i D v hcf =
      concreteReciprocityAddEquivOfEmbedding K L j D v hcf

theorem concreteReciprocityEquivOfEmbedding_eq
    (i j : L →ₐ[K] SeparableClosure K)
    (D : DegreeData (G K)) (v : ValuationData D (AG K))
    (hcf : SatisfiesClassFieldAxiom (AG K)) :
    concreteReciprocityEquivOfEmbedding K L i D v hcf =
      concreteReciprocityEquivOfEmbedding K L j D v hcf

theorem concreteNormResidueSymbolOfEmbedding_eq
    (i j : L →ₐ[K] SeparableClosure K)
    (D : DegreeData (G K)) (v : ValuationData D (AG K))
    (hcf : SatisfiesClassFieldAxiom (AG K)) :
    concreteNormResidueSymbolOfEmbedding K L i D v hcf =
      concreteNormResidueSymbolOfEmbedding K L j D v hcf