EverywhereUnramifiedProPCompositum.lean

structure FiniteEverywhereUnramifiedProPExtension
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) where
  /-- The intermediate field inside the chosen algebraic closure. -/
  field : IntermediateField F (AlgebraicClosure F)
  /-- Finiteness of the extension over the base field. -/
  [finiteDimensional : FiniteDimensional F field]
  /-- The extension is Galois over the base field. -/
  [isGalois : IsGalois F field]
  /-- The intermediate field is itself a number field. -/
  [numberField : NumberField field]
  /-- Its finite Galois group is a `p`-group. -/
  isPGroup : IsPGroup p (field ≃ₐ[F] field)
  /-- The extension is unramified at every finite and infinite place. -/
  everywhereUnramified : IsEverywhereUnramified F field

def bot : FiniteEverywhereUnramifiedProPExtension F p where
  field := ⊥
  finiteDimensional := inferInstance
  isGalois := inferInstance
  numberField := NumberField.of_module_finite F ↥(⊥ :
    IntermediateField F (AlgebraicClosure F))
  isPGroup := by
    apply IsPGroup.of_card (n := 0)
    rw [IsGalois.card_aut_eq_finrank F
      (⊥ : IntermediateField F (AlgebraicClosure F)),
      IntermediateField.finrank_bot, pow_zero]
  everywhereUnramified := by
    let hNumber : NumberField ↥(⊥ :
        IntermediateField F (AlgebraicClosure F)) :=
      NumberField.of_module_finite F ↥(⊥ :
        IntermediateField F (AlgebraicClosure F))
    let _ := hNumber
    exact everywhereUnramified_congrTop
      (IntermediateField.botEquiv F (AlgebraicClosure F)).symm
      (IsEverywhereUnramified.refl F)

theorem isPGroup_prod
    {G H : Type*} [Group G] [Group H]
    (hG : IsPGroup p G) (hH : IsPGroup p H) :
    IsPGroup p (G × H)

theorem isPGroup_sup
    (E₁ E₂ : FiniteEverywhereUnramifiedProPExtension F p) :
    IsPGroup p
      (↥(E₁.field ⊔ E₂.field) ≃ₐ[F]
        ↥(E₁.field ⊔ E₂.field))

def sup [Fact p.Prime] (hpOdd : Odd p)
    (E₁ E₂ : FiniteEverywhereUnramifiedProPExtension F p) :
    FiniteEverywhereUnramifiedProPExtension F p

theorem maximalEverywhereUnramifiedProP_eq_iSup_extension
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact p.Prime] :
    maximalEverywhereUnramifiedProP F p =
      ⨆ E : FiniteEverywhereUnramifiedProPExtension F p, E.field