SimpleExtensionLocalBehavior.lean

theorem valuativeRelExtension_isNontrivial
    {C F : Type}
    [Field C] [Field F] [Algebra C F]
    [ValuativeRel C] [ValuativeRel F]
    [Valuation.HasExtension
      (ValuativeRel.valuation C) (ValuativeRel.valuation F)]
    [(ValuativeRel.valuation C).IsNontrivial] :
    (ValuativeRel.valuation F).IsNontrivial

theorem
    kummerGeneratedExtension_chosenFinitePlaceIsUnramified_of_valuation_eq_one
    {L : Type}
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (n : ℕ+)
    (b : Kˣ)
    (beta : Lˣ)
    (hbeta :
      beta ^ (n : ℕ) =
        Units.map (algebraMap K L).toMonoidHom b)
    (hgen :
      IntermediateField.adjoin K
        ({(beta : L)} : Set L) = ⊤)
    (v : HeightOneSpectrum (𝓞 K))
    (hb : v.valuation K (b : K) = 1)
    (hn : v.valuation K ((n : ℕ) : K) = 1) :
    ChosenFinitePlaceIsUnramified
      (K := K) (L := L) v

theorem
    chosenSimpleKummerExtension_chosenFinitePlaceIsUnramified_of_valuation_eq_one
    (n : ℕ+)
    (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (b : Kˣ)
    (v : HeightOneSpectrum (𝓞 K))
    (hb : v.valuation K (b : K) = 1)
    (hn : v.valuation K ((n : ℕ) : K) = 1) :
    let L := chosenSimpleKummerExtension K n hnK b
    letI : FiniteDimensional K L :=
      chosenSimpleKummerExtension_finiteDimensional K n hnK b
    letI : IsAbelianGalois K L :=
      chosenSimpleKummerExtension_isAbelianGalois K n hnK hmu b
    letI : NumberField L :=
      NumberField.of_module_finite K L
    ChosenFinitePlaceIsUnramified
      (K := K) (L := L) v := by
  let L := chosenSimpleKummerExtension K n hnK b
  let : FiniteDimensional K L :=
    chosenSimpleKummerExtension_finiteDimensional K n hnK b
  let : IsAbelianGalois K L :=
    chosenSimpleKummerExtension_isAbelianGalois K n hnK hmu b
  let : NumberField L :=
    NumberField.of_module_finite K L
  let beta : Lˣ :=
    chosenSimpleKummerRootUnit K n hnK b
  apply
    kummerGeneratedExtension_chosenFinitePlaceIsUnramified_of_valuation_eq_one
      (K := K) (L := L) n b beta
  · dsimp only [L, beta]
    exact chosenSimpleKummerRootUnit_pow K n hnK b
  · simpa [L, beta] using
      chosenSimpleKummerExtension_adjoin_root_eq_top K n hnK b
  · exact hb
  · exact hn

theorem
    chosenSimpleKummerExtension_isUnramifiedAt_at_all_finitePlacesAbove_of_valuation_eq_one
    (n : ℕ+)
    (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (b : Kˣ)
    (v : HeightOneSpectrum (𝓞 K))
    (hb : v.valuation K (b : K) = 1)
    (hn : v.valuation K ((n : ℕ) : K) = 1) :
    let L := chosenSimpleKummerExtension K n hnK b
    letI : FiniteDimensional K L :=
      chosenSimpleKummerExtension_finiteDimensional K n hnK b
    letI : IsAbelianGalois K L :=
      chosenSimpleKummerExtension_isAbelianGalois K n hnK hmu b
    letI : NumberField L :=
      NumberField.of_module_finite K L
    ∀ P : HeightOneSpectrum (𝓞 L),
      finitePlaceBelow (K := K) P = v →
        Algebra.IsUnramifiedAt (𝓞 K) P.asIdeal := by
  let L := chosenSimpleKummerExtension K n hnK b
  let _ : FiniteDimensional K L :=
    chosenSimpleKummerExtension_finiteDimensional K n hnK b
  let _ : IsAbelianGalois K L :=
    chosenSimpleKummerExtension_isAbelianGalois K n hnK hmu b
  let _ : NumberField L :=
    NumberField.of_module_finite K L
  have hunram :
      ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v := by
    simpa only [L] using
      chosenSimpleKummerExtension_chosenFinitePlaceIsUnramified_of_valuation_eq_one
        (K := K) n hnK hmu b v hb hn
  change ∀ P : HeightOneSpectrum (𝓞 L),
    finitePlaceBelow (K := K) P = v →
      Algebra.IsUnramifiedAt (𝓞 K) P.asIdeal
  intro P hP
  exact
    isUnramifiedAt_at_finitePlaceAbove_of_chosenFinitePlaceIsUnramified
      (K := K) (L := L) (v := v) (P := P)
      (hP := hP) (hunram := hunram)

theorem
    chosenSimpleKummerExtension_finitePlaceSplitsCompletely_of_mem_nthPowerSubgroup
    (n : ℕ+)
    (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (b : Kˣ)
    (v : HeightOneSpectrum (𝓞 K))
    (hb :
      Units.map
            (algebraMap K (v.adicCompletion K)).toMonoidHom b ∈
        (powMonoidHom (n : ℕ) :
          (v.adicCompletion K)ˣ →*
            (v.adicCompletion K)ˣ).range) :
    let E := chosenSimpleKummerExtension K n hnK b
    letI : FiniteDimensional K E :=
      chosenSimpleKummerExtension_finiteDimensional K n hnK b
    letI : IsAbelianGalois K E :=
      chosenSimpleKummerExtension_isAbelianGalois K n hnK hmu b
    FinitePlaceSplitsCompletely
      (K := K) (L := E) v := by
  let E := chosenSimpleKummerExtension K n hnK b
  let : FiniteDimensional K E :=
    chosenSimpleKummerExtension_finiteDimensional K n hnK b
  let : IsAbelianGalois K E :=
    chosenSimpleKummerExtension_isAbelianGalois K n hnK hmu b
  let beta : Eˣ :=
    chosenSimpleKummerRootUnit K n hnK b
  have hbeta :
      beta ^ (n : ℕ) =
        Units.map (algebraMap K E).toMonoidHom b := by
    dsimp only [E, beta]
    exact chosenSimpleKummerRootUnit_pow K n hnK b
  let D : Subgroup (E ≃ₐ[K] E) :=
    absoluteValueDecompositionGroup K
      (chosenFinitePlaceExtension (L := E) v).1
  have hfixed :
      (beta : E) ∈
        IntermediateField.fixedField D := by
    simpa only [D] using
      (finitePlaceKummerRadicand_mem_nthPowerSubgroup_iff_root_mem_decompositionFixedField
        (K := K) (L := E) v n hmu b beta hbeta).mp hb
  have hgen :
      IntermediateField.adjoin K ({(beta : E)} : Set E) = ⊤ := by
    simpa only [E, beta] using
      chosenSimpleKummerExtension_adjoin_root_eq_top K n hnK b
  have hle :
      IntermediateField.adjoin K ({(beta : E)} : Set E) ≤
        IntermediateField.fixedField D := by
    apply IntermediateField.adjoin_le_iff.mpr
    intro x hx
    have hx' : x = (beta : E) :=
      Set.mem_singleton_iff.mp hx
    subst x
    exact hfixed
  have htop :
      IntermediateField.fixedField D = ⊤ := by
    apply top_unique
    rw [← hgen]
    exact hle
  change D = ⊥
  rw [← IntermediateField.fixingSubgroup_fixedField D,
    htop, IntermediateField.fixingSubgroup_top]

theorem simpleKummer_localTensorNormSubgroup_eq_top
    (n : ℕ+)
    (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (b : Kˣ)
    (w : InfinitePlace K)
    (hb :
      Units.map
            (algebraMap K w.Completion).toMonoidHom b ∈
        (powMonoidHom (n : ℕ) :
          w.Completionˣ →* w.Completionˣ).range) :
    let E := chosenSimpleKummerExtension K n hnK b
    letI : FiniteDimensional K E :=
      chosenSimpleKummerExtension_finiteDimensional K n hnK b
    letI : IsAbelianGalois K E :=
      chosenSimpleKummerExtension_isAbelianGalois K n hnK hmu b
    localTensorNormSubgroup (K := K) (L := E) w.1 = ⊤ := by
  let E := chosenSimpleKummerExtension K n hnK b
  let : FiniteDimensional K E :=
    chosenSimpleKummerExtension_finiteDimensional K n hnK b
  let : IsAbelianGalois K E :=
    chosenSimpleKummerExtension_isAbelianGalois K n hnK hmu b
  let vK : AbsoluteValue K ℝ := w.1
  let hvK : vK.IsNontrivial := w.isNontrivial
  let u : AbsoluteValueExtension vK E :=
    pullbackAbsoluteValueExtension
      vK hvK IsAlgClosed.lift
  let hK :=
    AbsoluteValue.extensionCompletionAlgebra
      (K := K) u.1
  let : SMul K u.1.Completion := hK.toSMul
  let : Algebra vK.Completion u.1.Completion :=
    AbsoluteValue.completionAlgebra vK u.1 u.2
  let := localizedCompletionGlobalAlgebra vK u
  let := localizedCompletionIsScalarTower vK u
  let C := vK.Completion
  let F := LocalizedCompletion vK u
  let eK : w.Completion ≃+* C :=
    (infinitePlaceCompletionAlgEquiv
      (K := K) w).toRingEquiv
  let eC : w.Completionˣ ≃* Cˣ :=
    Units.mapEquiv eK.toMulEquiv
  let : FiniteDimensional C F :=
    localizedCompletionModuleFinite vK hvK u
  let : IsGalois C F :=
    HilbertRamification.algebraicLocalization_isGalois vK u
  let beta : Eˣ :=
    chosenSimpleKummerRootUnit K n hnK b
  have hbeta :
      beta ^ (n : ℕ) =
        Units.map (algebraMap K E).toMonoidHom b := by
    dsimp only [E, beta]
    exact chosenSimpleKummerRootUnit_pow K n hnK b
  have hbC :
      Units.map
            (algebraMap K C).toMonoidHom b ∈
        (powMonoidHom (n : ℕ) : Cˣ →* Cˣ).range := by
    obtain ⟨y, hy⟩ :=
      (MonoidHom.mem_range
        (G := w.Completionˣ)).mp hb
    refine
      (MonoidHom.mem_range
        (G := Cˣ)).mpr ⟨eC y, ?_⟩
    rw [powMonoidHom_apply] at hy ⊢
    calc
      (eC y) ^ (n : ℕ) =
          eC (y ^ (n : ℕ)) :=
        (map_pow eC y (n : ℕ)).symm
      _ =
          eC
            (Units.map
              (algebraMap K w.Completion).toMonoidHom b) :=
        congrArg eC hy
      _ =
          Units.map
            (algebraMap K C).toMonoidHom b := by
        apply Units.ext
        change
          (infinitePlaceCompletionAlgEquiv (K := K) w)
              (algebraMap K w.Completion (b : K)) =
            algebraMap K w.1.Completion (b : K)
        exact
          (infinitePlaceCompletionAlgEquiv
            (K := K) w).commutes (b : K)
  have hfixed :
      (beta : E) ∈
        IntermediateField.fixedField
          (absoluteValueDecompositionGroup K u.1) := by
    apply
      kummerRadicand_root_mem_decompositionFixedField_of_mem_nthPowerSubgroup
        (K := K) (L := E) vK hvK u n hmu b beta hbeta
    exact hbC
  let D : Subgroup (E ≃ₐ[K] E) :=
    absoluteValueDecompositionGroup K u.1
  have hgen :
      IntermediateField.adjoin K ({(beta : E)} : Set E) = ⊤ := by
    simpa only [E, beta] using
      chosenSimpleKummerExtension_adjoin_root_eq_top K n hnK b
  have hle :
      IntermediateField.adjoin K ({(beta : E)} : Set E) ≤
        IntermediateField.fixedField D := by
    apply IntermediateField.adjoin_le_iff.mpr
    intro x hx
    have hx' : x = (beta : E) :=
      Set.mem_singleton_iff.mp hx
    subst x
    change
      (beta : E) ∈
        IntermediateField.fixedField
          (absoluteValueDecompositionGroup K u.1)
    exact hfixed
  have htop :
      IntermediateField.fixedField D = ⊤ := by
    apply top_unique
    rw [← hgen]
    exact hle
  have hD : D = ⊥ := by
    rw [← IntermediateField.fixingSubgroup_fixedField D,
      htop, IntermediateField.fixingSubgroup_top]
  let eLocal :
      D ≃* (F ≃ₐ[C] F) :=
    decompositionGroupEquivAlgebraicLocalizationAut
      vK hvK u
  have hdegree :
      Module.finrank C F = 1 := by
    calc
      Module.finrank C F =
          Nat.card (F ≃ₐ[C] F) :=
        (IsGalois.card_aut_eq_finrank C F).symm
      _ = Nat.card D :=
        (Nat.card_congr eLocal.toEquiv).symm
      _ = 1 := by
        rw [hD]
        exact Nat.card_unique
  let : Module.Free C F :=
    Module.Free.of_divisionRing C F
  have hNormTop :
      localNormSubgroup C F = ⊤ := by
    apply top_unique
    intro x _
    refine
      ⟨Units.map (algebraMap C F).toMonoidHom x, ?_⟩
    apply Units.ext
    change
      Algebra.norm C (algebraMap C F (x : C)) =
        (x : C)
    rw [Algebra.norm_algebraMap, hdegree, pow_one]
  change localTensorNormSubgroup (K := K) (L := E) vK = ⊤
  rw [localTensorNormSubgroup_eq_localNormSubgroup
    (K := K) (L := E) vK u hvK]
  exact hNormTop

theorem
    chosenSimpleKummerExtension_infiniteTensorNormSubgroup_eq_top_of_mem_nthPowerSubgroup
    (n : ℕ+)
    (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (b : Kˣ)
    (w : InfinitePlace K)
    (hb :
      Units.map
            (algebraMap K w.Completion).toMonoidHom b ∈
        (powMonoidHom (n : ℕ) :
          w.Completionˣ →* w.Completionˣ).range) :
    let E := chosenSimpleKummerExtension K n hnK b
    letI : FiniteDimensional K E :=
      chosenSimpleKummerExtension_finiteDimensional K n hnK b
    letI : IsAbelianGalois K E :=
      chosenSimpleKummerExtension_isAbelianGalois K n hnK hmu b
    infiniteTensorNormSubgroup
      (K := K) (L := E) w = ⊤ := by
  let E := chosenSimpleKummerExtension K n hnK b
  let : FiniteDimensional K E :=
    chosenSimpleKummerExtension_finiteDimensional K n hnK b
  let : IsAbelianGalois K E :=
    chosenSimpleKummerExtension_isAbelianGalois K n hnK hmu b
  let vK : AbsoluteValue K ℝ := w.1
  let C := vK.Completion
  let eK : w.Completion ≃+* C :=
    (infinitePlaceCompletionAlgEquiv
      (K := K) w).toRingEquiv
  let eC : w.Completionˣ ≃* Cˣ :=
    Units.mapEquiv eK.toMulEquiv
  have hLocalTensorTop :
      localTensorNormSubgroup (K := K) (L := E) vK = ⊤ :=
    simpleKummer_localTensorNormSubgroup_eq_top (K := K) n hnK hmu b w hb
  let eA :
      (w.Completion ⊗[K] E) ≃+*
        LocalTensorAlgebra (L := E) vK :=
    (infinitePlaceLocalTensorAlgEquiv
      (K := K) (L := E) w).toRingEquiv
  let eU :
      (w.Completion ⊗[K] E)ˣ ≃*
        (LocalTensorAlgebra (L := E) vK)ˣ :=
    infinitePlaceLocalTensorUnitsEquiv
      (K := K) (L := E) w
  have hnorm
      (z : (w.Completion ⊗[K] E)ˣ) :
      eC
          (infiniteTensorDetNorm
            (K := K) (L := E) w z) =
        localTensorDetNorm
          (K := K) (L := E) vK (eU z) := by
    apply Units.ext
    change
      eK
          (Algebra.norm w.Completion
            (z : w.Completion ⊗[K] E)) =
        Algebra.norm C
          (eA (z : w.Completion ⊗[K] E))
    exact
      _root_.map_norm_tensorProduct_baseChange
        (K := K) (L := E)
        (infinitePlaceCompletionAlgEquiv
          (K := K) w).toAlgHom
        (z : w.Completion ⊗[K] E)
  apply top_unique
  intro x _
  have hx :
      eC x ∈
        localTensorNormSubgroup
          (K := K) (L := E) vK := by
    rw [hLocalTensorTop]
    trivial
  obtain ⟨z, hz⟩ := hx
  refine ⟨eU.symm z, eC.injective ?_⟩
  exact (hnorm (eU.symm z)).trans
    ((congrArg (localTensorDetNorm (K := K) (L := E) vK)
      (eU.apply_symm_apply z)).trans hz)