Basic.lean

abbrev decompositionGroup
    (P : Ideal B) (G : Type*) [Group G] [MulSemiringAction G B] :
    Subgroup G

theorem mem_decompositionGroup_iff
    {P : Ideal B} {G : Type*} [Group G] [MulSemiringAction G B] {σ : G} :
    σ ∈ decompositionGroup P G ↔ σ • P = P

abbrev inertiaGroup
    (P : Ideal B) (G : Type*) [Group G] [MulSemiringAction G B] :
    Subgroup G

theorem mem_inertiaGroup_iff
    {P : Ideal B} {G : Type*} [Group G] [MulSemiringAction G B] {σ : G} :
    σ ∈ inertiaGroup P G ↔ ∀ x : B, σ • x - x ∈ P

abbrev residueStabilizerHom
    (p : Ideal A) (P : Ideal B) [P.LiesOver p]
    (G : Type*) [Group G] [MulSemiringAction G B] [SMulCommClass G A B] :
    decompositionGroup P G →* (B ⧸ P) ≃ₐ[A ⧸ p] B ⧸ P

theorem residueStabilizerHom_apply
    (p : Ideal A) (P : Ideal B) [P.LiesOver p]
    (G : Type*) [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (σ : decompositionGroup P G) (b : B) :
    residueStabilizerHom p P G σ b = ↑(σ • b)

instance inertiaSubgroupOfDecomposition_normal
    (P : Ideal B) (G : Type*) [Group G] [MulSemiringAction G B] :
    ((inertiaGroup P G).subgroupOf (decompositionGroup P G)).Normal

theorem exists_smul_eq_of_isGaloisGroup
    (p : Ideal A) (P Q : Ideal B)
    [P.IsPrime] [P.LiesOver p] [Q.IsPrime] [Q.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] :
    ∃ σ : G, σ • P = Q

theorem dedekindRamification_ramificationIdx_eq
    (p : Ideal A) (P Q : Ideal B)
    [P.IsPrime] [P.LiesOver p] [Q.IsPrime] [Q.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] :
    P.ramificationIdx A = Q.ramificationIdx A

theorem dedekindRamification_inertiaDeg_eq
    (p : Ideal A) [p.IsMaximal] (P Q : Ideal B)
    [P.IsPrime] [P.LiesOver p] [Q.IsPrime] [Q.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] :
    P.inertiaDeg A = Q.inertiaDeg A

def dedekindDecomposition_primesOverEquivQuotientDecompositionGroup
    (p : Ideal A) (P : Ideal B) [P.IsPrime] [P.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] :
    p.primesOver B ≃ G ⧸ decompositionGroup P G

theorem dedekindDecomposition_ncard_primesOver_eq_decomposition_index
    (p : Ideal A) (P : Ideal B) [P.IsPrime] [P.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] :
    (p.primesOver B).ncard = (decompositionGroup P G).index

theorem dedekindDecomposition_decompositionGroup_eq_top_iff_primesOver_ncard_eq_one
    (p : Ideal A) (P : Ideal B) [P.IsPrime] [P.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] :
    decompositionGroup P G = ⊤ ↔ (p.primesOver B).ncard = 1

theorem dedekindDecomposition_decompositionGroup_eq_bot_iff_primesOver_ncard_eq_card
    (p : Ideal A) (P : Ideal B) [P.IsPrime] [P.LiesOver p]
    {G : Type*} [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] :
    decompositionGroup P G = ⊥ ↔ (p.primesOver B).ncard = Nat.card G

theorem dedekindRamification_residueAction_ker
    (p : Ideal A) (P : Ideal B) [P.LiesOver p]
    (G : Type*) [Group G] [MulSemiringAction G B] [SMulCommClass G A B] :
    MonoidHom.ker (residueStabilizerHom p P G) =
      (inertiaGroup P G).subgroupOf (decompositionGroup P G)

theorem dedekindRamification_residueAction_mulExact
    (p : Ideal A) (P : Ideal B) [P.LiesOver p]
    (G : Type*) [Group G] [MulSemiringAction G B] [SMulCommClass G A B] :
    Function.MulExact
      ((inertiaGroup P G).subgroupOf (decompositionGroup P G)).subtype
      (residueStabilizerHom p P G)

theorem dedekindRamification_residueAction_surjective
    (p : Ideal A) (P : Ideal B) [P.IsPrime] [P.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B]
    [Algebra.IsInvariant A B G] :
    Function.Surjective (residueStabilizerHom p P G)

theorem dedekindRamification_residueExtension_normal
    (p : Ideal A) [p.IsMaximal] (P : Ideal B)
    [P.IsMaximal] [P.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [Algebra.IsInvariant A B G] :
    Normal (A ⧸ p) (B ⧸ P)

theorem dedekindRamification_residueExtension_isGalois
    (p : Ideal A) [p.IsMaximal] (P : Ideal B)
    [P.IsMaximal] [P.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [Algebra.IsInvariant A B G] [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)] :
    IsGalois (A ⧸ p) (B ⧸ P)

theorem dedekindResidue_residueExtension_normal_and_residueAction_surjective
    (p : Ideal A) [p.IsMaximal] (P : Ideal B)
    [P.IsMaximal] [P.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B]
    [Algebra.IsInvariant A B G] :
    Normal (A ⧸ p) (B ⧸ P) ∧
      Function.Surjective (residueStabilizerHom p P G)

theorem dedekindRamification_residueAction_shortExact
    (p : Ideal A) (P : Ideal B) [P.IsPrime] [P.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B]
    [Algebra.IsInvariant A B G] :
    Function.Injective
        ((inertiaGroup P G).subgroupOf (decompositionGroup P G)).subtype ∧
      Function.MulExact
        ((inertiaGroup P G).subgroupOf (decompositionGroup P G)).subtype
        (residueStabilizerHom p P G) ∧
      Function.Surjective (residueStabilizerHom p P G)

def dedekindRamification_decompositionQuotientInertiaEquivResidueGalois
    (p : Ideal A) (P : Ideal B) [P.IsPrime] [P.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B]
    [Algebra.IsInvariant A B G] :
    decompositionGroup P G ⧸
        (inertiaGroup P G).subgroupOf (decompositionGroup P G) ≃*
      (B ⧸ P) ≃ₐ[A ⧸ p] B ⧸ P

theorem dedekindRamification_residueAction_injective_of_inertiaGroup_eq_bot
    (p : Ideal A) (P : Ideal B) [P.LiesOver p]
    (G : Type*) [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (hI : inertiaGroup P G = ⊥) :
    Function.Injective (residueStabilizerHom p P G)

theorem dedekindRamification_residueAction_bijective_of_inertiaGroup_eq_bot
    (p : Ideal A) (P : Ideal B) [P.IsPrime] [P.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B]
    [Algebra.IsInvariant A B G] (hI : inertiaGroup P G = ⊥) :
    Function.Bijective (residueStabilizerHom p P G)

def dedekindRamification_decompositionGroupEquivResidueGalois_of_inertiaGroup_eq_bot
    (p : Ideal A) (P : Ideal B) [P.IsPrime] [P.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B]
    [Algebra.IsInvariant A B G] (hI : inertiaGroup P G = ⊥) :
    decompositionGroup P G ≃*
      (B ⧸ P) ≃ₐ[A ⧸ p] B ⧸ P

def dedekindRamification_residueGaloisEmbeddingIntoG_of_inertiaGroup_eq_bot
    (p : Ideal A) (P : Ideal B) [P.IsPrime] [P.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B]
    [Algebra.IsInvariant A B G] (hI : inertiaGroup P G = ⊥) :
    ((B ⧸ P) ≃ₐ[A ⧸ p] B ⧸ P) →* G

theorem dedekindRamification_residueGaloisEmbeddingIntoG_of_inertiaGroup_eq_bot_injective
    (p : Ideal A) (P : Ideal B) [P.IsPrime] [P.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B]
    [Algebra.IsInvariant A B G] (hI : inertiaGroup P G = ⊥) :
    Function.Injective
      (dedekindRamification_residueGaloisEmbeddingIntoG_of_inertiaGroup_eq_bot p P G hI)

theorem dedekindRamification_galois_prime_decomposition
    [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B]
    [IsTorsionFree A B]
    (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥)
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] :
    Ideal.map (algebraMap A B) p =
      ∏ P ∈ p.primesOver B, P ^ Ideal.ramificationIdxIn p B

theorem dedekindRamification_galois_fundamental_identity
    [IsDedekindDomain A] (p : Ideal A) [p.IsMaximal] (_hpb : p ≠ ⊥)
    (B : Type*) [CommRing B] [IsDedekindDomain B] [Algebra A B]
    [Module.Finite A B] [IsTorsionFree A B]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] :
    (p.primesOver B).ncard *
        (Ideal.ramificationIdxIn p B * Ideal.inertiaDegIn p B) =
      Nat.card G

theorem dedekindRamification_unramified_decomposition_law
    [IsDedekindDomain A]
    (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥)
    (B : Type*) [CommRing B] [IsDedekindDomain B] [Algebra A B]
    [Module.Finite A B] [IsTorsionFree A B]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B]
    (hunramified : Ideal.ramificationIdxIn p B = 1) :
    (p.primesOver B).ncard * Ideal.inertiaDegIn p B =
      Nat.card G

