NYLL
Module

IntrinsicFrobeniusQuotientTransport.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FixedFieldIntrinsicReciprocity.IntrinsicFrobeniusQuotientTransport
12 declarations indexed from sourceView source ↗

Module documentation

Intrinsic Frobenius quotient transport

This module constructs the intrinsic-to-ambient quotient transport and maps Frobenius elements before the closure comparisons.

Imports2
Imported by3

Declarations

def

intrinsicBaseContinuousEquivAmbientFixedField

L28 ↗
LocalClassFieldTheory.intrinsicBaseContinuousEquivAmbientFixedField
Documentation

The chosen equivalence of separable closures induces a continuous multiplicative equivalence from the intrinsic absolute-base subgroup of the finite fixed field to its ambient fixed subgroup.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
Lean source · statement
def
    intrinsicBaseContinuousEquivAmbientFixedField
    (K : Type) [Field K]
    (H : FiniteAbstractField
      Gal(SeparableClosure K/K))
    (e : intrinsicFixedFieldSeparableClosureEquiv K H) :
    (intrinsicAbstractBase
      (abstractFixedField K (SeparableClosure K) H.field)).toSubgroup ≃ₜ*
      H.field.toSubgroup
def

intrinsicFrobeniusQuotientContinuousEquivAmbientFixedField

L54 ↗
LocalClassFieldTheory.intrinsicFrobeniusQuotientContinuousEquivAmbientFixedField
Documentation

Descend the continuous intrinsic-to-ambient base equivalence to the quotients by the corresponding extension-inertia subgroups.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
Lean source · full declaration
def
    intrinsicFrobeniusQuotientContinuousEquivAmbientFixedField
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (H : FiniteAbstractField
      Gal(SeparableClosure K/K))
    (J : ClosedSubgroup Gal(SeparableClosure K/K))
    (hJH : J.toSubgroup ≤ H.field.toSubgroup)
    [hJnormal : (extensionSubgroup H.field J hJH).Normal]
    [hJfinite : Finite
      (H.field.toSubgroup ⧸ extensionSubgroup H.field J hJH)] :
    let F := abstractFixedField K (SeparableClosure K) H.field
    letI : Algebra F (SeparableClosure F) :=
      (separableClosure F (AlgebraicClosure F)).algebra
    ∀ (e : SeparableClosure F ≃ₐ[F] SeparableClosure K),
    let E := abstractRelativeFixedField K (SeparableClosure K) hJH
    letI : FiniteDimensional K F :=
      abstractFixedField_finiteDimensional
        K (SeparableClosure K) H.field H.finite
    letI : NontriviallyNormedField F :=
      finiteExtensionSpectralNormedField K F
    letI : ValuativeRel F :=
      finiteExtensionSpectralValuativeRel K F
    letI : IsNonarchimedeanLocalField F :=
      finiteExtensionSpectralIsNonarchimedeanLocalField K F
    letI : FiniteDimensional F E :=
      abstractRelativeFixedField_finiteDimensional
        K (SeparableClosure K) H.field J hJH H.finite hJfinite
    letI : IsGalois F E :=
      abstractRelativeFixedField_isGalois
        K (SeparableClosure K) H.field J hJH hJnormal
    let i : E →ₐ[F] SeparableClosure F :=
      e.symm.toAlgHom.comp E.val
    let EI := finiteGaloisAbstractExtensionOfEmbedding F E i
    ((intrinsicAbstractBase F).toSubgroup ⧸
        (localResidueDatum F).extensionInertiaWithin
          (intrinsicAbstractBase F) EI.field EI.below) ≃ₜ*
      (H.field.toSubgroup ⧸
        (localResidueDatum K).extensionInertiaWithin
          H.field J hJH) := by
  dsimp only
  let F := abstractFixedField K (SeparableClosure K) H.field
  letI : Algebra F (SeparableClosure F) :=
    (separableClosure F (AlgebraicClosure F)).algebra
  intro e
  let E := abstractRelativeFixedField K (SeparableClosure K) hJH
  letI : FiniteDimensional K F :=
    abstractFixedField_finiteDimensional
      K (SeparableClosure K) H.field H.finite
  letI : NontriviallyNormedField F :=
    finiteExtensionSpectralNormedField K F
  letI : ValuativeRel F :=
    finiteExtensionSpectralValuativeRel K F
  letI : IsNonarchimedeanLocalField F :=
    finiteExtensionSpectralIsNonarchimedeanLocalField K F
  letI : FiniteDimensional F E :=
    abstractRelativeFixedField_finiteDimensional
      K (SeparableClosure K) H.field J hJH H.finite hJfinite
  letI : IsGalois F E :=
    abstractRelativeFixedField_isGalois
      K (SeparableClosure K) H.field J hJH hJnormal
  let i : E →ₐ[F] SeparableClosure F :=
    e.symm.toAlgHom.comp E.val
  let EI := finiteGaloisAbstractExtensionOfEmbedding F E i
  let ψ := intrinsicBaseContinuousEquivAmbientFixedField K H e
  letI :
      ((localResidueDatum F).extensionInertiaWithin
        (intrinsicAbstractBase F) EI.field EI.below).Normal :=
    inferInstance
  letI :
      ((localResidueDatum K).extensionInertiaWithin
        H.field J hJH).Normal :=
    inferInstance
  exact
    LocalFieldTheory.QuotientGroup.continuousCongr
      ((localResidueDatum F).extensionInertiaWithin
        (intrinsicAbstractBase F) EI.field EI.below)
      ((localResidueDatum K).extensionInertiaWithin
        H.field J hJH)
      ψ
      (map_intrinsicExtensionInertia_eq_ambientFixedField
        K H J hJH e)
