theorem ArtinUnramified.hilbert_theorem_90 (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [IsCyclic Gal(L/K)] {σ : Gal(L/K)} (hσ : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers σ) {α : L} : (Algebra.norm K) α = 1 ↔ ∃ (β : Lˣ), ↑β / σ ↑β = α

theorem ArtinUnramified.zpow_apply_eq_of_apply_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {σ : Gal(L/K)} {x : L} (h : σ x = x) (n : ℤ) : (σ ^ n) x = x

def ArtinUnramified.sigmaMinusOneMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (σ : Gal(L/K)) : L →ₗ[K] L

theorem ArtinUnramified.range_sigmaMinusOneMap_le_ker_trace {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (σ : Gal(L/K)) : (sigmaMinusOneMap σ).range ≤ (Algebra.trace K L).ker

theorem ArtinUnramified.finrank_ker_sigmaMinusOneMap_eq_one {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {σ : Gal(L/K)} (hσ : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers σ) : Module.finrank K ↥(sigmaMinusOneMap σ).ker = 1

theorem ArtinUnramified.finrank_range_trace {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] : Module.finrank K ↥(Algebra.trace K L).range = 1

theorem ArtinUnramified.trace_surjective_cyclic (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [IsCyclic Gal(L/K)] : Function.Surjective ⇑(Algebra.trace K L)

theorem ArtinUnramified.ker_trace_eq_range_sigmaMinusOne (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [IsCyclic Gal(L/K)] {σ : Gal(L/K)} (hσ : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers σ) {x : L} (hx : (Algebra.trace K L) x = 0) : ∃ (y : L), σ y - y = x

theorem ArtinUnramified.galois_fixed_point_in_base (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [IsCyclic Gal(L/K)] {σ : Gal(L/K)} (hσ : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers σ) {x : L} (hx_fixed : σ x = x) : ∃ (k : K), (algebraMap K L) k = x

theorem ArtinUnramified.norm_one_iff_quotient (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [IsCyclic Gal(L/K)] {σ : Gal(L/K)} (hσ : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers σ) {α : L} (hα : (Algebra.norm K) α = 1) : ∃ (β : Lˣ), ↑β / σ ↑β = α

theorem ArtinUnramified.tate_cohomology_cyclic_extension (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [IsCyclic Gal(L/K)] {σ : Gal(L/K)} (hσ : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers σ) : Function.Surjective ⇑(Algebra.trace K L) ∧ (∀ {x : L}, (Algebra.trace K L) x = 0 → ∃ (y : L), σ y - y = x) ∧ (∀ {x : L}, σ x = x → ∃ (k : K), (algebraMap K L) k = x) ∧ ∀ {α : L}, (Algebra.norm K) α = 1 → ∃ (β : Lˣ), ↑β / σ ↑β = α

def ArtinUnramified.DecompositionGroupOfPlace {G : Type u_1} [Group G] {W : Type u_2} [MulAction G W] (w : W) : Subgroup G

noncomputable def ArtinUnramified.e₀ (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : ℕ

noncomputable def ArtinUnramified.nRamifiedInfinitePlaces (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] : ℕ

noncomputable def ArtinUnramified.e_inf (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] : ℕ

noncomputable def ArtinUnramified.e (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] : ℕ

theorem ArtinUnramified.ideal_map_comp_ringEquiv {R : Type u_1} [CommRing R] (e₁ e₂ : R ≃+* R) (I : Ideal R) : Ideal.map e₂ (Ideal.map e₁ I) = Ideal.map (e₁.trans e₂) I

theorem ArtinUnramified.ideal_map_refl_ringEquiv {R : Type u_1} [CommRing R] (I : Ideal R) : Ideal.map (RingEquiv.refl R) I = I

@[reducible, inline]

noncomputable abbrev ArtinUnramified.galRingEquiv (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] [IsGalois K L] (σ : Gal(L/K)) : NumberField.RingOfIntegers L ≃+* NumberField.RingOfIntegers L

theorem ArtinUnramified.galRingEquiv_mul (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] [IsGalois K L] (σ τ : Gal(L/K)) : galRingEquiv K L (σ * τ) = (galRingEquiv K L τ).trans (galRingEquiv K L σ)

theorem ArtinUnramified.galRingEquiv_one (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] [IsGalois K L] : galRingEquiv K L 1 = RingEquiv.refl (NumberField.RingOfIntegers L)

noncomputable def ArtinUnramified.mapIdealGal (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] [IsGalois K L] (σ : Gal(L/K)) : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers L))) →* ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers L)))

theorem ArtinUnramified.mk0_mapIdealGal_congr (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (σ : Gal(L/K)) {I J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers L)))} (h : ClassGroup.mk0 I = ClassGroup.mk0 J) : ClassGroup.mk0 ((mapIdealGal K L σ) I) = ClassGroup.mk0 ((mapIdealGal K L σ) J)

noncomputable def ArtinUnramified.actOnClassGroup (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (σ : Gal(L/K)) : ClassGroup (NumberField.RingOfIntegers L) →* ClassGroup (NumberField.RingOfIntegers L)

theorem ArtinUnramified.actOnClassGroup_mk0 (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (σ : Gal(L/K)) (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers L)))) : (actOnClassGroup K L σ) (ClassGroup.mk0 I) = ClassGroup.mk0 ((mapIdealGal K L σ) I)

