@[reducible, inline]

abbrev IsLeftGModule (G : Type u_1) (M : Type u_2) [Group G] [AddCommGroup M] [DistribMulAction G M] : Prop

theorem left_gmodule_smul_add (G : Type u_1) (M : Type u_2) [Group G] [AddCommGroup M] [DistribMulAction G M] (σ : G) (a b : M) : σ • (a + b) = σ • a + σ • b

theorem galois_action_fractional_ideal {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (σ : G) (I : Ideal B) (x : B) : x ∈ σ • I ↔ σ⁻¹ • x ∈ I

theorem galois_action_mul_compat {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (σ : G) (I J : Ideal B) : σ • (I * J) = σ • I * σ • J

@[reducible]

def galois_gmodule_fractional_ideals {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] : MulSemiringAction G (Ideal B)

theorem galois_action_preserves_prime {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (σ : G) (I : Ideal B) [I.IsPrime] : (σ • I).IsPrime

theorem galois_smul_ideal_mem_iff {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (σ : G) (I : Ideal B) (x : B) : x ∈ σ • I ↔ σ⁻¹ • x ∈ I

@[deprecated galois_smul_ideal_mem_iff (since := "2025-05-04")]

theorem theorem_7_2_sigma_preserves_fractional_ideal {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (σ : G) (I : Ideal B) (x : B) : x ∈ σ • I ↔ σ⁻¹ • x ∈ I

theorem galois_smul_ideal_mul {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (σ : G) (I J : Ideal B) : σ • (I * J) = σ • I * σ • J

@[deprecated galois_smul_ideal_mul (since := "2025-05-04")]

theorem theorem_7_2_gmodule_structure {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (σ : G) (I J : Ideal B) : σ • (I * J) = σ • I * σ • J

theorem galois_smul_isPrime {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (σ : G) (I : Ideal B) [I.IsPrime] : (σ • I).IsPrime

@[deprecated galois_smul_isPrime (since := "2025-05-04")]

theorem theorem_7_2_gset_on_primes {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (σ : G) (I : Ideal B) [I.IsPrime] : (σ • I).IsPrime

theorem galois_smul_ideal_add {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (σ : G) (I J : Ideal B) : σ • (I + J) = σ • I + σ • J

@[deprecated galois_smul_ideal_add (since := "2025-05-04")]

theorem theorem_7_2_gmodule_add_compat {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (σ : G) (I J : Ideal B) : σ • (I + J) = σ • I + σ • J

theorem galois_action_on_ideals_isPretransitive {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B] : MulAction.IsPretransitive G ↑(p.primesOver B)

theorem galois_transitive_on_primes_above {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B] (P Q : Ideal B) [P.IsPrime] [P.LiesOver p] [Q.IsPrime] [Q.LiesOver p] : ∃ (σ : G), σ • P = Q

theorem ramificationIdx_constant_of_isGaloisGroup {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B] (P Q : Ideal B) [P.IsPrime] [P.LiesOver p] [Q.IsPrime] [Q.LiesOver p] : p.ramificationIdx P = p.ramificationIdx Q

theorem inertiaDeg_constant_of_isGaloisGroup {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B] (P Q : Ideal B) [P.IsPrime] [P.LiesOver p] [Q.IsPrime] [Q.LiesOver p] : p.inertiaDeg P = p.inertiaDeg Q

theorem efg_eq_degree {A : Type u_1} [CommRing A] [IsDedekindDomain A] {p : Ideal A} [p.IsMaximal] (B : Type u_2) [CommRing B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B] (hp : p ≠ ⊥) : (p.primesOver B).ncard * (p.ramificationIdxIn B * p.inertiaDegIn B) = Nat.card G

@[reducible, inline]

abbrev decompositionGroup {B : Type u_2} [CommRing B] (G : Type u_3) [Group G] [MulSemiringAction G B] (Q : Ideal B) : Subgroup G

theorem mem_decompositionGroup_iff {B : Type u_2} [CommRing B] (G : Type u_3) [Group G] [MulSemiringAction G B] (Q : Ideal B) (σ : G) : σ ∈ decompositionGroup G Q ↔ σ • Q = Q

theorem decompositionGroup_conjugate {B : Type u_2} [CommRing B] (G : Type u_3) [Group G] [MulSemiringAction G B] (P : Ideal B) (σ : G) : decompositionGroup G (σ • P) = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj σ)) (decompositionGroup G P)

theorem card_decompositionGroup_eq_ef {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] (hp : p ≠ ⊥) (P : Ideal B) [P.LiesOver p] [P.IsMaximal] [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)] : Nat.card ↥(decompositionGroup G P) = p.ramificationIdxIn B * p.inertiaDegIn B

theorem index_decompositionGroup_eq_g {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [p.IsMaximal] (hp : p ≠ ⊥) (P : Ideal B) [P.LiesOver p] [P.IsMaximal] [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)] : (decompositionGroup G P).index = (p.primesOver B).ncard

noncomputable def residueField_surjection {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B] [Algebra.IsInvariant A B G] (Q : Ideal B) [Q.IsPrime] [Q.LiesOver p] : ↥(MulAction.stabilizer G Q) ⧸ (Ideal.inertia G Q).subgroupOf (MulAction.stabilizer G Q) ≃* (B ⧸ Q) ≃ₐ[A ⧸ p] B ⧸ Q

theorem residueField_normal {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [Algebra.IsInvariant A B G] (Q : Ideal B) [Q.LiesOver p] [p.IsMaximal] [Q.IsMaximal] : Normal (A ⧸ p) (B ⧸ Q)

@[reducible, inline]

abbrev inertiaGroup {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (Q : Ideal B) : Subgroup G

theorem inertiaGroup_le_decompositionGroup {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (Q : Ideal B) : inertiaGroup G Q ≤ decompositionGroup G Q

noncomputable def decompositionQuotientInertiaEquiv {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B] (Q : Ideal B) [Q.IsPrime] [Q.LiesOver p] : ↥(MulAction.stabilizer G Q) ⧸ (Ideal.inertia G Q).subgroupOf (MulAction.stabilizer G Q) ≃* (B ⧸ Q) ≃ₐ[A ⧸ p] B ⧸ Q

@[deprecated decompositionQuotientInertiaEquiv (since := "2025-05-04")]

noncomputable def exact_sequence_inertia_decomposition {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B] (Q : Ideal B) [Q.IsPrime] [Q.LiesOver p] : ↥(MulAction.stabilizer G Q) ⧸ (Ideal.inertia G Q).subgroupOf (MulAction.stabilizer G Q) ≃* (B ⧸ Q) ≃ₐ[A ⧸ p] B ⧸ Q

theorem card_inertiaGroup_eq_e_mul_insepDegree {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [p.IsMaximal] (hp : p ≠ ⊥) (P : Ideal B) [P.LiesOver p] [P.IsMaximal] : Nat.card ↥(inertiaGroup G P) = p.ramificationIdxIn B * Field.finInsepDegree (A ⧸ p) (B ⧸ P)

theorem card_inertiaGroup_eq_e {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] (hp : p ≠ ⊥) (P : Ideal B) [P.LiesOver p] [P.IsMaximal] [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)] : Nat.card ↥(inertiaGroup G P) = p.ramificationIdxIn B

theorem finrank_over_inertiaField_eq_ramificationIdx (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} (P : Ideal B) [P.LiesOver p] [FiniteDimensional K L] [MulSemiringAction Gal(L/K) B] [IsGaloisGroup Gal(L/K) A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Ring.HasFiniteQuotients A] [P.IsMaximal] (E : Type u_5) [Field E] [Algebra E L] [IsInertiaField K L P E] (hp : p ≠ ⊥) : Module.finrank E L = p.ramificationIdxIn B

theorem finrank_inertiaField_over_decompositionField_eq_inertiaDeg (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} (P : Ideal B) [P.LiesOver p] [FiniteDimensional K L] [MulSemiringAction Gal(L/K) B] [IsGaloisGroup Gal(L/K) A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Ring.HasFiniteQuotients A] [P.IsMaximal] (D : Type u_5) [Field D] [Algebra D L] [IsDecompositionField K L P D] (E : Type u_6) [Field E] [Algebra E L] [IsInertiaField K L P E] [IsGalois K L] [Algebra K D] [Algebra K E] [Algebra D E] [IsScalarTower K D E] [IsScalarTower K E L] [IsScalarTower K D L] (hp : p ≠ ⊥) : Module.finrank D E = p.inertiaDegIn B

theorem finrank_decompositionField_eq_ncard_primesOver (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} (P : Ideal B) [P.LiesOver p] [FiniteDimensional K L] [MulSemiringAction Gal(L/K) B] [IsGaloisGroup Gal(L/K) A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Ring.HasFiniteQuotients A] [P.IsMaximal] (D : Type u_5) [Field D] [Algebra D L] [IsDecompositionField K L P D] [IsGalois K L] [Algebra K D] [IsScalarTower K D L] (hp : p ≠ ⊥) : Module.finrank K D = (p.primesOver B).ncard

theorem finrank_over_decompositionField_eq_ef (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} (P : Ideal B) [P.LiesOver p] [FiniteDimensional K L] [MulSemiringAction Gal(L/K) B] [IsGaloisGroup Gal(L/K) A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Ring.HasFiniteQuotients A] [P.IsMaximal] (D : Type u_5) [Field D] [Algebra D L] [IsDecompositionField K L P D] (hp : p ≠ ⊥) : Module.finrank D L = p.ramificationIdxIn B * p.inertiaDegIn B

theorem stabilizer_subgroupOf_and_inertia_subgroupOf {B : Type u_1} [Ring B] (G : Type u_2) [Group G] [MulSemiringAction G B] (Q : Ideal B) (H : Subgroup G) : (MulAction.stabilizer G Q).subgroupOf H = MulAction.stabilizer (↥H) Q ∧ (Ideal.inertia G Q).subgroupOf H = Ideal.inertia (↥H) Q

theorem decompositionGroup_subgroupOf {B : Type u_1} [Ring B] (G : Type u_2) [Group G] [MulSemiringAction G B] (Q : Ideal B) (H : Subgroup G) : (MulAction.stabilizer G Q).subgroupOf H = MulAction.stabilizer (↥H) Q

theorem inertiaGroup_subgroupOf {B : Type u_1} [Ring B] (G : Type u_2) [Group G] [MulSemiringAction G B] (Q : Ideal B) (H : Subgroup G) : (Ideal.inertia G Q).subgroupOf H = Ideal.inertia (↥H) Q

theorem inertiaField_is_fixedField_of_inertiaGroup (K : Type u_1) (L : Type u_2) {B : Type u_3} [Field K] [Field L] [Algebra K L] [CommRing B] [MulSemiringAction Gal(L/K) B] (P : Ideal B) [IsGalois K L] : IsInertiaField K L P ↥(FixedPoints.intermediateField ↥(Ideal.inertia Gal(L/K) P))

theorem decompositionField_is_fixedField_of_decompositionGroup (K : Type u_1) (L : Type u_2) {B : Type u_3} [Field K] [Field L] [Algebra K L] [CommRing B] [MulSemiringAction Gal(L/K) B] (P : Ideal B) [IsGalois K L] : IsDecompositionField K L P ↥(FixedPoints.intermediateField ↥(MulAction.stabilizer Gal(L/K) P))

theorem Subgroup.le_of_card_subgroupOf_eq' {G : Type u_4} [Group G] {H K : Subgroup G} [Finite ↥H] (h : Nat.card ↥(H.subgroupOf K) = Nat.card ↥H) : H ≤ K

theorem card_inertia_tower_formula {K : Type u_4} {L : Type u_5} {B : Type u_6} [Field K] [Field L] [Algebra K L] [CommRing B] [MulSemiringAction Gal(L/K) B] [IsDedekindDomain B] [FaithfulSMul Gal(L/K) B] {A : Type u_7} [CommRing A] [IsDedekindDomain A] [Algebra A B] (P : Ideal B) [IsGalois K L] [FiniteDimensional K L] [P.IsMaximal] (p : Ideal A) [p.IsMaximal] (E : IntermediateField K L) (C_E : Type u_8) [CommRing C_E] [IsDedekindDomain C_E] [Algebra A C_E] [Algebra A ↥E] [Algebra C_E ↥E] [IsIntegralClosure C_E A ↥E] (P_E : Ideal C_E) [P_E.IsMaximal] [P_E.LiesOver p] [Algebra C_E B] [IsScalarTower A C_E B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite C_E B] [Module.IsTorsionFree C_E B] [Module.IsTorsionFree A C_E] [P.LiesOver p] [P.LiesOver P_E] [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)] [Algebra.IsSeparable (C_E ⧸ P_E) (B ⧸ P)] [IsGaloisGroup Gal(L/K) A B] [IsGaloisGroup (↥E.fixingSubgroup) C_E B] (hp : p ≠ ⊥) (hP_E : P_E ≠ ⊥) : p.ramificationIdx P_E * Nat.card ↥(Ideal.inertia (↥E.fixingSubgroup) P) = Nat.card ↥(Ideal.inertia Gal(L/K) P)

theorem ramificationIdx_mul_card_inertia_subgroupOf {K : Type u_4} {L : Type u_5} {B : Type u_6} [Field K] [Field L] [Algebra K L] [CommRing B] [MulSemiringAction Gal(L/K) B] [IsDedekindDomain B] [FaithfulSMul Gal(L/K) B] {A : Type u_7} [CommRing A] [IsDedekindDomain A] [Algebra A B] (P : Ideal B) [IsGalois K L] [FiniteDimensional K L] [P.IsMaximal] (p : Ideal A) [p.IsMaximal] (E : IntermediateField K L) (C_E : Type u_8) [CommRing C_E] [IsDedekindDomain C_E] [Algebra A C_E] [Algebra A ↥E] [Algebra C_E ↥E] [IsIntegralClosure C_E A ↥E] (P_E : Ideal C_E) [P_E.IsMaximal] [P_E.LiesOver p] [Algebra C_E B] [IsScalarTower A C_E B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite C_E B] [Module.IsTorsionFree C_E B] [Module.IsTorsionFree A C_E] [P.LiesOver p] [P.LiesOver P_E] [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)] [Algebra.IsSeparable (C_E ⧸ P_E) (B ⧸ P)] [IsGaloisGroup Gal(L/K) A B] [IsGaloisGroup (↥E.fixingSubgroup) C_E B] (hp : p ≠ ⊥) (hP_E : P_E ≠ ⊥) : p.ramificationIdx P_E * Nat.card ↥((Ideal.inertia Gal(L/K) P).subgroupOf E.fixingSubgroup) = Nat.card ↥(Ideal.inertia Gal(L/K) P)

theorem ramificationIdx_eq_one_iff_inertia_le_fixingSubgroup (K : Type u_1) (L : Type u_2) {B : Type u_3} [Field K] [Field L] [Algebra K L] [CommRing B] [MulSemiringAction Gal(L/K) B] [IsDedekindDomain B] [FaithfulSMul Gal(L/K) B] {A : Type u_4} [CommRing A] [IsDedekindDomain A] [Algebra A B] (P : Ideal B) [IsGalois K L] [FiniteDimensional K L] [P.IsMaximal] (p : Ideal A) [p.IsMaximal] (E : IntermediateField K L) (C_E : Type u_5) [CommRing C_E] [IsDedekindDomain C_E] [Algebra A C_E] [Algebra A ↥E] [Algebra C_E ↥E] [IsIntegralClosure C_E A ↥E] (P_E : Ideal C_E) [P_E.IsMaximal] [P_E.LiesOver p] [Algebra C_E B] [IsScalarTower A C_E B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite C_E B] [Module.IsTorsionFree C_E B] [Module.IsTorsionFree A C_E] [P.LiesOver p] [P.LiesOver P_E] [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)] [Algebra.IsSeparable (C_E ⧸ P_E) (B ⧸ P)] [IsGaloisGroup Gal(L/K) A B] [IsGaloisGroup (↥E.fixingSubgroup) C_E B] (hp : p ≠ ⊥) (hP_E : P_E ≠ ⊥) : p.ramificationIdx P_E = 1 ↔ Ideal.inertia Gal(L/K) P ≤ E.fixingSubgroup

theorem e_eq_one_iff_le_inertiaField (K : Type u_1) (L : Type u_2) {B : Type u_3} [Field K] [Field L] [Algebra K L] [CommRing B] [MulSemiringAction Gal(L/K) B] [IsDedekindDomain B] [FaithfulSMul Gal(L/K) B] {A : Type u_4} [CommRing A] [IsDedekindDomain A] [Algebra A B] (P : Ideal B) [IsGalois K L] [FiniteDimensional K L] [P.IsMaximal] (p : Ideal A) [p.IsMaximal] (E : IntermediateField K L) (C_E : Type u_5) [CommRing C_E] [IsDedekindDomain C_E] [Algebra A C_E] [Algebra A ↥E] [Algebra C_E ↥E] [IsIntegralClosure C_E A ↥E] (P_E : Ideal C_E) [P_E.IsMaximal] [P_E.LiesOver p] [Algebra C_E B] [IsScalarTower A C_E B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite C_E B] [Module.IsTorsionFree C_E B] [Module.IsTorsionFree A C_E] [P.LiesOver p] [P.LiesOver P_E] [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)] [Algebra.IsSeparable (C_E ⧸ P_E) (B ⧸ P)] [IsGaloisGroup Gal(L/K) A B] [IsGaloisGroup (↥E.fixingSubgroup) C_E B] (hp : p ≠ ⊥) (hP_E : P_E ≠ ⊥) : p.ramificationIdx P_E = 1 ↔ E ≤ IntermediateField.fixedField (Ideal.inertia Gal(L/K) P)

theorem ef_mul_card_stabilizer_subgroupOf (K : Type u_1) (L : Type u_2) {B : Type u_3} [Field K] [Field L] [Algebra K L] [CommRing B] [MulSemiringAction Gal(L/K) B] [IsDedekindDomain B] [FaithfulSMul Gal(L/K) B] {A : Type u_4} [CommRing A] [IsDedekindDomain A] [Algebra A B] (P : Ideal B) [IsGalois K L] [FiniteDimensional K L] [P.IsMaximal] (p : Ideal A) [p.IsMaximal] (E : IntermediateField K L) (C_E : Type u_5) [CommRing C_E] [IsDedekindDomain C_E] [Algebra A C_E] [Algebra A ↥E] [Algebra C_E ↥E] [IsIntegralClosure C_E A ↥E] (P_E : Ideal C_E) [P_E.IsMaximal] [P_E.LiesOver p] [Algebra C_E B] [IsScalarTower A C_E B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite C_E B] [Module.IsTorsionFree C_E B] [Module.IsTorsionFree A C_E] [P.LiesOver p] [P.LiesOver P_E] [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)] [Algebra.IsSeparable (C_E ⧸ P_E) (B ⧸ P)] [IsGaloisGroup Gal(L/K) A B] [IsGaloisGroup (↥E.fixingSubgroup) C_E B] (hp : p ≠ ⊥) (hP_E : P_E ≠ ⊥) : p.ramificationIdx P_E * p.inertiaDeg P_E * Nat.card ↥((MulAction.stabilizer Gal(L/K) P).subgroupOf E.fixingSubgroup) = Nat.card ↥(MulAction.stabilizer Gal(L/K) P)

theorem ef_eq_one_iff_stabilizer_le_fixingSubgroup (K : Type u_1) (L : Type u_2) {B : Type u_3} [Field K] [Field L] [Algebra K L] [CommRing B] [MulSemiringAction Gal(L/K) B] [IsDedekindDomain B] [FaithfulSMul Gal(L/K) B] {A : Type u_4} [CommRing A] [IsDedekindDomain A] [Algebra A B] (P : Ideal B) [IsGalois K L] [FiniteDimensional K L] [P.IsMaximal] (p : Ideal A) [p.IsMaximal] (E : IntermediateField K L) (C_E : Type u_5) [CommRing C_E] [IsDedekindDomain C_E] [Algebra A C_E] [Algebra A ↥E] [Algebra C_E ↥E] [IsIntegralClosure C_E A ↥E] (P_E : Ideal C_E) [P_E.IsMaximal] [P_E.LiesOver p] [Algebra C_E B] [IsScalarTower A C_E B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite C_E B] [Module.IsTorsionFree C_E B] [Module.IsTorsionFree A C_E] [P.LiesOver p] [P.LiesOver P_E] [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)] [Algebra.IsSeparable (C_E ⧸ P_E) (B ⧸ P)] [IsGaloisGroup Gal(L/K) A B] [IsGaloisGroup (↥E.fixingSubgroup) C_E B] (hp : p ≠ ⊥) (hP_E : P_E ≠ ⊥) : p.ramificationIdx P_E = 1 ∧ p.inertiaDeg P_E = 1 ↔ MulAction.stabilizer Gal(L/K) P ≤ E.fixingSubgroup

theorem ef_eq_one_iff_le_decompositionField (K : Type u_1) (L : Type u_2) {B : Type u_3} [Field K] [Field L] [Algebra K L] [CommRing B] [MulSemiringAction Gal(L/K) B] [IsDedekindDomain B] [FaithfulSMul Gal(L/K) B] {A : Type u_4} [CommRing A] [IsDedekindDomain A] [Algebra A B] (P : Ideal B) [IsGalois K L] [FiniteDimensional K L] [P.IsMaximal] (p : Ideal A) [p.IsMaximal] (E : IntermediateField K L) (C_E : Type u_5) [CommRing C_E] [IsDedekindDomain C_E] [Algebra A C_E] [Algebra A ↥E] [Algebra C_E ↥E] [IsIntegralClosure C_E A ↥E] (P_E : Ideal C_E) [P_E.IsMaximal] [P_E.LiesOver p] [Algebra C_E B] [IsScalarTower A C_E B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite C_E B] [Module.IsTorsionFree C_E B] [Module.IsTorsionFree A C_E] [P.LiesOver p] [P.LiesOver P_E] [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)] [Algebra.IsSeparable (C_E ⧸ P_E) (B ⧸ P)] [IsGaloisGroup Gal(L/K) A B] [IsGaloisGroup (↥E.fixingSubgroup) C_E B] (hp : p ≠ ⊥) (hP_E : P_E ≠ ⊥) : p.ramificationIdx P_E = 1 ∧ p.inertiaDeg P_E = 1 ↔ E ≤ IntermediateField.fixedField (MulAction.stabilizer Gal(L/K) P)

theorem e_ef_eq_one_iff_le_inertiaField_decompositionField (K : Type u_1) (L : Type u_2) {B : Type u_3} [Field K] [Field L] [Algebra K L] [CommRing B] [MulSemiringAction Gal(L/K) B] [IsDedekindDomain B] [FaithfulSMul Gal(L/K) B] {A : Type u_4} [CommRing A] [IsDedekindDomain A] [Algebra A B] (P : Ideal B) [IsGalois K L] [FiniteDimensional K L] [P.IsMaximal] (p : Ideal A) [p.IsMaximal] (E : IntermediateField K L) (C_E : Type u_5) [CommRing C_E] [IsDedekindDomain C_E] [Algebra A C_E] [Algebra A ↥E] [Algebra C_E ↥E] [IsIntegralClosure C_E A ↥E] (P_E : Ideal C_E) [P_E.IsMaximal] [P_E.LiesOver p] [Algebra C_E B] [IsScalarTower A C_E B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite C_E B] [Module.IsTorsionFree C_E B] [Module.IsTorsionFree A C_E] [P.LiesOver p] [P.LiesOver P_E] [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)] [Algebra.IsSeparable (C_E ⧸ P_E) (B ⧸ P)] [IsGaloisGroup Gal(L/K) A B] [IsGaloisGroup (↥E.fixingSubgroup) C_E B] (hp : p ≠ ⊥) (hP_E : P_E ≠ ⊥) : (p.ramificationIdx P_E = 1 ↔ E ≤ IntermediateField.fixedField (Ideal.inertia Gal(L/K) P)) ∧ (p.ramificationIdx P_E = 1 ∧ p.inertiaDeg P_E = 1 ↔ E ≤ IntermediateField.fixedField (MulAction.stabilizer Gal(L/K) P))

theorem inertiaGroup_normal_in_decompositionGroup {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (G : Type u_3) [Group G] [MulSemiringAction G B] [SMulCommClass G A B] [Algebra.IsInvariant A B G] (Q : Ideal B) [Q.IsPrime] : ((Ideal.inertia G Q).subgroupOf (MulAction.stabilizer G Q)).Normal

theorem isGalois_inertiaField_normalClosure (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsGalois K L] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra B L] [MulSemiringAction Gal(L/K) B] (P : Ideal B) : IsGalois K ↥(IntermediateField.fixedField (Subgroup.normalClosure ↑(Ideal.inertia Gal(L/K) P)))

theorem isGalois_decompositionField_normalClosure (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsGalois K L] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra B L] [MulSemiringAction Gal(L/K) B] (P : Ideal B) : IsGalois K ↥(IntermediateField.fixedField (Subgroup.normalClosure ↑(MulAction.stabilizer Gal(L/K) P)))

theorem normalClosure_le_iff_forall_conj {G : Type u_3} [Group G] (H N : Subgroup G) : Subgroup.normalClosure ↑H ≤ N ↔ ∀ (g : G), Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H ≤ N

theorem normalClosure_stabilizer_le_iff {G : Type u_3} [Group G] {α : Type u_4} [MulAction G α] (a : α) (N : Subgroup G) : Subgroup.normalClosure ↑(MulAction.stabilizer G a) ≤ N ↔ ∀ (g : G), MulAction.stabilizer G (g • a) ≤ N

theorem Ideal.IsMaximal.smul {G : Type u_3} [Group G] {B : Type u_4} [CommRing B] [MulSemiringAction G B] {P : Ideal B} (hP : P.IsMaximal) (g : G) : (g • P).IsMaximal

theorem inertia_smul_eq_inertia_map_conj {G : Type u_3} {B : Type u_4} [Group G] [CommRing B] [MulSemiringAction G B] (P : Ideal B) (σ : G) : Ideal.inertia G (σ • P) = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj σ)) (Ideal.inertia G P)

