FiniteGaloisSubextension.lean

structure FiniteGaloisSubextension (K : ClosedSubgroup G) where
  /-- The closed subgroup representing the top field. -/
  field : ClosedSubgroup G
  /-- The top-field subgroup is contained in the base-field subgroup. -/
  below : field.toSubgroup ≤ K.toSubgroup
  /-- The top-field subgroup is normal inside the base-field subgroup. -/
  normal : (extensionSubgroup K field below).Normal
  /-- The relative Galois quotient is finite. -/
  finite : Finite (K.toSubgroup ⧸ extensionSubgroup K field below)

def toGaloisSubextension (L : FiniteGaloisSubextension K) :
    DegreeData.GaloisSubextension K where
  field := L.field
  below := L.below
  normal := L.normal

def toFiniteAbstractExtension (L : FiniteGaloisSubextension K) :
    DegreeData.FiniteAbstractExtension G where
  field := L.field
  base := K
  below := L.below
  finiteQuotient := L.finite

def extensionQuotient (L : FiniteGaloisSubextension K) : Type u

def IsUnramified (L : FiniteGaloisSubextension K) (D : DegreeData G) : Prop

def IsTotallyRamified (L : FiniteGaloisSubextension K)
    (D : DegreeData G) : Prop

instance extensionSubgroup_normalInstance (L : FiniteGaloisSubextension K) :
    (extensionSubgroup K L.field L.below).Normal

instance extensionQuotient_groupInstance (L : FiniteGaloisSubextension K) :
    Group L.extensionQuotient

instance extensionQuotient_finiteInstance (L : FiniteGaloisSubextension K) :
    Finite L.extensionQuotient

def extensionQuotientMulEquiv (L : FiniteGaloisSubextension K) :
    L.extensionQuotient ≃*
      (K.toSubgroup ⧸ extensionSubgroup K L.field L.below)

def extensionQuotientMk (L : FiniteGaloisSubextension K) :
    K.toSubgroup →* L.extensionQuotient

theorem extensionQuotientMk_apply (L : FiniteGaloisSubextension K)
    (k : K.toSubgroup) :
    L.extensionQuotientMulEquiv (L.extensionQuotientMk k) =
      (QuotientGroup.mk k :
        K.toSubgroup ⧸ extensionSubgroup K L.field L.below)

theorem extensionQuotientMk_eq_one_iff (L : FiniteGaloisSubextension K)
    (k : K.toSubgroup) :
    L.extensionQuotientMk k = 1 ↔
      k ∈ extensionSubgroup K L.field L.below

theorem extensionQuotientMk_surjective (L : FiniteGaloisSubextension K) :
    Function.Surjective L.extensionQuotientMk

def toGaloisExtensionQuotientMulEquiv (L : FiniteGaloisSubextension K) :
    L.extensionQuotient ≃* L.toGaloisSubextension.extensionQuotient

theorem extensionQuotient_inductionOn
    (L : FiniteGaloisSubextension K) {motive : L.extensionQuotient → Prop}
    (q : L.extensionQuotient)
    (mk : ∀ k : K.toSubgroup, motive (L.extensionQuotientMk k)) :
    motive q

theorem toGaloisSubextension_isUnramified_iff
    (L : FiniteGaloisSubextension K) (D : DegreeData G) :
    L.toGaloisSubextension.IsUnramified D ↔ L.IsUnramified D

theorem toGaloisSubextension_isTotallyRamified_iff
    (L : FiniteGaloisSubextension K) (D : DegreeData G) :
    L.toGaloisSubextension.IsTotallyRamified D ↔ L.IsTotallyRamified D

theorem isUnramified_toGaloisSubextension
    (L : FiniteGaloisSubextension K) (D : DegreeData G)
    (hL : L.IsUnramified D) :
    L.toGaloisSubextension.IsUnramified D

theorem isTotallyRamified_toGaloisSubextension
    (L : FiniteGaloisSubextension K) (D : DegreeData G)
    (hL : L.IsTotallyRamified D) :
    L.toGaloisSubextension.IsTotallyRamified D

theorem isUnramified_iff_inertia_le (L : FiniteGaloisSubextension K)
    (D : DegreeData G) :
    L.IsUnramified D ↔
      K.toSubgroup ⊓ D.degree.toMonoidHom.ker ≤ L.field.toSubgroup

theorem isTotallyRamified_iff_image_le (L : FiniteGaloisSubextension K)
    (D : DegreeData G) :
    L.IsTotallyRamified D ↔
      K.toSubgroup.map D.degree.toMonoidHom ≤
        L.field.toSubgroup.map D.degree.toMonoidHom