def

intrinsicFrobeniusQuotientEquivAmbientFixedField

L141 ↗
LocalClassFieldTheory.intrinsicFrobeniusQuotientEquivAmbientFixedField
Documentation

The multiplicative equivalence from the intrinsic extension-inertia quotient of a finite fixed field to the corresponding quotient inside the ambient absolute Galois group, induced by the chosen equivalence of separable closures.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
Lean source · full declaration
def intrinsicFrobeniusQuotientEquivAmbientFixedField
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (H : FiniteAbstractField
      Gal(SeparableClosure K/K))
    (J : ClosedSubgroup Gal(SeparableClosure K/K))
    (hJH : J.toSubgroup ≤ H.field.toSubgroup)
    [hJnormal : (extensionSubgroup H.field J hJH).Normal]
    [hJfinite : Finite
      (H.field.toSubgroup ⧸ extensionSubgroup H.field J hJH)] :
    let F := abstractFixedField K (SeparableClosure K) H.field
    letI : Algebra F (SeparableClosure F) :=
      (separableClosure F (AlgebraicClosure F)).algebra
    ∀ (e : SeparableClosure F ≃ₐ[F] SeparableClosure K),
    let E := abstractRelativeFixedField K (SeparableClosure K) hJH
    letI : FiniteDimensional K F :=
      abstractFixedField_finiteDimensional
        K (SeparableClosure K) H.field H.finite
    letI : NontriviallyNormedField F :=
      finiteExtensionSpectralNormedField K F
    letI : ValuativeRel F :=
      finiteExtensionSpectralValuativeRel K F
    letI : IsNonarchimedeanLocalField F :=
      finiteExtensionSpectralIsNonarchimedeanLocalField K F
    letI : FiniteDimensional F E :=
      abstractRelativeFixedField_finiteDimensional
        K (SeparableClosure K) H.field J hJH H.finite hJfinite
    letI : IsGalois F E :=
      abstractRelativeFixedField_isGalois
        K (SeparableClosure K) H.field J hJH hJnormal
    let i : E →ₐ[F] SeparableClosure F :=
      e.symm.toAlgHom.comp E.val
    let EI := finiteGaloisAbstractExtensionOfEmbedding F E i
    ((intrinsicAbstractBase F).toSubgroup ⧸
        (localResidueDatum F).extensionInertiaWithin
          (intrinsicAbstractBase F) EI.field EI.below) ≃*
      (H.field.toSubgroup ⧸
        (localResidueDatum K).extensionInertiaWithin
          H.field J hJH) := by
  dsimp only
  intro e
  exact
    (intrinsicFrobeniusQuotientContinuousEquivAmbientFixedField
      K H J hJH e).toMulEquiv
theorem

intrinsicFrobeniusQuotientEquivAmbientFixedField_mk

L189 ↗
LocalClassFieldTheory.intrinsicFrobeniusQuotientEquivAmbientFixedField_mk
Documentation