theorem normalClosure_inertia_le_iff {G : Type u_3} {B : Type u_4} [Group G] [CommRing B] [MulSemiringAction G B] (P : Ideal B) (N : Subgroup G) : Subgroup.normalClosure ↑(Ideal.inertia G P) ≤ N ↔ ∀ (σ : G), Ideal.inertia G (σ • P) ≤ N

theorem unramified_all_primes_iff_le_inertiaField_normalClosure (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra B L] [MulSemiringAction Gal(L/K) B] [FaithfulSMul Gal(L/K) B] {A : Type u_4} [CommRing A] [IsDedekindDomain A] [Algebra A B] [Algebra.IsIntegral A B] [SMulCommClass Gal(L/K) A B] (P : Ideal B) [P.IsMaximal] (p : Ideal A) [p.IsMaximal] [P.LiesOver p] (E : IntermediateField K L) (C_E : Type u_5) [CommRing C_E] [IsDedekindDomain C_E] [Algebra A C_E] [Algebra C_E B] [IsScalarTower A C_E B] [Algebra A ↥E] [Algebra C_E ↥E] [IsIntegralClosure C_E A ↥E] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite C_E B] [Module.IsTorsionFree C_E B] [Module.IsTorsionFree A C_E] [IsGaloisGroup Gal(L/K) A B] [IsGaloisGroup (↥E.fixingSubgroup) C_E B] (hp : p ≠ ⊥) (h_sep_A : ∀ (P' : Ideal B) [P'.IsMaximal] [inst : P'.LiesOver p], Algebra.IsSeparable (A ⧸ p) (B ⧸ P')) (h_sep_C : ∀ (Q' : Ideal C_E) (P' : Ideal B) [Q'.IsMaximal] [P'.IsMaximal] [Q'.LiesOver p] [inst : P'.LiesOver Q'], Algebra.IsSeparable (C_E ⧸ Q') (B ⧸ P')) (h_exists_smul : ∀ (Q' : Ideal C_E) [Q'.IsMaximal] [Q'.LiesOver p], ∃ (σ : Gal(L/K)), (σ • P).LiesOver Q') (hQ_ne_bot : ∀ (Q' : Ideal C_E) [Q'.IsMaximal] [Q'.LiesOver p], Q' ≠ ⊥) : (∀ (Q : Ideal C_E) [Q.IsMaximal] [Q.LiesOver p], p.ramificationIdx Q = 1) ↔ E ≤ IntermediateField.fixedField (Subgroup.normalClosure ↑(Ideal.inertia Gal(L/K) P))