theorem ArtinUnramified.actOnClassGroup_mul (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (σ τ : Gal(L/K)) : actOnClassGroup K L (σ * τ) = (actOnClassGroup K L σ).comp (actOnClassGroup K L τ)

theorem ArtinUnramified.actOnClassGroup_one (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] : actOnClassGroup K L 1 = MonoidHom.id (ClassGroup (NumberField.RingOfIntegers L))

noncomputable def ArtinUnramified.classGroupMulAut (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (σ : Gal(L/K)) : MulAut (ClassGroup (NumberField.RingOfIntegers L))

noncomputable def ArtinUnramified.classGroupAutHom (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] : Gal(L/K) →* MulAut (ClassGroup (NumberField.RingOfIntegers L))

@[implicit_reducible]

noncomputable instance ArtinUnramified.galActsOnClassGroup (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] : MulDistribMulAction Gal(L/K) (ClassGroup (NumberField.RingOfIntegers L))

noncomputable def ArtinUnramified.classGroupFixed (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] : Subgroup (ClassGroup (NumberField.RingOfIntegers L))

noncomputable def ArtinUnramified.normImageUnits (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : Subgroup (NumberField.RingOfIntegers K)ˣ

noncomputable def ArtinUnramified.normUnitsIndex (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] : ℕ

theorem ArtinUnramified.normUnitsIndex_pos (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] : 0 < normUnitsIndex K L

noncomputable def ArtinUnramified.normIntegerUnits (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : Subgroup (NumberField.RingOfIntegers K)ˣ

theorem ArtinUnramified.normIntegerUnits_le_normImageUnits (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : normIntegerUnits K L ≤ normImageUnits K L

theorem ArtinUnramified.normIntegerUnits_index_pos (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : 0 < (normIntegerUnits K L).index

noncomputable def ArtinUnramified.principalFixedIndex (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : ℕ

theorem ArtinUnramified.herbrand_quotient_computation_ch23 (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : ∃ (h0 : ℕ) (h_minus1 : ℕ), 0 < h_minus1 ∧ h0.Coprime h_minus1 ∧ h0 * Module.finrank K L = h_minus1 * e_inf K L

theorem ArtinUnramified.herbrand_quotient_divisibility_ch23 (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : e_inf K L ∣ (normIntegerUnits K L).index * Module.finrank K L

theorem ArtinUnramified.normIntegerUnits_index_dvd_tateH0_ch23 (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] (h0 h_minus1 : ℕ) (h_pos : 0 < h_minus1) (h_coprime : h0.Coprime h_minus1) (h_eq : h0 * Module.finrank K L = h_minus1 * e_inf K L) : h0 ∣ (normIntegerUnits K L).index

theorem ArtinUnramified.herbrand_quotient_units_ch23 (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : ∃ (r : ℕ), (normIntegerUnits K L).index * Module.finrank K L = r * e_inf K L

theorem ArtinUnramified.e_inf_dvd_index_mul_finrank_ch23 (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : e_inf K L ∣ (normIntegerUnits K L).index * Module.finrank K L

theorem ArtinUnramified.herbrand_quotient_units_index (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : ∃ (r : ℕ), 0 < r ∧ r * e_inf K L = (normIntegerUnits K L).index * Module.finrank K L

theorem ArtinUnramified.herbrand_quotient_units_pos_nat (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : ∃ (q : ℕ), 0 < q ∧ (normIntegerUnits K L).index * Module.finrank K L = e_inf K L * q

theorem ArtinUnramified.e_inf_dvd_index_mul_finrank (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : e_inf K L ∣ (normIntegerUnits K L).index * Module.finrank K L

theorem ArtinUnramified.les_connecting_surjection_aux (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : ∃ (f : ↥(classGroupFixed K L) →* ↥(normImageUnits K L) ⧸ (normIntegerUnits K L).subgroupOf (normImageUnits K L)), Nat.card ↥f.ker * Nat.card (↥(normImageUnits K L) ⧸ (normIntegerUnits K L).subgroupOf (normImageUnits K L)) = Nat.card ↥(classGroupFixed K L)

theorem ArtinUnramified.les_connecting_surjection (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : ∃ (f : ↥(classGroupFixed K L) →* ↥(normImageUnits K L) ⧸ (normIntegerUnits K L).subgroupOf (normImageUnits K L)), Function.Surjective ⇑f

theorem ArtinUnramified.tate_les_relIndex_dvd_classGroupFixed_card (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : (normIntegerUnits K L).relIndex (normImageUnits K L) ∣ Nat.card ↥(classGroupFixed K L)

theorem ArtinUnramified.index_tower_ideal_class_ch23 (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : Nat.card ↥(classGroupFixed K L) / (normIntegerUnits K L).relIndex (normImageUnits K L) * principalFixedIndex K L = e₀ K L * NumberField.classNumber K

theorem ArtinUnramified.classGroupFixed_mul_principalFixedIndex_from_les (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : Nat.card ↥(classGroupFixed K L) * principalFixedIndex K L = e₀ K L * NumberField.classNumber K * (normIntegerUnits K L).relIndex (normImageUnits K L)

theorem ArtinUnramified.acnf_cohomological_eq7 (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : Nat.card ↥(classGroupFixed K L) * (normIntegerUnits K L).index * Module.finrank K L = e K L * NumberField.classNumber K * (normIntegerUnits K L).relIndex (normImageUnits K L)

theorem ArtinUnramified.normIntegerUnits_relIndex_pos (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : 0 < (normIntegerUnits K L).relIndex (normImageUnits K L)

theorem ArtinUnramified.ambiguous_class_number_formula (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : Nat.card ↥(classGroupFixed K L) * normUnitsIndex K L * Module.finrank K L = e K L * NumberField.classNumber K

structure ArtinUnramified.RamificationData : Type

• e₀ : ℕ
• e_inf : ℕ
• e₀_pos : 0 < self.e₀
• e_inf_pos : 0 < self.e_inf

def ArtinUnramified.RamificationData.e (rd : RamificationData) : ℕ

def ArtinUnramified.RamificationData.IsTotallyUnramified (rd : RamificationData) : Prop

noncomputable def ArtinUnramified.RamificationData.ofNumberFieldExtension (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (he₀_pos : 0 < ArtinUnramified.e₀ K L) : RamificationData

structure ArtinUnramified.CyclicExtensionData : Type (max (u_1 + 1) (u_2 + 1))

• G : Type u_1
• M : Type u_2
• instGroupG : Group self.G
• instFiniteG : Finite self.G
• instCyclicG : IsCyclic self.G
• instCommGroupM : CommGroup self.M
• instFiniteM : Finite self.M
• instAction : MulDistribMulAction self.G self.M
• n : ℕ
• hn_pos : 0 < self.n
• hn_eq : self.n = Nat.card self.G
• ram : RamificationData
• card_ClK : ℕ
• hcard_ClK_pos : 0 < self.card_ClK
• norm_units_index : ℕ
• hnorm_pos : 0 < self.norm_units_index
• norm_index_IK : ℕ
• hnorm_index_IK_pos : 0 < self.norm_index_IK
• h0_ClL : ℕ
• hh0_pos : 0 < self.h0_ClL
• h_acnf : Nat.card ↥(FixedPoints.subgroup self.G self.M) * self.norm_units_index * self.n = self.ram.e * self.card_ClK
• h_norm_index_ineq : self.norm_index_IK ≤ self.n
• h_eq8 : self.norm_index_IK * self.ram.e = self.h0_ClL * self.norm_units_index * self.n

noncomputable def ArtinUnramified.CyclicExtensionData.card_ClL_G (d : CyclicExtensionData) : ℕ

theorem Ideal.spanNorm_mem_nonZeroDivisors {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] {I : Ideal (NumberField.RingOfIntegers L)} (hI : I ∈ nonZeroDivisors (Ideal (NumberField.RingOfIntegers L))) : spanNorm (NumberField.RingOfIntegers K) I ∈ nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))

noncomputable def ArtinUnramified.spanNormNZD (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers L))) →* ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))

noncomputable def ArtinUnramified.normToClK (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers L))) →* ClassGroup (NumberField.RingOfIntegers K)

theorem ArtinUnramified.normToClK_well_defined {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] {I J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers L)))} (h : ClassGroup.mk0 I = ClassGroup.mk0 J) : (normToClK K L) I = (normToClK K L) J

theorem ArtinUnramified.normToClK_of_mk0_eq_one {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] {I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers L)))} (h : ClassGroup.mk0 I = 1) : (normToClK K L) I = 1

noncomputable def ArtinUnramified.normOnFracUnits (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers L)) (FractionRing (NumberField.RingOfIntegers L)))ˣ →* ClassGroup (NumberField.RingOfIntegers K)

theorem ArtinUnramified.normOnFracUnits_kills_principal (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] : (toPrincipalIdeal (NumberField.RingOfIntegers L) (FractionRing (NumberField.RingOfIntegers L))).range ≤ (normOnFracUnits K L).ker

noncomputable def ArtinUnramified.ClassGroup.normMap (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] : ClassGroup (NumberField.RingOfIntegers L) →* ClassGroup (NumberField.RingOfIntegers K)

noncomputable def ArtinUnramified.idealGroupIndex (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] : ℕ

noncomputable def ArtinUnramified.CyclicExtensionData.norm_index_IK_ax (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : ℕ

theorem ArtinUnramified.CyclicExtensionData.norm_index_IK_pos_ax (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : 0 < norm_index_IK_ax K L

noncomputable def ArtinUnramified.CyclicExtensionData.h0_ClL_ax (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : ℕ

theorem ArtinUnramified.CyclicExtensionData.h0_ClL_pos_ax (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : 0 < h0_ClL_ax K L

theorem ArtinUnramified.CyclicExtensionData.norm_index_ineq_ax (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : norm_index_IK_ax K L ≤ Module.finrank K L

theorem ArtinUnramified.CyclicExtensionData.eq8_ax (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] (he₀_pos : 0 < e₀ K L) : norm_index_IK_ax K L * (RamificationData.ofNumberFieldExtension K L he₀_pos).e = h0_ClL_ax K L * normUnitsIndex K L * Module.finrank K L

noncomputable def ArtinUnramified.CyclicExtensionData.ofNumberFieldExtension (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] (he₀_pos : 0 < e₀ K L) : CyclicExtensionData

noncomputable def ArtinUnramified.galUnitsAutHom (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] [IsGalois K L] : Gal(L/K) →* MulAut (NumberField.RingOfIntegers L)ˣ

@[implicit_reducible]

noncomputable instance ArtinUnramified.galActsOnUnits (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] [IsGalois K L] : MulDistribMulAction Gal(L/K) (NumberField.RingOfIntegers L)ˣ

noncomputable def ArtinUnramified.normMapUnits (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] [IsGalois K L] [Fintype Gal(L/K)] : (NumberField.RingOfIntegers L)ˣ →* (NumberField.RingOfIntegers L)ˣ

noncomputable def ArtinUnramified.unitsFixed (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] [IsGalois K L] : Subgroup (NumberField.RingOfIntegers L)ˣ

noncomputable def ArtinUnramified.normImageUnitsSubgroup (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] [IsGalois K L] [Fintype Gal(L/K)] : Subgroup (NumberField.RingOfIntegers L)ˣ

noncomputable def ArtinUnramified.normKerUnits (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] [IsGalois K L] [Fintype Gal(L/K)] : Subgroup (NumberField.RingOfIntegers L)ˣ

def ArtinUnramified.augmentationUnitsSubgroup (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] [IsGalois K L] : Subgroup (NumberField.RingOfIntegers L)ˣ

theorem ArtinUnramified.subgroup_fg_of_comm_fg (L : Type u_2) [Field L] [NumberField L] (H : Subgroup (NumberField.RingOfIntegers L)ˣ) : H.FG

theorem ArtinUnramified.pow_card_mem_augmentationUnitsSubgroup (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [Fintype Gal(L/K)] (u : (NumberField.RingOfIntegers L)ˣ) (hu : (normMapUnits K L) u = 1) : u ^ Fintype.card Gal(L/K) ∈ augmentationUnitsSubgroup K L

def ArtinUnramified.tateH0Units (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] [IsGalois K L] [Fintype Gal(L/K)] : Type u_2

def ArtinUnramified.tateMinus1Units (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] [IsGalois K L] [Fintype Gal(L/K)] : Type u_2

instance ArtinUnramified.tateH0Units.finite (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [Fintype Gal(L/K)] [IsCyclic Gal(L/K)] : Finite (tateH0Units K L)

instance ArtinUnramified.tateMinus1Units.finite (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [Fintype Gal(L/K)] [IsCyclic Gal(L/K)] : Finite (tateMinus1Units K L)

noncomputable def ArtinUnramified.herbrandQuotientUnitsValue (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] [IsGalois K L] [Fintype Gal(L/K)] [IsCyclic Gal(L/K)] : ℚ

theorem ArtinUnramified.infinitePlace_map_prod {L : Type u_1} [Field L] [NumberField L] (w : NumberField.InfinitePlace L) {ι : Type u_2} (s : Finset ι) (f : ι → L) : w (∏ i ∈ s, f i) = ∏ i ∈ s, w (f i)

theorem ArtinUnramified.infinitePlace_prod_units {L : Type u_1} [Field L] [NumberField L] (w : NumberField.InfinitePlace L) {ι : Type u_2} (s : Finset ι) (f : ι → (NumberField.RingOfIntegers L)ˣ) : w ((algebraMap (NumberField.RingOfIntegers L) L) ↑(∏ i ∈ s, f i)) = ∏ i ∈ s, w ((algebraMap (NumberField.RingOfIntegers L) L) ↑(f i))

theorem ArtinUnramified.infinitePlace_unit_pos {L : Type u_1} [Field L] [NumberField L] (w : NumberField.InfinitePlace L) (u : (NumberField.RingOfIntegers L)ˣ) : 0 < w ((algebraMap (NumberField.RingOfIntegers L) L) ↑u)

theorem ArtinUnramified.prop_15_9_raw_units (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] : ∃ (u : NumberField.InfinitePlace L → (NumberField.RingOfIntegers L)ˣ), ∀ (v w : NumberField.InfinitePlace L), w ≠ v → w ((algebraMap (NumberField.RingOfIntegers L) L) ↑(u v)) < 1

theorem ArtinUnramified.infinitePlace_smul_galActsOnUnits (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (σ : Gal(L/K)) (w : NumberField.InfinitePlace L) (u : (NumberField.RingOfIntegers L)ˣ) : w ((algebraMap (NumberField.RingOfIntegers L) L) ↑(σ • u)) = (σ⁻¹ • w) ((algebraMap (NumberField.RingOfIntegers L) L) ↑u)

theorem ArtinUnramified.prop_15_9_and_averaging (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] : ∃ (α : NumberField.InfinitePlace L → (NumberField.RingOfIntegers L)ˣ), (∀ (v : NumberField.InfinitePlace L) (τ : Gal(L/K)), τ • v = v → τ • α v = α v) ∧ ∀ (v w : NumberField.InfinitePlace L), w ≠ v → w ((algebraMap (NumberField.RingOfIntegers L) L) ↑(α v)) < 1

theorem ArtinUnramified.herbrand_equivariant_diagonal_dominant_units (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] : ∃ (β : NumberField.InfinitePlace L → (NumberField.RingOfIntegers L)ˣ), (∀ (σ : Gal(L/K)) (w : NumberField.InfinitePlace L), σ • β w = β (σ • w)) ∧ ∀ (v w : NumberField.InfinitePlace L), w ≠ v → w ((algebraMap (NumberField.RingOfIntegers L) L) ↑(β v)) < 1

theorem ArtinUnramified.diag_dom_units_injective {K : Type u_1} [Field K] [NumberField K] (β : NumberField.InfinitePlace K → (NumberField.RingOfIntegers K)ˣ) (hβ : ∀ (v w : NumberField.InfinitePlace K), w ≠ v → w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(β v)) < 1) : Function.Injective β

theorem ArtinUnramified.herbrand_step1_equivariant_units (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] : ∃ (β : NumberField.InfinitePlace L → (NumberField.RingOfIntegers L)ˣ), (∀ (σ : Gal(L/K)) (w : NumberField.InfinitePlace L), σ • β w = β (σ • w)) ∧ Function.Injective β ∧ (Subgroup.closure (Set.range β)).FiniteIndex

theorem ArtinUnramified.relations_proportional (K : Type u_1) [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (β : NumberField.InfinitePlace L → (NumberField.RingOfIntegers L)ˣ) (hinj : Function.Injective β) (hfi : (Subgroup.closure (Set.range β)).FiniteIndex) (n m : NumberField.InfinitePlace L → ℤ) (hn : ∏ w : NumberField.InfinitePlace L, β w ^ n w = 1) (hm : ∏ w : NumberField.InfinitePlace L, β w ^ m w = 1) : ∃ (a : ℤ) (b : ℤ), (a ≠ 0 ∨ b ≠ 0) ∧ ∀ (w : NumberField.InfinitePlace L), a * m w = b * n w

theorem ArtinUnramified.nontrivial_constant_relation_axiom (K : Type u_1) [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (β : NumberField.InfinitePlace L → (NumberField.RingOfIntegers L)ˣ) (hequiv : ∀ (σ : Gal(L/K)) (w : NumberField.InfinitePlace L), σ • β w = β (σ • w)) (hinj : Function.Injective β) (hfi : (Subgroup.closure (Set.range β)).FiniteIndex) : ∃ (k : ℤ), k ≠ 0 ∧ ∏ w : NumberField.InfinitePlace L, β w ^ k = 1

theorem ArtinUnramified.proportional_galois_implies_constant (K : Type u_1) [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (β : NumberField.InfinitePlace L → (NumberField.RingOfIntegers L)ˣ) (hequiv : ∀ (σ : Gal(L/K)) (w : NumberField.InfinitePlace L), σ • β w = β (σ • w)) (hinj : Function.Injective β) (hfi : (Subgroup.closure (Set.range β)).FiniteIndex) (n : NumberField.InfinitePlace L → ℤ) (hn : ∏ w : NumberField.InfinitePlace L, β w ^ n w = 1) (hn_ne : ∃ (w₀ : NumberField.InfinitePlace L), n w₀ ≠ 0) : ∃ (k : ℤ), ∀ (w : NumberField.InfinitePlace L), n w = k

theorem ArtinUnramified.relations_are_constant (K : Type u_1) [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (β : NumberField.InfinitePlace L → (NumberField.RingOfIntegers L)ˣ) (hequiv : ∀ (σ : Gal(L/K)) (w : NumberField.InfinitePlace L), σ • β w = β (σ • w)) (hinj : Function.Injective β) (hfi : (Subgroup.closure (Set.range β)).FiniteIndex) (n : NumberField.InfinitePlace L → ℤ) : ∏ w : NumberField.InfinitePlace L, β w ^ n w = 1 → ∃ (k : ℤ), ∀ (w : NumberField.InfinitePlace L), n w = k

theorem ArtinUnramified.nontrivial_constant_relation_exists (K : Type u_1) [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (β : NumberField.InfinitePlace L → (NumberField.RingOfIntegers L)ˣ) (hequiv : ∀ (σ : Gal(L/K)) (w : NumberField.InfinitePlace L), σ • β w = β (σ • w)) (hinj : Function.Injective β) (hfi : (Subgroup.closure (Set.range β)).FiniteIndex) : ∃ (k : ℤ), k ≠ 0 ∧ ∏ w : NumberField.InfinitePlace L, β w ^ k = 1

theorem ArtinUnramified.rank_one_constant_relations (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (β : NumberField.InfinitePlace L → (NumberField.RingOfIntegers L)ˣ) (hequiv : ∀ (σ : Gal(L/K)) (w : NumberField.InfinitePlace L), σ • β w = β (σ • w)) (hinj : Function.Injective β) (hfi : (Subgroup.closure (Set.range β)).FiniteIndex) : (∀ (n : NumberField.InfinitePlace L → ℤ), ∏ w : NumberField.InfinitePlace L, β w ^ n w = 1 → ∃ (k : ℤ), ∀ (w : NumberField.InfinitePlace L), n w = k) ∧ ∃ (k : ℤ), k ≠ 0 ∧ ∏ w : NumberField.InfinitePlace L, β w ^ k = 1

theorem ArtinUnramified.dirichlet_rank_one_relation (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (β : NumberField.InfinitePlace L → (NumberField.RingOfIntegers L)ˣ) (hequiv : ∀ (σ : Gal(L/K)) (w : NumberField.InfinitePlace L), σ • β w = β (σ • w)) (hinj : Function.Injective β) (hfi : (Subgroup.closure (Set.range β)).FiniteIndex) : ∃ (n₀ : ℤ), n₀ ≠ 0 ∧ ∏ w : NumberField.InfinitePlace L, β w ^ n₀ = 1 ∧ ∀ (n : NumberField.InfinitePlace L → ℤ), ∏ w : NumberField.InfinitePlace L, β w ^ n w = 1 → ∃ (m : ℤ), ∀ (w : NumberField.InfinitePlace L), n w = m * n₀

theorem ArtinUnramified.zpow_closure_finiteIndex {G : Type u_1} [CommGroup G] {ι : Type u_2} [Fintype ι] (β : ι → G) (n₀ : ℤ) (hn₀ : n₀ ≠ 0) (hfi : (Subgroup.closure (Set.range β)).FiniteIndex) : (Subgroup.closure (Set.range fun (w : ι) => β w ^ n₀)).FiniteIndex

theorem ArtinUnramified.herbrand_relation_generator (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (β : NumberField.InfinitePlace L → (NumberField.RingOfIntegers L)ˣ) (hequiv : ∀ (σ : Gal(L/K)) (w : NumberField.InfinitePlace L), σ • β w = β (σ • w)) (hinj : Function.Injective β) (hfi : (Subgroup.closure (Set.range β)).FiniteIndex) : ∃ (n₀ : ℤ), n₀ ≠ 0 ∧ ∏ w : NumberField.InfinitePlace L, β w ^ n₀ = 1 ∧ (∀ (n : NumberField.InfinitePlace L → ℤ), ∏ w : NumberField.InfinitePlace L, β w ^ n w = 1 → ∃ (m : ℤ), ∀ (w : NumberField.InfinitePlace L), n w = m * n₀) ∧ (Function.Injective fun (w : NumberField.InfinitePlace L) => β w ^ n₀) ∧ (Subgroup.closure (Set.range fun (w : NumberField.InfinitePlace L) => β w ^ n₀)).FiniteIndex

theorem ArtinUnramified.herbrand_step2_relation_construction (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (β : NumberField.InfinitePlace L → (NumberField.RingOfIntegers L)ˣ) (hequiv : ∀ (σ : Gal(L/K)) (w : NumberField.InfinitePlace L), σ • β w = β (σ • w)) (hinj : Function.Injective β) (hfi : (Subgroup.closure (Set.range β)).FiniteIndex) : ∃ (ε : NumberField.InfinitePlace L → (NumberField.RingOfIntegers L)ˣ), (∀ (σ : Gal(L/K)) (w : NumberField.InfinitePlace L), σ • ε w = ε (σ • w)) ∧ Function.Injective ε ∧ (Subgroup.closure (Set.range ε)).FiniteIndex ∧ ∏ w : NumberField.InfinitePlace L, ε w = 1 ∧ ∀ (n : NumberField.InfinitePlace L → ℤ), ∏ w : NumberField.InfinitePlace L, ε w ^ n w = 1 → ∃ (c : ℤ), ∀ (w : NumberField.InfinitePlace L), n w = c

theorem ArtinUnramified.herbrand_unit_theorem (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] : ∃ (ε : NumberField.InfinitePlace L → (NumberField.RingOfIntegers L)ˣ), (∀ (σ : Gal(L/K)) (w : NumberField.InfinitePlace L), σ • ε w = ε (σ • w)) ∧ Function.Injective ε ∧ (Subgroup.closure (Set.range ε)).FiniteIndex ∧ ∏ w : NumberField.InfinitePlace L, ε w = 1 ∧ ∀ (n : NumberField.InfinitePlace L → ℤ), ∏ w : NumberField.InfinitePlace L, ε w ^ n w = 1 → ∃ (c : ℤ), ∀ (w : NumberField.InfinitePlace L), n w = c

theorem ArtinUnramified.herbrand_quotient_computation_A (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [Fintype Gal(L/K)] [IsCyclic Gal(L/K)] : ∃ (h0_A : ℕ) (hminus1_A : ℕ), 0 < hminus1_A ∧ h0_A * Module.finrank K L = hminus1_A * e_inf K L

noncomputable def ArtinUnramified.algebraMapToFixed (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] : (NumberField.RingOfIntegers K)ˣ →* ↥(unitsFixed K L)

theorem ArtinUnramified.algebraMapToFixed_surjective (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] : Function.Surjective ⇑(algebraMapToFixed K L)

theorem ArtinUnramified.normMapUnits_val_eq_algebraMap_mk' (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [Fintype Gal(L/K)] (v : (NumberField.RingOfIntegers L)ˣ) : ↑((normMapUnits K L) v) = (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) (IsIntegralClosure.mk' (NumberField.RingOfIntegers K) ((Algebra.norm K) ((algebraMap (NumberField.RingOfIntegers L) L) ↑v)) ⋯)

theorem ArtinUnramified.tateH0Units_card_eq_normIntegerUnits_index (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [Fintype Gal(L/K)] [IsCyclic Gal(L/K)] [Finite (tateH0Units K L)] : Nat.card (tateH0Units K L) = (normIntegerUnits K L).index

theorem ArtinUnramified.herbrand_quotient_tate_units_identity (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [Fintype Gal(L/K)] [IsCyclic Gal(L/K)] : Nat.card (tateH0Units K L) * Module.finrank K L = Nat.card (tateMinus1Units K L) * e_inf K L

theorem ArtinUnramified.tateMinus1Units_card_eq_principalFixedIndex (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [Fintype Gal(L/K)] [IsCyclic Gal(L/K)] [Finite (tateMinus1Units K L)] : Nat.card (tateMinus1Units K L) = principalFixedIndex K L

theorem ArtinUnramified.cor_23_48_herbrand_invariance (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [Fintype Gal(L/K)] [IsCyclic Gal(L/K)] [Finite (tateH0Units K L)] [Finite (tateMinus1Units K L)] (h0_A hminus1_A : ℕ) : 0 < hminus1_A → ∀ (hcomp : h0_A * Module.finrank K L = hminus1_A * e_inf K L), Nat.card (tateH0Units K L) * hminus1_A = Nat.card (tateMinus1Units K L) * h0_A

theorem ArtinUnramified.herbrand_quotient_units_tate (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [Fintype Gal(L/K)] [IsCyclic Gal(L/K)] : Nat.card (tateH0Units K L) * Module.finrank K L = Nat.card (tateMinus1Units K L) * e_inf K L

theorem ArtinUnramified.herbrand_quotient_invariance_A (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [Fintype Gal(L/K)] [IsCyclic Gal(L/K)] (h0_A hminus1_A : ℕ) (hpos : 0 < hminus1_A) (hcomp : h0_A * Module.finrank K L = hminus1_A * e_inf K L) : Nat.card (tateH0Units K L) * hminus1_A = Nat.card (tateMinus1Units K L) * h0_A

theorem ArtinUnramified.herbrand_quotient_invariance_units (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [Fintype Gal(L/K)] [IsCyclic Gal(L/K)] : ∃ (h0_A : ℕ) (hminus1_A : ℕ), 0 < hminus1_A ∧ Nat.card (tateH0Units K L) * hminus1_A = Nat.card (tateMinus1Units K L) * h0_A ∧ h0_A * Module.finrank K L = hminus1_A * e_inf K L

theorem ArtinUnramified.herbrand_quotient_units (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [Fintype Gal(L/K)] [IsCyclic Gal(L/K)] : Nat.card (tateH0Units K L) * Module.finrank K L = Nat.card (tateMinus1Units K L) * e_inf K L

theorem ArtinUnramified.herbrand_quotient_units_value_eq (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [Fintype Gal(L/K)] [IsCyclic Gal(L/K)] : herbrandQuotientUnitsValue K L = ↑(e_inf K L) / ↑(Module.finrank K L)

structure ArtinUnramified.IdealGroupData : Type (max (max (u_1 + 1) (u_2 + 1)) (u_3 + 1))

• G : Type u_1
• I_L : Type u_2
• I_K : Type u_3
• instGroupG : Group self.G
• instFiniteG : Finite self.G
• instCyclicG : IsCyclic self.G
• instCommGroupIL : CommGroup self.I_L
• instCommGroupIK : CommGroup self.I_K
• instAction : MulDistribMulAction self.G self.I_L
• normMap : self.I_L →* self.I_K
• extensionMap : self.I_K →* self.I_L
• extensionMap_injective : Function.Injective ⇑self.extensionMap
• e₀ : ℕ
• e₀_pos : 0 < self.e₀
• normImage_index_pos : 0 < self.normMap.range.index
• extensionMap_range_le_fixedPoints : self.extensionMap.range ≤ FixedPoints.subgroup self.G self.I_L
• cohomNorm_eq (I : self.I_L) : ∏ g : self.G, g • I = self.extensionMap (self.normMap I)
• augmentation_preimage (σ : self.G) : (∀ (g : self.G), g ∈ Subgroup.zpowers σ) → ∀ (I : self.I_L), ∏ g : self.G, g • I = 1 → ∃ (J : self.I_L), σ • J * J⁻¹ = I
• index_fixedPoints_over_range : (self.extensionMap.range.subgroupOf (FixedPoints.subgroup self.G self.I_L)).index = self.e₀

def ArtinUnramified.IdealGroupData.fixedIdeals (d : IdealGroupData) : Subgroup d.I_L

def ArtinUnramified.IdealGroupData.extendedIdeals (d : IdealGroupData) : Subgroup d.I_L

def ArtinUnramified.IdealGroupData.normImage (d : IdealGroupData) : Subgroup d.I_K

noncomputable def ArtinUnramified.IdealGroupData.cohomNormImage (d : IdealGroupData) : Subgroup d.I_L

theorem ArtinUnramified.index_fixed_over_extended_eq_e₀ (d : IdealGroupData) : (d.extendedIdeals.subgroupOf d.fixedIdeals).index = d.e₀

theorem ArtinUnramified.extendedIdeals_le_fixedIdeals (d : IdealGroupData) : d.extendedIdeals ≤ d.fixedIdeals

theorem ArtinUnramified.cohomNormImage_le_extendedIdeals (d : IdealGroupData) : d.cohomNormImage ≤ d.extendedIdeals

theorem ArtinUnramified.relIndex_map_range_of_injective {A : Type u_1} {B : Type u_2} [CommGroup A] [CommGroup B] (f : A →* B) (K : Subgroup A) (hf : Function.Injective ⇑f) : (Subgroup.map f K).relIndex f.range = K.index

theorem ArtinUnramified.cohomNormImage_eq_normImage_map (d : IdealGroupData) : d.cohomNormImage = Subgroup.map d.extensionMap d.normImage

theorem ArtinUnramified.cohomNormImage_relIndex_extendedIdeals (d : IdealGroupData) : d.cohomNormImage.relIndex d.extendedIdeals = d.normImage.index

theorem ArtinUnramified.herbrand_quotient_ideals (d : IdealGroupData) : (d.cohomNormImage.subgroupOf d.fixedIdeals).index = d.e₀ * d.normImage.index

theorem ArtinUnramified.herbrand_quotient_ideals_modulus (d : IdealGroupData) (h_unram : d.e₀ = 1) : (d.cohomNormImage.subgroupOf d.fixedIdeals).index = d.normImage.index

noncomputable def ArtinUnramified.quotient_equiv_image_quotient {A : Type u_1} {C : Type u_2} [CommGroup A] [CommGroup C] (f : A →* C) (B : Subgroup A) (hB : f.ker ≤ B) : A ⧸ B ≃* ↥f.range ⧸ (Subgroup.map f B).subgroupOf f.range

def ArtinUnramified.TateCohomologyAllTrivial (G : Type u_1) [Group G] [Finite G] (M : Type u_2) [CommGroup M] [MulDistribMulAction G M] : Prop

theorem ArtinUnramified.tate_cohomology_trivial_unramified (d : CyclicExtensionData) (hunr : d.ram.IsTotallyUnramified) : TateCohomologyAllTrivial d.G d.M

theorem ArtinUnramified.norm_index_inequality_thm22_29 (d : CyclicExtensionData) (hunr : d.ram.IsTotallyUnramified) : d.norm_index_IK ≤ d.n

theorem ArtinUnramified.norm_index_identity_eq8 (d : CyclicExtensionData) : d.norm_index_IK * d.ram.e = d.h0_ClL * d.norm_units_index * d.n

theorem ArtinUnramified.norm_index_ineq_unramified (d : CyclicExtensionData) (hunr : d.ram.IsTotallyUnramified) : d.n ≤ d.norm_index_IK

theorem ArtinUnramified.norm_index_equality_consequences (d : CyclicExtensionData) (hunr : d.ram.IsTotallyUnramified) : d.norm_index_IK = d.n ∧ d.norm_units_index = 1 ∧ d.h0_ClL = 1

theorem ArtinUnramified.class_group_invariants_unramified (d : CyclicExtensionData) (hunr : d.ram.IsTotallyUnramified) : d.card_ClL_G * d.n = d.card_ClK ∧ d.norm_units_index = 1 ∧ TateCohomologyAllTrivial d.G d.M

theorem ArtinUnramified.norm_units_index_eq_one_unramified (d : CyclicExtensionData) (hunr : d.ram.IsTotallyUnramified) : d.norm_units_index = 1

def ArtinUnramified.galFracSubmod (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (σ : Gal(L/K)) (M : Submodule (NumberField.RingOfIntegers L) L) : Submodule (NumberField.RingOfIntegers L) L

noncomputable def ArtinUnramified.galFracIdeal (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (σ : Gal(L/K)) (I : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers L)) L) : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers L)) L

noncomputable def ArtinUnramified.galFracIdealEquiv (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (σ : Gal(L/K)) : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers L)) L ≃* FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers L)) L

noncomputable def ArtinUnramified.galFracIdealAutHom (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] : Gal(L/K) →* MulAut (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers L)) L)

def ArtinUnramified.mulAutUnitsLift (M : Type u_3) [Monoid M] : MulAut M →* MulAut Mˣ

@[reducible]

noncomputable def ArtinUnramified.galActionOnFracIdealUnits_ax (K : Type u_3) (L : Type u_4) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : MulDistribMulAction Gal(L/K) (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers L)) L)ˣ

@[reducible]

noncomputable def ArtinUnramified.galActionOnFracIdealUnits (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : MulDistribMulAction Gal(L/K) (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers L)) L)ˣ

noncomputable def ArtinUnramified.idealNormMonoidHom_ax (K : Type u_3) (L : Type u_4) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers L)) L)ˣ →* (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ

noncomputable def ArtinUnramified.idealNormMonoidHom (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers L)) L)ˣ →* (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ

noncomputable def ArtinUnramified.idealExtensionMonoidHom_ax (K : Type u_3) (L : Type u_4) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ →* (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers L)) L)ˣ

noncomputable def ArtinUnramified.idealExtensionMonoidHom (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ →* (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers L)) L)ˣ

theorem ArtinUnramified.idealExtensionMonoidHom_injective (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : Function.Injective ⇑(idealExtensionMonoidHom K L)

theorem ArtinUnramified.idealNormMonoidHom_range_index_pos (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : 0 < (idealNormMonoidHom K L).range.index

theorem ArtinUnramified.galFracIdeal_extended_eq (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] (σ : Gal(L/K)) (I : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K) : galFracIdeal K L σ ((FractionalIdeal.extendedHomₐ L (NumberField.RingOfIntegers L)) I) = (FractionalIdeal.extendedHomₐ L (NumberField.RingOfIntegers L)) I

theorem ArtinUnramified.galActionOnFracIdealUnits_extensionMap_fixed (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : (idealExtensionMonoidHom K L).range ≤ FixedPoints.subgroup Gal(L/K) (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers L)) L)ˣ

noncomputable def ArtinUnramified.IdealGroupData.ofNumberFieldExtension (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] (he₀_pos : 0 < ArtinUnramified.e₀ K L) : IdealGroupData