The fixed-field quotient equivalence sends the class of an intrinsic automorphism to the class of the corresponding ambient automorphism.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
Lean source · full declaration
theorem intrinsicFrobeniusQuotientEquivAmbientFixedField_mk
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (H : FiniteAbstractField
      Gal(SeparableClosure K/K))
    (J : ClosedSubgroup Gal(SeparableClosure K/K))
    (hJH : J.toSubgroup ≤ H.field.toSubgroup)
    [hJnormal : (extensionSubgroup H.field J hJH).Normal]
    [hJfinite : Finite
      (H.field.toSubgroup ⧸ extensionSubgroup H.field J hJH)] :
    let F := abstractFixedField K (SeparableClosure K) H.field
    letI : Algebra F (SeparableClosure F) :=
      (separableClosure F (AlgebraicClosure F)).algebra
    ∀ (e : SeparableClosure F ≃ₐ[F] SeparableClosure K)
      (τ : (intrinsicAbstractBase F).toSubgroup),
    intrinsicFrobeniusQuotientEquivAmbientFixedField
        K H J hJH e (QuotientGroup.mk τ) =
      QuotientGroup.mk
        (intrinsicBaseEquivAmbientFixedField K H e τ) := by
  dsimp only
  rintro e τ
  exact LocalFieldTheory.QuotientGroup.continuousCongr_mk _ _ _ _ _
theorem

intrinsicFrobeniusQuotientEquivAmbientFixedField_normalizedDegree

L214 ↗
LocalClassFieldTheory.intrinsicFrobeniusQuotientEquivAmbientFixedField_normalizedDegree
Documentation

The intrinsic-to-ambient Frobenius quotient equivalence preserves the normalized extension degree of every quotient class.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
Lean source · full declaration
theorem
    intrinsicFrobeniusQuotientEquivAmbientFixedField_normalizedDegree
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (H : FiniteAbstractField
      Gal(SeparableClosure K/K))
    (J : ClosedSubgroup Gal(SeparableClosure K/K))
    (hJH : J.toSubgroup ≤ H.field.toSubgroup)
    [hJnormal : (extensionSubgroup H.field J hJH).Normal]
    [hJfinite : Finite
      (H.field.toSubgroup ⧸ extensionSubgroup H.field J hJH)] :
    let F := abstractFixedField K (SeparableClosure K) H.field
    letI : Algebra F (SeparableClosure F) :=
      (separableClosure F (AlgebraicClosure F)).algebra
    ∀ (e : SeparableClosure F ≃ₐ[F] SeparableClosure K),
    let E := abstractRelativeFixedField K (SeparableClosure K) hJH
    letI : FiniteDimensional K F :=
      abstractFixedField_finiteDimensional
        K (SeparableClosure K) H.field H.finite
    letI : NontriviallyNormedField F :=
      finiteExtensionSpectralNormedField K F
    letI : ValuativeRel F :=
      finiteExtensionSpectralValuativeRel K F
    letI : IsNonarchimedeanLocalField F :=
      finiteExtensionSpectralIsNonarchimedeanLocalField K F
    letI : FiniteDimensional F E :=
      abstractRelativeFixedField_finiteDimensional
        K (SeparableClosure K) H.field J hJH H.finite hJfinite
    letI : IsGalois F E :=
      abstractRelativeFixedField_isGalois
        K (SeparableClosure K) H.field J hJH hJnormal
    let i : E →ₐ[F] SeparableClosure F :=
      e.symm.toAlgHom.comp E.val
    let EI := finiteGaloisAbstractExtensionOfEmbedding F E i
    ∀ (q :
      (intrinsicAbstractBase F).toSubgroup ⧸
        (localResidueDatum F).extensionInertiaWithin
          (intrinsicAbstractBase F) EI.field EI.below),
    let RF :=
      (intrinsicFiniteAbstractBase F).toFiniteResidueAbstractField
        (localResidueDatum F)
    let RH :=
      H.toFiniteResidueAbstractField (localResidueDatum K)
    (localResidueDatum K).extensionNormalizedDegree
        RH J hJH
        (intrinsicFrobeniusQuotientEquivAmbientFixedField
          K H J hJH e q) =
      (localResidueDatum F).extensionNormalizedDegree
        RF EI.field EI.below q := by
  dsimp only
  let F := abstractFixedField K (SeparableClosure K) H.field
  let : Algebra F (SeparableClosure F) :=
    (separableClosure F (AlgebraicClosure F)).algebra
  intro e
  let E := abstractRelativeFixedField K (SeparableClosure K) hJH
  let : FiniteDimensional K F :=
    abstractFixedField_finiteDimensional
      K (SeparableClosure K) H.field H.finite
  let : NontriviallyNormedField F :=
    finiteExtensionSpectralNormedField K F
  let : ValuativeRel F :=
    finiteExtensionSpectralValuativeRel K F
  let : IsNonarchimedeanLocalField F :=
    finiteExtensionSpectralIsNonarchimedeanLocalField K F
  let : FiniteDimensional F E :=
    abstractRelativeFixedField_finiteDimensional
      K (SeparableClosure K) H.field J hJH H.finite hJfinite
  let : IsGalois F E :=
    abstractRelativeFixedField_isGalois
      K (SeparableClosure K) H.field J hJH hJnormal
  let i : E →ₐ[F] SeparableClosure F :=
    e.symm.toAlgHom.comp E.val
  let EI := finiteGaloisAbstractExtensionOfEmbedding F E i
  intro q
  let RF :=
    (intrinsicFiniteAbstractBase F).toFiniteResidueAbstractField
      (localResidueDatum F)
  let RH :=
    H.toFiniteResidueAbstractField (localResidueDatum K)
  refine Quotient.inductionOn' q ?_
  intro τ
  let τRF : RF.field.toSubgroup :=
    ⟨τ.1, τ.2⟩
  let ψτRH : RH.field.toSubgroup :=
    ⟨(intrinsicBaseEquivAmbientFixedField K H e τ).1,
      (intrinsicBaseEquivAmbientFixedField K H e τ).2⟩
  change
    (localResidueDatum K).normalizedDegree RH ψτRH =
      (localResidueDatum F).normalizedDegree RF τRF
  have hψτRH :
      ψτRH =
        (abstractSubgroupEquivGaloisGroup
          K (SeparableClosure K) H.field).symm
            (AlgEquiv.autCongr e τ.1) := by
    apply Subtype.ext
    exact
      intrinsicBaseEquivAmbientFixedField_apply_val
        K H e τ
  rw [hψτRH]
  exact
    (intrinsicBase_normalizedDegree_eq_ambientFixedField
      K H e τ).symm