def toFiniteAbstractFieldExtension
    {K : FiniteAbstractField G} (L : FiniteGaloisSubextension K.field) :
    FiniteAbstractFieldExtension G

theorem finite_extension_trans
    {P L K : ClosedSubgroup G}
    (hPL : P.toSubgroup ≤ L.toSubgroup)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hPLfinite : Finite
      (L.toSubgroup ⧸ extensionSubgroup L P hPL)]
    [hLKfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)] :
    Finite (K.toSubgroup ⧸ extensionSubgroup K P (hPL.trans hLK))

theorem finite_extension_over_intermediate
    {P M K : ClosedSubgroup G}
    (hPK : P.toSubgroup ≤ K.toSubgroup)
    (hMK : M.toSubgroup ≤ K.toSubgroup)
    (hPM : P.toSubgroup ≤ M.toSubgroup)
    [hPKfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K P hPK)] :
    Finite (M.toSubgroup ⧸ extensionSubgroup M P hPM)

theorem finite_intermediate_extension
    {P M K : ClosedSubgroup G}
    (hPK : P.toSubgroup ≤ K.toSubgroup)
    (hPM : P.toSubgroup ≤ M.toSubgroup)
    (hMK : M.toSubgroup ≤ K.toSubgroup)
    [hPKfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K P hPK)] :
    Finite (K.toSubgroup ⧸ extensionSubgroup K M hMK)

def baseChange (M : FiniteGaloisSubextension K) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup) : FiniteGaloisSubextension L where
  field := L ⊓ M.field
  below := inf_le_left
  normal := by
    let f : L.toSubgroup →* K.toSubgroup := Subgroup.inclusion hLK
    have heq : extensionSubgroup L (L ⊓ M.field) inf_le_left =
        (extensionSubgroup K M.field M.below).comap f := by
      ext x
      rw [mem_extensionSubgroup_iff, Subgroup.mem_comap,
        mem_extensionSubgroup_iff]
      change (x : G) ∈ L ⊓ M.field ↔ (x : G) ∈ M.field
      exact ⟨fun hx => hx.2, fun hx => ⟨x.property, hx⟩⟩
    rw [heq]
    let : (extensionSubgroup K M.field M.below).Normal := M.normal
    infer_instance
  finite := by
    let f : L.toSubgroup →* K.toSubgroup := Subgroup.inclusion hLK
    let E := extensionSubgroup K M.field M.below
    have heq : extensionSubgroup L (L ⊓ M.field) inf_le_left = E.comap f := by
      ext x
      rw [mem_extensionSubgroup_iff, Subgroup.mem_comap]
      dsimp only [E, f, Subgroup.inclusion]
      rw [mem_extensionSubgroup_iff]
      change (x : G) ∈ L ⊓ M.field ↔ (x : G) ∈ M.field
      exact ⟨fun hx => hx.2, fun hx => ⟨x.property, hx⟩⟩
    let : Finite (K.toSubgroup ⧸ E) := M.finite
    let : E.Normal := M.normal
    have hE0 : E.index ≠ 0 := Subgroup.index_ne_zero_of_finite
    have hrel0 : E.relIndex f.range ≠ 0 := by
      intro hzero
      have hdvd : E.relIndex f.range ∣ E.index :=
        E.relIndex_dvd_index_of_normal f.range
      rw [hzero, zero_dvd_iff] at hdvd
      exact hE0 hdvd
    apply Nat.finite_of_card_ne_zero
    change (extensionSubgroup L (L ⊓ M.field) inf_le_left).index ≠ 0
    rw [heq, E.index_comap f]
    exact hrel0

def refl (K : ClosedSubgroup G) : FiniteGaloisSubextension K where
  field := K
  below := le_rfl
  normal := by
    have htop : extensionSubgroup K K le_rfl = ⊤ := by
      rw [eq_top_iff]
      intro x _
      exact x.2
    rw [htop]
    infer_instance
  finite := by
    have htop : extensionSubgroup K K le_rfl = ⊤ := by
      rw [eq_top_iff]
      intro x _
      exact x.2
    rw [htop]
    infer_instance