theorem splitsCompletely_all_primes_iff_le_decompositionField_normalClosure (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra B L] [MulSemiringAction Gal(L/K) B] [FaithfulSMul Gal(L/K) B] {A : Type u_4} [CommRing A] [IsDedekindDomain A] [Algebra A B] [Algebra.IsIntegral A B] [SMulCommClass Gal(L/K) A B] (P : Ideal B) [P.IsMaximal] (p : Ideal A) [p.IsMaximal] [P.LiesOver p] (E : IntermediateField K L) (C_E : Type u_5) [CommRing C_E] [IsDedekindDomain C_E] [Algebra A C_E] [Algebra C_E B] [IsScalarTower A C_E B] [Algebra A ↥E] [Algebra C_E ↥E] [IsIntegralClosure C_E A ↥E] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite C_E B] [Module.IsTorsionFree C_E B] [Module.IsTorsionFree A C_E] [IsGaloisGroup Gal(L/K) A B] [IsGaloisGroup (↥E.fixingSubgroup) C_E B] (hp : p ≠ ⊥) (h_sep_A : ∀ (P' : Ideal B) [P'.IsMaximal] [inst : P'.LiesOver p], Algebra.IsSeparable (A ⧸ p) (B ⧸ P')) (h_sep_C : ∀ (Q' : Ideal C_E) (P' : Ideal B) [Q'.IsMaximal] [P'.IsMaximal] [Q'.LiesOver p] [inst : P'.LiesOver Q'], Algebra.IsSeparable (C_E ⧸ Q') (B ⧸ P')) (h_exists_smul : ∀ (Q' : Ideal C_E) [Q'.IsMaximal] [Q'.LiesOver p], ∃ (σ : Gal(L/K)), (σ • P).LiesOver Q') (hQ_ne_bot : ∀ (Q' : Ideal C_E) [Q'.IsMaximal] [Q'.LiesOver p], Q' ≠ ⊥) : (∀ (Q : Ideal C_E) [Q.IsMaximal] [Q.LiesOver p], p.ramificationIdx Q = 1 ∧ p.inertiaDeg Q = 1) ↔ E ≤ IntermediateField.fixedField (Subgroup.normalClosure ↑(MulAction.stabilizer Gal(L/K) P))