abbrev

intrinsicFixedFieldFrobeniusElements

L319 ↗
LocalClassFieldTheory.intrinsicFixedFieldFrobeniusElements
Documentation

Intrinsic extension-inertia quotient classes whose normalized degree is a strictly positive power of the canonical Frobenius degree.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
Lean source · statement
abbrev intrinsicFixedFieldFrobeniusElements
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (H : FiniteAbstractField
      Gal(SeparableClosure K/K))
    (J : ClosedSubgroup Gal(SeparableClosure K/K))
    (hJH : J.toSubgroup ≤ H.field.toSubgroup)
    [hJnormal : (extensionSubgroup H.field J hJH).Normal]
    [hJfinite : Finite
      (H.field.toSubgroup ⧸ extensionSubgroup H.field J hJH)]
    (e : intrinsicFixedFieldSeparableClosureEquiv K H)
abbrev

ambientFixedFieldFrobeniusQuotient

L366 ↗
LocalClassFieldTheory.ambientFixedFieldFrobeniusQuotient
Documentation

The ambient fixed subgroup modulo the extension-inertia subgroup attached to the given finite Galois extension.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
Lean source · statement
abbrev ambientFixedFieldFrobeniusQuotient
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (H : FiniteAbstractField
      Gal(SeparableClosure K/K))
    (J : ClosedSubgroup Gal(SeparableClosure K/K))
    (hJH : J.toSubgroup ≤ H.field.toSubgroup)
    [_hJnormal : (extensionSubgroup H.field J hJH).Normal]
abbrev

ambientFixedFieldFrobeniusProperty

L380 ↗
LocalClassFieldTheory.ambientFixedFieldFrobeniusProperty
Documentation