def compositum (L₁ L₂ : FiniteGaloisSubextension K) :
    FiniteGaloisSubextension K where
  field := L₁.field ⊓ L₂.field
  below := fun _ h => L₁.below h.1
  normal := by
    have heq : extensionSubgroup K (L₁.field ⊓ L₂.field)
        (fun _ h => L₁.below h.1) =
        extensionSubgroup K L₁.field L₁.below ⊓
          extensionSubgroup K L₂.field L₂.below := by
      ext k
      simp only [Subgroup.mem_inf, mem_extensionSubgroup_iff]
      constructor
      · intro hk
        exact ⟨hk.1, hk.2⟩
      · rintro ⟨h₁, h₂⟩
        exact ⟨h₁, h₂⟩
    rw [heq]
    let : (extensionSubgroup K L₁.field L₁.below).Normal := L₁.normal
    let : (extensionSubgroup K L₂.field L₂.below).Normal := L₂.normal
    infer_instance
  finite := by
    have heq : extensionSubgroup K (L₁.field ⊓ L₂.field)
        (fun _ h => L₁.below h.1) =
        extensionSubgroup K L₁.field L₁.below ⊓
          extensionSubgroup K L₂.field L₂.below := by
      ext k
      simp only [Subgroup.mem_inf, mem_extensionSubgroup_iff]
      constructor
      · intro hk
        exact ⟨hk.1, hk.2⟩
      · rintro ⟨h₁, h₂⟩
        exact ⟨h₁, h₂⟩
    let : (extensionSubgroup K L₁.field L₁.below).FiniteIndex :=
      @Subgroup.finiteIndex_of_finite_quotient K.toSubgroup _
        (extensionSubgroup K L₁.field L₁.below) L₁.finite
    let : (extensionSubgroup K L₂.field L₂.below).FiniteIndex :=
      @Subgroup.finiteIndex_of_finite_quotient K.toSubgroup _
        (extensionSubgroup K L₂.field L₂.below) L₂.finite
    rw [heq]
    exact Subgroup.finite_quotient_of_finiteIndex

theorem compositum_le_left (L₁ L₂ : FiniteGaloisSubextension K) :
    (L₁.compositum L₂).field.toSubgroup ≤ L₁.field.toSubgroup

theorem compositum_le_right (L₁ L₂ : FiniteGaloisSubextension K) :
    (L₁.compositum L₂).field.toSubgroup ≤ L₂.field.toSubgroup

theorem finiteNormSubgroup_compositum_le_left
    (A : Rep ℤ G) (L₁ L₂ : FiniteGaloisSubextension K) :
    letI := (L₁.compositum L₂).finite
    letI := L₁.finite
    finiteNormSubgroup A K (L₁.compositum L₂).field
        (L₁.compositum L₂).below ≤
      finiteNormSubgroup A K L₁.field L₁.below := by
  let P := L₁.compositum L₂
  let hPL₁ := L₁.compositum_le_left L₂
  let : Finite (K.toSubgroup ⧸
      extensionSubgroup K P.field P.below) := P.finite
  let : Finite (K.toSubgroup ⧸
      extensionSubgroup K L₁.field L₁.below) := L₁.finite
  have hPKindex : P.field.toSubgroup.relIndex K.toSubgroup ≠ 0 := by
    rw [Subgroup.relIndex]
    exact Subgroup.index_ne_zero_of_finite
  have hPLindex : P.field.toSubgroup.relIndex L₁.field.toSubgroup ≠ 0 := by
    intro hzero
    have hmul := Subgroup.relIndex_mul_relIndex
      P.field.toSubgroup L₁.field.toSubgroup K.toSubgroup hPL₁ L₁.below
    rw [hzero, zero_mul] at hmul
    exact hPKindex hmul.symm
  let hPLfinite : Finite (L₁.field.toSubgroup ⧸
      extensionSubgroup L₁.field P.field hPL₁) := by
    apply Nat.finite_of_card_ne_zero
    change (extensionSubgroup L₁.field P.field hPL₁).index ≠ 0
    simpa [Subgroup.relIndex] using hPLindex
  let T : DegreeData.FiniteTower G := {
    top := P.field
    middle := L₁.field
    base := K
    top_le_middle := hPL₁
    middle_le_base := L₁.below
    finiteTopQuotient := hPLfinite
    finiteBaseQuotient := L₁.finite }
  rintro x ⟨a, rfl⟩
  refine ⟨relativeNorm A L₁.field P.field hPL₁ a, ?_⟩
  exact T.norm_trans_apply A a

theorem finiteNormSubgroup_compositum_le_right
    (A : Rep ℤ G) (L₁ L₂ : FiniteGaloisSubextension K) :
    letI := (L₁.compositum L₂).finite
    letI := L₂.finite
    finiteNormSubgroup A K (L₁.compositum L₂).field
        (L₁.compositum L₂).below ≤
      finiteNormSubgroup A K L₂.field L₂.below := by
  simpa [compositum, inf_comm] using
    finiteNormSubgroup_compositum_le_left A L₂ L₁