theorem
    dedekindRamification_unramified_numberOfPrimes_eq_degree_div_inertiaDegree
    [IsDedekindDomain A]
    (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥)
    (B : Type*) [CommRing B] [IsDedekindDomain B] [Algebra A B]
    [Module.Finite A B] [IsTorsionFree A B]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B]
    (hunramified : Ideal.ramificationIdxIn p B = 1) :
    (p.primesOver B).ncard =
      Nat.card G / Ideal.inertiaDegIn p B

theorem dedekindRamification_ncard_primesOver_mul_decomposition_card
    (p : Ideal A) (P : Ideal B) [P.IsPrime] [P.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] :
    (p.primesOver B).ncard * Nat.card (decompositionGroup P G) =
      Nat.card G

theorem dedekindRamification_decomposition_card_eq_ramificationIdxIn_mul_inertiaDegIn
    [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B]
    [IsTorsionFree A B]
    (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥)
    (P : Ideal B) [P.IsPrime] [P.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] :
    Nat.card (decompositionGroup P G) =
      Ideal.ramificationIdxIn p B * Ideal.inertiaDegIn p B

theorem dedekindRamification_decompositionQuotientInertia_card_eq_inertiaDeg
    (p : Ideal A) [p.IsMaximal]
    (P : Ideal B) [P.IsPrime] [P.LiesOver p] [P.IsMaximal]
    [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] :
  Nat.card
        (decompositionGroup P G ⧸
          (inertiaGroup P G).subgroupOf (decompositionGroup P G)) =
      P.inertiaDeg A