def IsFrobeniusElement {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (σ : G) (Q : Ideal B) (q : ℕ) : Prop

theorem isFrobeniusElement_one {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (Q : Ideal B) : IsFrobeniusElement G 1 Q 1

noncomputable def frobeniusElement {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (Q : Ideal B) (q : ℕ) (hexists : ∃! σ : G, IsFrobeniusElement G σ Q q) : G

theorem frobeniusElement_spec {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (Q : Ideal B) (q : ℕ) (hexists : ∃! σ : G, IsFrobeniusElement G σ Q q) : IsFrobeniusElement G (frobeniusElement G Q q hexists) Q q

theorem frobeniusElement_unique {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (Q : Ideal B) (q : ℕ) (hexists : ∃! σ : G, IsFrobeniusElement G σ Q q) (σ : G) (hσ : IsFrobeniusElement G σ Q q) : σ = frobeniusElement G Q q hexists

theorem isFrobeniusElement_eq_isArithFrobAt {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (G : Type u_3) [Group G] [MulSemiringAction G B] [SMulCommClass G A B] (σ : G) (Q : Ideal B) : IsFrobeniusElement G σ Q (Nat.card (A ⧸ Ideal.under A Q)) ↔ IsArithFrobAt A σ Q

theorem frobenius_existsUnique_of_inertia_eq_bot {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (G : Type u_3) [Group G] [MulSemiringAction G B] [SMulCommClass G A B] [Finite G] [Algebra.IsInvariant A B G] (Q : Ideal B) [Q.IsPrime] [Finite (B ⧸ Q)] (hunr : Ideal.inertia G Q = ⊥) : ∃! σ : G, IsFrobeniusElement G σ Q (Nat.card (A ⧸ Ideal.under A Q))

theorem isFrobeniusElement_conj {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] {σ τ : G} {Q : Ideal B} {q : ℕ} (hσ : IsFrobeniusElement G σ Q q) : IsFrobeniusElement G (τ * σ * τ⁻¹) (τ • Q) q

theorem frobeniusElement_conjugate {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] {Q : Ideal B} {q : ℕ} (hexists_Q : ∃! σ : G, IsFrobeniusElement G σ Q q) (τ : G) (hexists_tQ : ∃! σ : G, IsFrobeniusElement G σ (τ • Q) q) : frobeniusElement G (τ • Q) q hexists_tQ = τ * frobeniusElement G Q q hexists_Q * τ⁻¹

noncomputable def frobeniusClass {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (Q : Ideal B) (q : ℕ) (hexists : ∃! σ : G, IsFrobeniusElement G σ Q q) : ConjClasses G

theorem frobeniusClass_eq_of_conjugate {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] {Q : Ideal B} {q : ℕ} (hexists_Q : ∃! σ : G, IsFrobeniusElement G σ Q q) (τ : G) (hexists_tQ : ∃! σ : G, IsFrobeniusElement G σ (τ • Q) q) : frobeniusClass G (τ • Q) q hexists_tQ = frobeniusClass G Q q hexists_Q

@[reducible, inline]

noncomputable abbrev artinSymbol {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (Q : Ideal B) (q : ℕ) (hexists : ∃! σ : G, IsFrobeniusElement G σ Q q) : G

theorem artinSymbol_eq_one_iff_frobeniusCondition {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] {Q : Ideal B} {q : ℕ} (hexists : ∃! σ : G, IsFrobeniusElement G σ Q q) : frobeniusElement G Q q hexists = 1 ↔ ∀ (x : B), x - x ^ q ∈ Q

theorem artinSymbol_eq_one_iff_decompositionGroup_trivial {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] {Q : Ideal B} {q : ℕ} (hexists : ∃! σ : G, IsFrobeniusElement G σ Q q) (hmem : frobeniusElement G Q q hexists ∈ MulAction.stabilizer G Q) (hgen : ∀ g ∈ MulAction.stabilizer G Q, ∃ (n : ℕ), g = frobeniusElement G Q q hexists ^ n) : frobeniusElement G Q q hexists = 1 ↔ MulAction.stabilizer G Q = ⊥

structure UnramifiedFrobeniusData {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (P : Ideal B) (q : ℕ) : Prop

• unique_exists : ∃! σ : G, IsFrobeniusElement G σ P q
• mem_stabilizer : frobeniusElement G P q ⋯ ∈ MulAction.stabilizer G P
• generates_stabilizer (g : G) : g ∈ MulAction.stabilizer G P → ∃ (n : ℕ), g = frobeniusElement G P q ⋯ ^ n

theorem decompositionGroup_trivial_iff_splitsCompletely {A : Type u_1} {B : Type u_2} [CommRing A] [IsDedekindDomain A] [CommRing B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] {p : Ideal A} [p.IsMaximal] (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B] (hp : p ≠ ⊥) (P : Ideal B) [P.LiesOver p] [P.IsMaximal] [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)] : MulAction.stabilizer G P = ⊥ ↔ (p.primesOver B).ncard = Nat.card G

theorem artinSymbol_trivial_iff_splitsCompletely {A : Type u_1} {B : Type u_2} [CommRing A] [IsDedekindDomain A] [CommRing B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] {p : Ideal A} [p.IsMaximal] (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B] (hp : p ≠ ⊥) (P : Ideal B) [P.LiesOver p] [P.IsMaximal] [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)] {q : ℕ} (hexists : ∃! σ : G, IsFrobeniusElement G σ P q) (hmem : frobeniusElement G P q hexists ∈ MulAction.stabilizer G P) (hgen : ∀ g ∈ MulAction.stabilizer G P, ∃ (n : ℕ), g = frobeniusElement G P q hexists ^ n) : frobeniusElement G P q hexists = 1 ↔ (p.primesOver B).ncard = Nat.card G

theorem artinSymbol_trivial_iff_splitsCompletely' {A : Type u_1} {B : Type u_2} [CommRing A] [IsDedekindDomain A] [CommRing B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] {p : Ideal A} [p.IsMaximal] (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B] (hp : p ≠ ⊥) (P : Ideal B) [P.LiesOver p] [P.IsMaximal] [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)] {q : ℕ} (hdata : UnramifiedFrobeniusData G P q) : frobeniusElement G P q ⋯ = 1 ↔ (p.primesOver B).ncard = Nat.card G

theorem Ideal.pow_sub_pow_mem {R : Type u_3} [CommRing R] (I : Ideal R) {a b : R} (n : ℕ) (h : a - b ∈ I) : a ^ n - b ^ n ∈ I

theorem isFrobeniusElement_pow {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] {σ : G} {Q : Ideal B} {q : ℕ} (hσ : IsFrobeniusElement G σ Q q) (f : ℕ) : IsFrobeniusElement G (σ ^ f) Q (q ^ f)

theorem artinSymbol_tower {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] {Q : Ideal B} {q f : ℕ} (hexists_q : ∃! σ : G, IsFrobeniusElement G σ Q q) (hexists_qf : ∃! σ : G, IsFrobeniusElement G σ Q (q ^ f)) : frobeniusElement G Q (q ^ f) hexists_qf = frobeniusElement G Q q hexists_q ^ f

theorem isFrobeniusElement_restriction {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] {C : Type u_3} [CommRing C] (H : Type u_4) [Group H] [MulSemiringAction H C] (ι : C →+* B) (ρ : G →* H) (hcompat : ∀ (g : G) (c : C), ι (ρ g • c) = g • ι c) {σ : G} {Q : Ideal B} {q : ℕ} (hσ : IsFrobeniusElement G σ Q q) : IsFrobeniusElement H (ρ σ) (Ideal.comap ι Q) q

theorem frobeniusElement_restriction {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] {C : Type u_3} [CommRing C] (H : Type u_4) [Group H] [MulSemiringAction H C] (ι : C →+* B) (ρ : G →* H) (hcompat : ∀ (g : G) (c : C), ι (ρ g • c) = g • ι c) {Q : Ideal B} {q : ℕ} (hexists_G : ∃! σ : G, IsFrobeniusElement G σ Q q) (hexists_H : ∃! τ : H, IsFrobeniusElement H τ (Ideal.comap ι Q) q) : frobeniusElement H (Ideal.comap ι Q) q hexists_H = ρ (frobeniusElement G Q q hexists_G)

theorem isFrobeniusElement_mul_inv_mem_inertia {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] {σ σ' : G} {Q : Ideal B} {n : ℕ} (h1 : IsFrobeniusElement G σ Q n) (h2 : IsFrobeniusElement G σ' Q n) : σ * σ'⁻¹ ∈ Ideal.inertia G Q

theorem frobenius_existsUnique_of_exists_of_inertia_eq_bot {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] {Q : Ideal B} {n : ℕ} {σ : G} (hσ : IsFrobeniusElement G σ Q n) (hunr : Ideal.inertia G Q = ⊥) : ∃! τ : G, IsFrobeniusElement G τ Q n

theorem frobeniusElement_tower_and_restriction_abstract {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] {C : Type u_3} [CommRing C] (H : Type u_4) [Group H] [MulSemiringAction H C] (ι : C →+* B) (ρ : G →* H) (hcompat : ∀ (g : G) (c : C), ι (ρ g • c) = g • ι c) {Q : Ideal B} {q f : ℕ} (hexists_q : ∃! σ : G, IsFrobeniusElement G σ Q q) (hexists_qf : ∃! σ : G, IsFrobeniusElement G σ Q (q ^ f)) (hexists_H : ∃! τ : H, IsFrobeniusElement H τ (Ideal.comap ι Q) q) : frobeniusElement G Q (q ^ f) hexists_qf = frobeniusElement G Q q hexists_q ^ f ∧ frobeniusElement H (Ideal.comap ι Q) q hexists_H = ρ (frobeniusElement G Q q hexists_q)

theorem frobeniusElement_tower_and_restriction {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] {A : Type u_3} [CommRing A] [Algebra A B] [SMulCommClass G A B] [Finite G] [Algebra.IsInvariant A B G] {C : Type u_4} [CommRing C] (H : Type u_5) [Group H] [MulSemiringAction H C] [Algebra A C] [SMulCommClass H A C] [Finite H] [Algebra.IsInvariant A C H] (ι : C →+* B) (ρ : G →* H) (hcompat : ∀ (g : G) (c : C), ι (ρ g • c) = g • ι c) {Q : Ideal B} [Q.IsPrime] [Finite (B ⧸ Q)] [(Ideal.comap ι Q).IsPrime] [Finite (C ⧸ Ideal.comap ι Q)] (hunr : Ideal.inertia G Q = ⊥) (hunr_H : Ideal.inertia H (Ideal.comap ι Q) = ⊥) (hunder : Ideal.under A (Ideal.comap ι Q) = Ideal.under A Q) {f : ℕ} : let q := Nat.card (A ⧸ Ideal.under A Q); have hexists_q := ⋯; have hexists_qf := ⋯; frobeniusElement G Q (q ^ f) hexists_qf = frobeniusElement G Q q hexists_q ^ f ∧ ∃ (hexists_H : ∃! τ : H, IsFrobeniusElement H τ (Ideal.comap ι Q) q), frobeniusElement H (Ideal.comap ι Q) q hexists_H = ρ (frobeniusElement G Q q hexists_q)

noncomputable def artinMap {A : Type u_1} [CommRing A] (G : Type u_2) [CommGroup G] {S : Set (Ideal A)} (artinSymbolPrime : { 𝔭 : Ideal A // 𝔭.IsPrime ∧ 𝔭 ∉ S } → G) : FreeAbelianGroup { 𝔭 : Ideal A // 𝔭.IsPrime ∧ 𝔭 ∉ S } →+ Additive G

theorem artinMap_of {A : Type u_1} [CommRing A] (G : Type u_2) [CommGroup G] {S : Set (Ideal A)} (artinSymbolPrime : { 𝔭 : Ideal A // 𝔭.IsPrime ∧ 𝔭 ∉ S } → G) (𝔭 : { 𝔭 : Ideal A // 𝔭.IsPrime ∧ 𝔭 ∉ S }) : (artinMap G artinSymbolPrime) (FreeAbelianGroup.of 𝔭) = Additive.ofMul (artinSymbolPrime 𝔭)