The property that an ambient quotient class has normalized degree equal to a strictly positive power of the canonical Frobenius degree.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
Lean source · statement
abbrev ambientFixedFieldFrobeniusProperty
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (H : FiniteAbstractField
      Gal(SeparableClosure K/K))
    (J : ClosedSubgroup Gal(SeparableClosure K/K))
    (hJH : J.toSubgroup ≤ H.field.toSubgroup)
    [hJnormal : (extensionSubgroup H.field J hJH).Normal]
    (q : ambientFixedFieldFrobeniusQuotient K H J hJH) : Prop
abbrev

ambientFixedFieldFrobeniusElements

L397 ↗
LocalClassFieldTheory.ambientFixedFieldFrobeniusElements
Documentation

Ambient extension-inertia quotient classes satisfying the positive Frobenius-degree property.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
Lean source · statement
abbrev ambientFixedFieldFrobeniusElements
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (H : FiniteAbstractField
      Gal(SeparableClosure K/K))
    (J : ClosedSubgroup Gal(SeparableClosure K/K))
    (hJH : J.toSubgroup ≤ H.field.toSubgroup)
    [hJnormal : (extensionSubgroup H.field J hJH).Normal]
theorem

intrinsicFrobeniusElementToAmbientFixedField_property

L410 ↗
LocalClassFieldTheory.intrinsicFrobeniusElementToAmbientFixedField_property
Documentation

Transporting an intrinsic Frobenius element to the ambient quotient preserves its positive Frobenius-degree property.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
Lean source · statement
theorem
    intrinsicFrobeniusElementToAmbientFixedField_property
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (H : FiniteAbstractField
      Gal(SeparableClosure K/K))
    (J : ClosedSubgroup Gal(SeparableClosure K/K))
    (hJH : J.toSubgroup ≤ H.field.toSubgroup)
    [hJnormal : (extensionSubgroup H.field J hJH).Normal]
    [hJfinite : Finite
      (H.field.toSubgroup ⧸ extensionSubgroup H.field J hJH)]
    (e : intrinsicFixedFieldSeparableClosureEquiv K H)
    (σ : intrinsicFixedFieldFrobeniusElements K H J hJH e) :
    ambientFixedFieldFrobeniusProperty K H J hJH
      (intrinsicFrobeniusQuotientEquivAmbientFixedField
        K H J hJH e σ.1)
def

intrinsicFrobeniusElementToAmbientFixedField

L440 ↗
LocalClassFieldTheory.intrinsicFrobeniusElementToAmbientFixedField
Documentation

Transport an intrinsic fixed-field Frobenius element to the ambient extension-inertia quotient, together with its positive Frobenius-degree property.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
Lean source · statement
def
    intrinsicFrobeniusElementToAmbientFixedField
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (H : FiniteAbstractField
      Gal(SeparableClosure K/K))
    (J : ClosedSubgroup Gal(SeparableClosure K/K))
    (hJH : J.toSubgroup ≤ H.field.toSubgroup)
    [hJnormal : (extensionSubgroup H.field J hJH).Normal]
    [hJfinite : Finite
      (H.field.toSubgroup ⧸ extensionSubgroup H.field J hJH)]
    (e : intrinsicFixedFieldSeparableClosureEquiv K H)
    (σ : intrinsicFixedFieldFrobeniusElements K H J hJH e) :
    ambientFixedFieldFrobeniusElements K H J hJH
theorem

intrinsicFrobeniusElementToAmbientFixedField_val

L463 ↗
LocalClassFieldTheory.intrinsicFrobeniusElementToAmbientFixedField_val
Documentation

The quotient class underlying a transported intrinsic Frobenius element is the image under the intrinsic-to-ambient quotient equivalence.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
Lean source · statement
theorem intrinsicFrobeniusElementToAmbientFixedField_val
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (H : FiniteAbstractField
      Gal(SeparableClosure K/K))
    (J : ClosedSubgroup Gal(SeparableClosure K/K))
    (hJH : J.toSubgroup ≤ H.field.toSubgroup)
    [hJnormal : (extensionSubgroup H.field J hJH).Normal]
    [hJfinite : Finite
      (H.field.toSubgroup ⧸ extensionSubgroup H.field J hJH)]
    (e : intrinsicFixedFieldSeparableClosureEquiv K H)
    (σ : intrinsicFixedFieldFrobeniusElements K H J hJH e) :
    (intrinsicFrobeniusElementToAmbientFixedField
        K H J hJH e σ).1 =
      intrinsicFrobeniusQuotientEquivAmbientFixedField
        K H J hJH e σ.1

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