theorem dedekindRamification_decompositionQuotientInertia_card_eq_inertiaDegIn
    (p : Ideal A) [p.IsMaximal]
    (P : Ideal B) [P.IsPrime] [P.LiesOver p] [P.IsMaximal]
    [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] :
    Nat.card
        (decompositionGroup P G ⧸
          (inertiaGroup P G).subgroupOf (decompositionGroup P G)) =
      Ideal.inertiaDegIn p B

theorem dedekindRamification_decomposition_card_eq_quotient_card_mul_inertia_card
    (P : Ideal B) (G : Type*) [Group G] [MulSemiringAction G B] :
    Nat.card (decompositionGroup P G) =
      Nat.card
          (decompositionGroup P G ⧸
            (inertiaGroup P G).subgroupOf (decompositionGroup P G)) *
        Nat.card (inertiaGroup P G)

theorem dedekindRamification_decomposition_card_eq_inertia_card_mul_inertiaDegIn
    (p : Ideal A) [p.IsMaximal]
    (P : Ideal B) [P.IsPrime] [P.LiesOver p] [P.IsMaximal]
    [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] :
    Nat.card (decompositionGroup P G) =
      Nat.card (inertiaGroup P G) * Ideal.inertiaDegIn p B

theorem dedekindRamification_inertia_card_eq_ramificationIdxIn
    [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B]
    [IsTorsionFree A B]
    (p : Ideal A) (P : Ideal B) [P.LiesOver p] [P.IsMaximal]
    [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] (hp : p ≠ ⊥) :
    Nat.card (P.toAddSubgroup.inertia G) = Ideal.ramificationIdxIn p B