AbsoluteRealProPUnramified.lean

theorem finiteInertia_fixes_layer
    (F : Type) [Field F] [NumberField F]
    (M : FiniteGaloisIntermediateField F (AlgebraicClosure F)) [NumberField M]
    (T : Set (HeightOneSpectrum (𝓞 F)))
    (hM : IsUnramifiedAtFinitePlacesOutside F M T)
    (v : HeightOneSpectrum (𝓞 F)) (hv : v ∉ T)
    (σ : finitePlaceAbsoluteInertiaSubgroup F v) :
    (σ.1.1 : AlgebraicClosure F ≃ₐ[F] AlgebraicClosure F) ∈
      M.toIntermediateField.fixingSubgroup

theorem absoluteToMaximalRealProPOutside_inertia (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ))) (v : HeightOneSpectrum (𝓞 ℚ))
    (hv : v ∉ T) (σ : finitePlaceAbsoluteInertiaSubgroup ℚ v) :
    absoluteToMaximalRealProPOutside p T
      (finitePlaceAbsoluteDecompositionInclusion ℚ v σ.1) = 1

theorem infiniteArtin_fixes_totallyReal
    (F : Type) [Field F] [CharZero F] (M : IntermediateField F (AlgebraicClosure F))
    [IsTotallyReal M] (v : InfinitePlace F) (x : M) :
    (show AlgebraicClosure F ≃ₐ[F] AlgebraicClosure F from absoluteInfinitePlaceArtinNegOne F v)
      (x : AlgebraicClosure F) = (x : AlgebraicClosure F) := by
  let w : InfinitePlace (AlgebraicClosure F) :=
    chosenInfinitePlaceAbove (L := AlgebraicClosure F) v
  let c : Gal(AlgebraicClosure F/F) :=
    chosenInfinitePlaceArtinMonoidHom (K := F) (L := AlgebraicClosure F) v (-1 : v.Completionˣ)
  change c (x : AlgebraicClosure F) = (x : AlgebraicClosure F)
  by_cases hw : w.IsUnramified F
  · have hc : c = 1 := by
      change (infinitePlaceArtinMonoidHomOfPlace (K := F) (L := AlgebraicClosure F)
        v w (chosenInfinitePlaceAbove_comap (L := AlgebraicClosure F) v)) (-1) = 1
      simp only [infinitePlaceArtinMonoidHomOfPlace, dite_eq_left hw, MonoidHom.one_apply]
    rw [hc]
    rfl
  · have hConj : ComplexEmbedding.IsConj w.embedding c :=
      chosenInfinitePlaceArtinMonoidHom_neg_one_isConj_of_ramified
        (K := F) (L := AlgebraicClosure F) v hw
    have hReal : ComplexEmbedding.IsReal (w.embedding.comp (algebraMap M (AlgebraicClosure F))) :=
      IsTotallyReal.complexEmbedding_isReal _
    apply w.embedding.injective
    exact (hConj.eq (x : AlgebraicClosure F)).trans
      (RingHom.congr_fun (ComplexEmbedding.isReal_iff.mp hReal) x)

theorem absoluteToMaximalRealProPOutside_infiniteArtin (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ))) (v : InfinitePlace ℚ) :
    absoluteToMaximalRealProPOutside p T (absoluteInfinitePlaceArtinNegOne ℚ v) = 1