noncomputable def localModuleIndex {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {M : Type u_3} [AddCommGroup M] [Module R M] (φ : M →ₗ[R] M) : FractionalIdeal (nonZeroDivisors R) K

theorem localModuleIndex_comp_equiv {R : Type u_1} [CommRing R] [IsDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {M : Type u_3} [AddCommGroup M] [Module R M] (φ : M →ₗ[R] M) (u v : M ≃ₗ[R] M) : localModuleIndex (↑u ∘ₗ φ ∘ₗ ↑v) = localModuleIndex φ

theorem localModuleIndex_comp {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {M : Type u_3} [AddCommGroup M] [Module R M] (φ ψ : M →ₗ[R] M) : localModuleIndex (φ ∘ₗ ψ) = localModuleIndex φ * localModuleIndex ψ

@[simp]

theorem localModuleIndex_id {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {M : Type u_3} [AddCommGroup M] [Module R M] : localModuleIndex LinearMap.id = 1

theorem prod_ne_zero_of_ne_bot {A : Type u_1} [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {n : ℕ} (J : Fin n → Ideal A) (hJ : ∀ (i : Fin n), J i ≠ ⊥) : ↑(∏ i : Fin n, J i) ≠ 0

theorem locally_free_becomes_free_after_inverting {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] : ∃ (I : FractionalIdeal (nonZeroDivisors A) K), I ≠ 0 ∧ ∀ (v : IsDedekindDomain.HeightOneSpectrum A) (φ : V →ₗ[A] V), (∀ (x : V), x ∈ M ↔ φ x ∈ N) → FractionalIdeal.count K v I = FractionalIdeal.count K v (FractionalIdeal.spanSingleton (nonZeroDivisors A) ((algebraMap A K) (LinearMap.det φ)))

theorem comparison_map_membership {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] : ∃ (φ : V →ₗ[A] V), ∀ (x : V), x ∈ M ↔ φ x ∈ N

theorem comparison_map_det_ne_zero {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] (φ : V →ₗ[A] V) (hφ : ∀ (x : V), x ∈ M ↔ φ x ∈ N) : (algebraMap A K) (LinearMap.det φ) ≠ 0

theorem lattice_comparison_map_exists {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] : ∃ (φ : V →ₗ[A] V), (∀ (x : V), x ∈ M ↔ φ x ∈ N) ∧ (algebraMap A K) (LinearMap.det φ) ≠ 0

theorem snf_det_eq_prod_count_at_prime {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] : N ≤ M → ∀ {n : ℕ} (J : Fin n → Ideal A), (∀ (i : Fin n), J i ≠ ⊥) → ∀ (x✝ : (↥M ⧸ Submodule.comap M.subtype N) ≃ₗ[A] DirectSum (Fin n) fun (i : Fin n) => A ⧸ J i) (φ : V →ₗ[A] V), (∀ (x : V), x ∈ M ↔ φ x ∈ N) → ∀ (v : IsDedekindDomain.HeightOneSpectrum A), FractionalIdeal.count K v (FractionalIdeal.spanSingleton (nonZeroDivisors A) ((algebraMap A K) (LinearMap.det φ))) = FractionalIdeal.count K v ↑(∏ i : Fin n, J i)

theorem snf_local_ideal_eq_prod {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] (hle : N ≤ M) {n : ℕ} (J : Fin n → Ideal A) (hJ : ∀ (i : Fin n), J i ≠ ⊥) (hiso : (↥M ⧸ Submodule.comap M.subtype N) ≃ₗ[A] DirectSum (Fin n) fun (i : Fin n) => A ⧸ J i) (φ : V →ₗ[A] V) (hφ : ∀ (x : V), x ∈ M ↔ φ x ∈ N) (P : Ideal A) (x✝ : P.IsMaximal) : Ideal.map (algebraMap A (Localization.AtPrime P)) (Ideal.span {LinearMap.det φ}) = Ideal.map (algebraMap A (Localization.AtPrime P)) (∏ i : Fin n, J i)

theorem snf_ideal_eq_prod {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] (hle : N ≤ M) {n : ℕ} (J : Fin n → Ideal A) (hJ : ∀ (i : Fin n), J i ≠ ⊥) (hiso : (↥M ⧸ Submodule.comap M.subtype N) ≃ₗ[A] DirectSum (Fin n) fun (i : Fin n) => A ⧸ J i) (φ : V →ₗ[A] V) (hφ : ∀ (x : V), x ∈ M ↔ φ x ∈ N) : Ideal.span {LinearMap.det φ} = ∏ i : Fin n, J i

theorem local_det_eq_prod_at_prime {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] (hle : N ≤ M) {n : ℕ} (J : Fin n → Ideal A) (hJ : ∀ (i : Fin n), J i ≠ ⊥) (hiso : (↥M ⧸ Submodule.comap M.subtype N) ≃ₗ[A] DirectSum (Fin n) fun (i : Fin n) => A ⧸ J i) (φ : V →ₗ[A] V) (hφ : ∀ (x : V), x ∈ M ↔ φ x ∈ N) (P : Ideal A) (hP : P.IsMaximal) : Ideal.map (algebraMap A (Localization.AtPrime P)) (Ideal.span {LinearMap.det φ}) = Ideal.map (algebraMap A (Localization.AtPrime P)) (∏ i : Fin n, J i)

theorem smith_normal_form_det_eq_prod_global {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] (hle : N ≤ M) {n : ℕ} (J : Fin n → Ideal A) (hJ : ∀ (i : Fin n), J i ≠ ⊥) (hiso : (↥M ⧸ Submodule.comap M.subtype N) ≃ₗ[A] DirectSum (Fin n) fun (i : Fin n) => A ⧸ J i) (φ : V →ₗ[A] V) (hφ : ∀ (x : V), x ∈ M ↔ φ x ∈ N) : Ideal.span {LinearMap.det φ} = ∏ i : Fin n, J i

theorem smith_normal_form_local_at_prime {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] (hle : N ≤ M) {n : ℕ} (J : Fin n → Ideal A) (hJ : ∀ (i : Fin n), J i ≠ ⊥) (hiso : (↥M ⧸ Submodule.comap M.subtype N) ≃ₗ[A] DirectSum (Fin n) fun (i : Fin n) => A ⧸ J i) (φ : V →ₗ[A] V) (hφ : ∀ (x : V), x ∈ M ↔ φ x ∈ N) (P : Ideal A) (x✝ : P.IsMaximal) : Ideal.map (algebraMap A (Localization.AtPrime P)) (Ideal.span {LinearMap.det φ}) = Ideal.map (algebraMap A (Localization.AtPrime P)) (∏ i : Fin n, J i)

theorem lattice_comparison_det_eq_prod {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] (hle : N ≤ M) {n : ℕ} (J : Fin n → Ideal A) (hJ : ∀ (i : Fin n), J i ≠ ⊥) (hiso : (↥M ⧸ Submodule.comap M.subtype N) ≃ₗ[A] DirectSum (Fin n) fun (i : Fin n) => A ⧸ J i) (φ : V →ₗ[A] V) (hφ : ∀ (x : V), x ∈ M ↔ φ x ∈ N) : Ideal.span {LinearMap.det φ} = ∏ i : Fin n, J i

theorem smith_normal_form_det_eq_prod_count {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] : N ≤ M → ∀ {n : ℕ} (J : Fin n → Ideal A), (∀ (i : Fin n), J i ≠ ⊥) → ∀ (x✝ : (↥M ⧸ Submodule.comap M.subtype N) ≃ₗ[A] DirectSum (Fin n) fun (i : Fin n) => A ⧸ J i) (φ : V →ₗ[A] V), (∀ (x : V), x ∈ M ↔ φ x ∈ N) → ∀ (v : IsDedekindDomain.HeightOneSpectrum A), FractionalIdeal.count K v (FractionalIdeal.spanSingleton (nonZeroDivisors A) ((algebraMap A K) (LinearMap.det φ))) = FractionalIdeal.count K v ↑(∏ i : Fin n, J i)

theorem product_property_from_local_analysis {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] (I : FractionalIdeal (nonZeroDivisors A) K) (hI : I ≠ 0) (hcount : ∀ (v : IsDedekindDomain.HeightOneSpectrum A) (φ : V →ₗ[A] V), (∀ (x : V), x ∈ M ↔ φ x ∈ N) → FractionalIdeal.count K v I = FractionalIdeal.count K v (FractionalIdeal.spanSingleton (nonZeroDivisors A) ((algebraMap A K) (LinearMap.det φ)))) : N ≤ M → ∀ {n : ℕ} (J : Fin n → Ideal A), (∀ (i : Fin n), J i ≠ ⊥) → ∀ (x✝ : (↥M ⧸ Submodule.comap M.subtype N) ≃ₗ[A] DirectSum (Fin n) fun (i : Fin n) => A ⧸ J i), I = ↑(∏ i : Fin n, J i)

theorem dedekind_domain_glue_local_to_global {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] : ∃ (I : FractionalIdeal (nonZeroDivisors A) K), I ≠ 0 ∧ (N ≤ M → ∀ {n : ℕ} (J : Fin n → Ideal A), (∀ (i : Fin n), J i ≠ ⊥) → ∀ (x : (↥M ⧸ Submodule.comap M.subtype N) ≃ₗ[A] DirectSum (Fin n) fun (i : Fin n) => A ⧸ J i), I = ↑(∏ i : Fin n, J i)) ∧ ∀ (v : IsDedekindDomain.HeightOneSpectrum A) (φ : V →ₗ[A] V), (∀ (x : V), x ∈ M ↔ φ x ∈ N) → FractionalIdeal.count K v I = FractionalIdeal.count K v (FractionalIdeal.spanSingleton (nonZeroDivisors A) ((algebraMap A K) (LinearMap.det φ)))

theorem moduleIndex_exists_with_product {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] : ∃ (I : FractionalIdeal (nonZeroDivisors A) K), I ≠ 0 ∧ (N ≤ M → ∀ {n : ℕ} (J : Fin n → Ideal A), (∀ (i : Fin n), J i ≠ ⊥) → ∀ (x : (↥M ⧸ Submodule.comap M.subtype N) ≃ₗ[A] DirectSum (Fin n) fun (i : Fin n) => A ⧸ J i), I = ↑(∏ i : Fin n, J i))

noncomputable def moduleIndex {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] : FractionalIdeal (nonZeroDivisors A) K

theorem moduleIndex_ne_zero {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] : moduleIndex K M N ≠ 0

theorem moduleIndex_count_eq_local {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] (v : IsDedekindDomain.HeightOneSpectrum A) (φ : V →ₗ[A] V) (hφ : ∀ (x : V), x ∈ M ↔ φ x ∈ N) : FractionalIdeal.count K v (moduleIndex K M N) = FractionalIdeal.count K v (FractionalIdeal.spanSingleton (nonZeroDivisors A) ((algebraMap A K) (LinearMap.det φ)))

theorem proposition_6_2 {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] : moduleIndex K M N ≠ 0 ∧ ∀ (v : IsDedekindDomain.HeightOneSpectrum A) (φ : V →ₗ[A] V), (∀ (x : V), x ∈ M ↔ φ x ∈ N) → FractionalIdeal.count K v (moduleIndex K M N) = FractionalIdeal.count K v (FractionalIdeal.spanSingleton (nonZeroDivisors A) ((algebraMap A K) (LinearMap.det φ)))

theorem moduleIndex_mul {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N P : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] [Module.Finite A ↥P] : moduleIndex K M P = moduleIndex K M N * moduleIndex K N P

theorem moduleIndex_self {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M : Submodule A V) [Module.Finite A ↥M] : moduleIndex K M M = 1

theorem moduleIndex_swap {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] : moduleIndex K N M = (moduleIndex K M N)⁻¹

theorem moduleIndex_eq_prod {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M N : Submodule A V) [Module.Finite A ↥M] [Module.Finite A ↥N] (hNM : N ≤ M) {n : ℕ} (I : Fin n → Ideal A) (hI : ∀ (i : Fin n), I i ≠ ⊥) (hiso : (↥M ⧸ Submodule.comap M.subtype N) ≃ₗ[A] DirectSum (Fin n) fun (i : Fin n) => A ⧸ I i) : moduleIndex K M N = ↑(∏ i : Fin n, I i)

noncomputable def concreteModuleIndex {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] (N : Submodule R M) : ℕ

theorem concreteModuleIndex_eq_cardQuot {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] (N : Submodule R M) : concreteModuleIndex N = N.cardQuot

@[simp]

theorem concreteModuleIndex_top {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] : concreteModuleIndex ⊤ = 1

theorem concreteModuleIndex_mul_tower {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] (N P : Submodule R M) (hPN : P ≤ N) : Nat.card ↥(Submodule.map P.mkQ N) * Nat.card (M ⧸ N) = Nat.card (M ⧸ P)

theorem concreteModuleIndex_ideal_mul {S : Type u_3} [CommRing S] [IsDedekindDomain S] [Module.Free ℤ S] (I J : Ideal S) : Nat.card (S ⧸ I * J) = Nat.card (S ⧸ I) * Nat.card (S ⧸ J)

theorem concreteModuleIndex_eq_natAbs_det {M : Type u_1} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℤ M) (N : Submodule ℤ M) (bN : Module.Basis ι ℤ ↥N) : (b.det (Subtype.val ∘ ⇑bN)).natAbs = concreteModuleIndex N

theorem concreteModuleIndex_eq_natAbs_det_equiv {M : Type u_1} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (N : Submodule ℤ M) {E : Type u_2} [EquivLike E M ↥N] [AddEquivClass E M ↥N] (e : E) : (LinearMap.det (N.subtype ∘ₗ (↑e).toIntLinearMap)).natAbs = concreteModuleIndex N

theorem idealNorm_eq_concreteModuleIndex {K : Type u_1} [Field K] [NumberField K] (I : Ideal (NumberField.RingOfIntegers K)) : Ideal.absNorm I = concreteModuleIndex I

theorem absNorm_mul_eq {K : Type u_1} [Field K] [NumberField K] (I J : Ideal (NumberField.RingOfIntegers K)) : Ideal.absNorm (I * J) = Ideal.absNorm I * Ideal.absNorm J

noncomputable def DedekindKummer.dedekind_kummer_bijection {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [Module.IsTorsionFree R S] {x : S} {I : Ideal R} (hI : I.IsMaximal) (hI' : I ≠ ⊥) (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x) : ↑{J : Ideal S | J ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R S) I)} ≃ ↑{d : Polynomial (R ⧸ I) | d ∈ UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}

theorem DedekindKummer.dedekind_kummer_multiplicity {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [Module.IsTorsionFree R S] {x : S} {I : Ideal R} (hI : I.IsMaximal) (hI' : I ≠ ⊥) (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x) {J : Ideal S} (hJ : J ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R S) I)) : emultiplicity J (Ideal.map (algebraMap R S) I) = emultiplicity (↑((dedekind_kummer_bijection hI hI' hx hx') ⟨J, hJ⟩)) (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))

theorem DedekindKummer.dedekind_kummer_prime_formula {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [Module.IsTorsionFree R S] {x : S} {I : Ideal R} (hI : I.IsMaximal) {Q : Polynomial R} (hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))) (hI' : I ≠ ⊥) (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x) : ↑((dedekind_kummer_bijection hI hI' hx hx').symm ⟨Polynomial.map (Ideal.Quotient.mk I) Q, hQ⟩) = Ideal.span (↑(Ideal.map (algebraMap R S) I) ∪ {(Polynomial.aeval x) Q})

theorem DedekindKummer.dedekind_kummer {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [Module.IsTorsionFree R S] {x : S} {I : Ideal R} (hI : I.IsMaximal) (hI' : I ≠ ⊥) (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x) : UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R S) I) = Multiset.map (fun (f : ↑{d : Polynomial (R ⧸ I) | d ∈ UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}) => ↑((dedekind_kummer_bijection hI hI' hx hx').symm f)) (UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach

noncomputable def idealNorm (A : Type u_1) [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain A] {B : Type u_2} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] : Ideal B →*₀ Ideal A

@[simp]

theorem idealNorm_def (A : Type u_1) [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain A] {B : Type u_2} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] : idealNorm A = Ideal.relNorm A

theorem idealNorm_apply (A : Type u_1) [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain A] {B : Type u_2} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] (I : Ideal B) : (idealNorm A) I = Ideal.span (⇑(Algebra.intNorm A B) '' ↑I)

@[simp]

theorem idealNorm_zero (A : Type u_1) [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain A] {B : Type u_2} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] : (idealNorm A) 0 = 0

theorem idealNorm_ne_zero (A : Type u_1) [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain A] {B : Type u_2} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] {I : Ideal B} (hI : I ≠ 0) : (idealNorm A) I ≠ 0

theorem idealNorm_eq_zero_iff (A : Type u_1) [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain A] {B : Type u_2} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] {I : Ideal B} : (idealNorm A) I = 0 ↔ I = 0

theorem idealNorm_mono (A : Type u_1) [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain A] {B : Type u_2} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] {I J : Ideal B} (h : I ≤ J) : (idealNorm A) I ≤ (idealNorm A) J

theorem idealNorm_principal (A : Type u_1) [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain A] {B : Type u_2} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] (α : B) : (idealNorm A) (Ideal.span {α}) = Ideal.span {(Algebra.intNorm A B) α}

theorem idealNorm_principal_free (A : Type u_1) [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain A] {B : Type u_2} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Free A B] (α : B) : (idealNorm A) (Ideal.span {α}) = Ideal.span {(Algebra.norm A) α}

theorem idealNorm_mul (A : Type u_1) [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain A] {B : Type u_2} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] (I J : Ideal B) : (idealNorm A) (I * J) = (idealNorm A) I * (idealNorm A) J

theorem idealNorm_one (A : Type u_1) [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain A] {B : Type u_2} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] : (idealNorm A) 1 = 1

theorem relNorm_ne_bot_of_ne_bot {A : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [IsIntegrallyClosed A] {B : Type u_4} [CommRing B] [IsDomain B] [IsDedekindDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] (I : Ideal B) : I ≠ ⊥ → (Ideal.relNorm A) I ≠ ⊥

theorem relNorm_det_local_generator {A : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [IsIntegrallyClosed A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_5} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] {B : Type u_6} [CommRing B] [IsDomain B] [IsDedekindDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] (I : Ideal B) (hI : I ≠ ⊥) (v : IsDedekindDomain.HeightOneSpectrum A) (φ : L →ₗ[A] L) (hφ : ∀ (x : L), x ∈ ⊤ ↔ φ x ∈ Submodule.restrictScalars A (Ideal.map (algebraMap B L) I)) : ∃ (b : B), b ≠ 0 ∧ FractionalIdeal.count K v ↑((Ideal.relNorm A) I) = FractionalIdeal.count K v ↑(Ideal.span {(Algebra.intNorm A B) b}) ∧ FractionalIdeal.count K v (FractionalIdeal.spanSingleton (nonZeroDivisors A) ((algebraMap A K) (LinearMap.det φ))) = FractionalIdeal.count K v ↑(Ideal.span {(Algebra.intNorm A B) b})

theorem relNorm_count_eq_comparison_det {A : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [IsIntegrallyClosed A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_5} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_6} [CommRing B] [IsDomain B] [IsDedekindDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] (I : Ideal B) (hI : I ≠ ⊥) (v : IsDedekindDomain.HeightOneSpectrum A) (φ : L →ₗ[A] L) (hφ : ∀ (x : L), x ∈ ⊤ ↔ φ x ∈ Submodule.restrictScalars A (Ideal.map (algebraMap B L) I)) : FractionalIdeal.count K v ↑((Ideal.relNorm A) I) = FractionalIdeal.count K v (FractionalIdeal.spanSingleton (nonZeroDivisors A) ((algebraMap A K) (LinearMap.det φ)))

theorem relNorm_eq_moduleIndex_fractional_localization {A : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [IsIntegrallyClosed A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_5} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_6} [CommRing B] [IsDomain B] [IsDedekindDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] [Module.Finite A L] (I : Ideal B) (hI : I ≠ ⊥) : ↑((Ideal.relNorm A) I) = moduleIndex K ⊤ (Submodule.restrictScalars A (Ideal.map (algebraMap B L) I))

theorem relNorm_count_eq_det_spanSingleton_local {A : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [IsIntegrallyClosed A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_5} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_6} [CommRing B] [IsDomain B] [IsDedekindDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] [Module.Finite A L] (I : Ideal B) (hI : I ≠ ⊥) (v : IsDedekindDomain.HeightOneSpectrum A) (φ : L →ₗ[A] L) (hφ : ∀ (x : L), x ∈ ⊤ ↔ φ x ∈ Submodule.restrictScalars A (Ideal.map (algebraMap B L) I)) : FractionalIdeal.count K v ↑((Ideal.relNorm A) I) = FractionalIdeal.count K v (FractionalIdeal.spanSingleton (nonZeroDivisors A) ((algebraMap A K) (LinearMap.det φ)))

theorem relNorm_count_eq_moduleIndex_count_axiom {A : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [IsIntegrallyClosed A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_5} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_6} [CommRing B] [IsDomain B] [IsDedekindDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] [Module.Finite A L] (I : Ideal B) (hI : I ≠ ⊥) (v : IsDedekindDomain.HeightOneSpectrum A) : FractionalIdeal.count K v ↑((Ideal.relNorm A) I) = FractionalIdeal.count K v (moduleIndex K ⊤ (Submodule.restrictScalars A (Ideal.map (algebraMap B L) I)))

theorem relNorm_count_eq_moduleIndex_count_local {A : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [IsIntegrallyClosed A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_5} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_6} [CommRing B] [IsDomain B] [IsDedekindDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] [Module.Finite A L] (I : Ideal B) (hI : I ≠ ⊥) (v : IsDedekindDomain.HeightOneSpectrum A) : FractionalIdeal.count K v ↑((Ideal.relNorm A) I) = FractionalIdeal.count K v (moduleIndex K ⊤ (Submodule.restrictScalars A (Ideal.map (algebraMap B L) I)))

theorem relNorm_eq_moduleIndex_fractional {A : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [IsIntegrallyClosed A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_5} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_6} [CommRing B] [IsDomain B] [IsDedekindDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] [Module.Finite A L] (I : Ideal B) (hI : I ≠ ⊥) : ↑((Ideal.relNorm A) I) = moduleIndex K ⊤ (Submodule.restrictScalars A (Ideal.map (algebraMap B L) I))

theorem relNorm_count_eq_det_count {A : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [IsIntegrallyClosed A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_5} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_6} [CommRing B] [IsDomain B] [IsDedekindDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] [Module.Finite A L] (I : Ideal B) (hI : I ≠ ⊥) (v : IsDedekindDomain.HeightOneSpectrum A) (φ : L →ₗ[A] L) (hφ : ∀ (x : L), x ∈ ⊤ ↔ φ x ∈ Submodule.restrictScalars A (Ideal.map (algebraMap B L) I)) : FractionalIdeal.count K v ↑((Ideal.relNorm A) I) = FractionalIdeal.count K v (FractionalIdeal.spanSingleton (nonZeroDivisors A) ((algebraMap A K) (LinearMap.det φ)))

theorem idealNorm_eq_moduleIndex {A : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [IsIntegrallyClosed A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_5} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_6} [CommRing B] [IsDomain B] [IsDedekindDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] [Module.Finite A L] (I : Ideal B) (hI : I ≠ ⊥) : ↑((Ideal.relNorm A) I) = moduleIndex K ⊤ (Submodule.restrictScalars A (Ideal.map (algebraMap B L) I))

theorem moduleIndex_eq_idealNorm_inv_mul {A : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [IsIntegrallyClosed A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_5} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_6} [CommRing B] [IsDomain B] [IsDedekindDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] [Module.Finite A L] (I J : Ideal B) (hI : I ≠ ⊥) (hJ : J ≠ ⊥) : moduleIndex K (Submodule.restrictScalars A (Ideal.map (algebraMap B L) I)) (Submodule.restrictScalars A (Ideal.map (algebraMap B L) J)) = (↑((Ideal.relNorm A) I))⁻¹ * ↑((Ideal.relNorm A) J)

noncomputable def fractionalIdealNorm {A : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_5} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_6} [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [Module.Finite A L] (𝔍 : FractionalIdeal (nonZeroDivisors B) L) : FractionalIdeal (nonZeroDivisors A) K

theorem fractionalIdealNorm_coeIdeal {A : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [IsIntegrallyClosed A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_5} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_6} [CommRing B] [IsDomain B] [IsDedekindDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] [Module.Finite A L] (I : Ideal B) (hI : I ≠ ⊥) : fractionalIdealNorm K ↑I = ↑((Ideal.relNorm A) I)

theorem fractionalIdeal_multiplicative_comparison_map {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] [IsIntegrallyClosed A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_4} [CommRing B] [IsDomain B] [IsDedekindDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] [Module.Finite A L] (𝔍₁ 𝔍₂ : FractionalIdeal (nonZeroDivisors B) L) : ∃ (φ : L →ₗ[A] L), (∀ (x : L), x ∈ ⊤ ↔ φ x ∈ Submodule.restrictScalars A ↑𝔍₂) ∧ (∀ (x : L), x ∈ Submodule.restrictScalars A ↑𝔍₁ ↔ φ x ∈ Submodule.restrictScalars A ↑(𝔍₁ * 𝔍₂)) ∧ (algebraMap A K) (LinearMap.det φ) ≠ 0

theorem fractionalIdealNorm_mul {A : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [IsIntegrallyClosed A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_5} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_6} [CommRing B] [IsDomain B] [IsDedekindDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] [Module.Finite A L] (𝔍₁ 𝔍₂ : FractionalIdeal (nonZeroDivisors B) L) : fractionalIdealNorm K (𝔍₁ * 𝔍₂) = fractionalIdealNorm K 𝔍₁ * fractionalIdealNorm K 𝔍₂

theorem fractionalIdealNorm_inv {A : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [IsIntegrallyClosed A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_5} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_6} [CommRing B] [IsDomain B] [IsDedekindDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] [Module.Finite A L] (𝔍 : FractionalIdeal (nonZeroDivisors B) L) : fractionalIdealNorm K 𝔍⁻¹ = (fractionalIdealNorm K 𝔍)⁻¹

theorem moduleIndex_eq_fractionalIdealNorm_inv_mul {A : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [IsIntegrallyClosed A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_5} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_6} [CommRing B] [IsDomain B] [IsDedekindDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] [Module.Finite A L] (I J : Ideal B) (hI : I ≠ ⊥) (hJ : J ≠ ⊥) : moduleIndex K (Submodule.restrictScalars A (Ideal.map (algebraMap B L) I)) (Submodule.restrictScalars A (Ideal.map (algebraMap B L) J)) = fractionalIdealNorm K ((↑I)⁻¹ * ↑J)

theorem moduleIndex_eq_fractionalIdealNorm_div {A : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [IsIntegrallyClosed A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_5} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_6} [CommRing B] [IsDomain B] [IsDedekindDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] [Module.Finite A L] (I J : Ideal B) (hI : I ≠ ⊥) (hJ : J ≠ ⊥) : moduleIndex K (Submodule.restrictScalars A (Ideal.map (algebraMap B L) I)) (Submodule.restrictScalars A (Ideal.map (algebraMap B L) J)) = fractionalIdealNorm K (↑J / ↑I)

theorem moduleIndex_eq_idealNorm_eq_fractionalIdealNorm {A : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [IsIntegrallyClosed A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_5} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_6} [CommRing B] [IsDomain B] [IsDedekindDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] [Module.Finite A L] (I J : Ideal B) (hI : I ≠ ⊥) (hJ : J ≠ ⊥) : moduleIndex K (Submodule.restrictScalars A (Ideal.map (algebraMap B L) I)) (Submodule.restrictScalars A (Ideal.map (algebraMap B L) J)) = (↑((Ideal.relNorm A) I))⁻¹ * ↑((Ideal.relNorm A) J) ∧ moduleIndex K (Submodule.restrictScalars A (Ideal.map (algebraMap B L) I)) (Submodule.restrictScalars A (Ideal.map (algebraMap B L) J)) = fractionalIdealNorm K ((↑I)⁻¹ * ↑J) ∧ moduleIndex K (Submodule.restrictScalars A (Ideal.map (algebraMap B L) I)) (Submodule.restrictScalars A (Ideal.map (algebraMap B L) J)) = fractionalIdealNorm K (↑J / ↑I)

theorem idealNorm_eq_span_norms (A : Type u_1) [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain A] {B : Type u_2} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] (I : Ideal B) : (idealNorm A) I = Ideal.span (⇑(Algebra.intNorm A B) '' ↑I)

theorem idealNorm_eq_span_fieldNorms (A : Type u_1) [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain A] {B : Type u_2} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Free A B] (I : Ideal B) : (idealNorm A) I = Ideal.span (⇑(Algebra.norm A) '' ↑I)

theorem fractionalIdealNorm_eq_span_fieldNorms {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] [IsIntegrallyClosed A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_4} [CommRing B] [IsDomain B] [IsDedekindDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] [Module.Finite A L] (I : FractionalIdeal (nonZeroDivisors B) L) : ↑(fractionalIdealNorm K I) = Submodule.span A (⇑(Algebra.norm K) '' ↑I)

theorem idealNorm_prime {A : Type u_1} [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain A] {B : Type u_2} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [PerfectField (FractionRing A)] (Q : Ideal B) (p : Ideal A) [Q.LiesOver p] [Q.IsMaximal] [p.IsMaximal] : (idealNorm A) Q = p ^ p.inertiaDeg Q

theorem idealNorm_map_eq_pow {A : Type u_1} [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain A] (B : Type u_3) [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] (I : Ideal A) : (idealNorm A) (Ideal.map (algebraMap A B) I) = I ^ Module.finrank (FractionRing A) (FractionRing B)

theorem absNorm_eq_card_quot {K : Type u_1} [Field K] [NumberField K] (I : Ideal (NumberField.RingOfIntegers K)) : Ideal.absNorm I = Nat.card (NumberField.RingOfIntegers K ⧸ I)

theorem absNorm_mul_card_quotient_eq {K : Type u_1} [Field K] [NumberField K] (I J : Ideal (NumberField.RingOfIntegers K)) (hle : J ≤ I) : Ideal.absNorm I * Nat.card ↥(Submodule.map (Submodule.mkQ J) I) = Ideal.absNorm J

theorem moduleIndex_eq_absNorm_quotient {K : Type u_1} [Field K] [NumberField K] (I J : Ideal (NumberField.RingOfIntegers K)) (hI : I ≠ ⊥) (hle : J ≤ I) (C : Ideal (NumberField.RingOfIntegers K)) (hC : J = I * C) : Nat.card ↥(Submodule.map (Submodule.mkQ J) I) = Ideal.absNorm C

theorem DedekindKummer.NF.inertiaDeg_eq_natDegree {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {p : ℕ} [Fact (Nat.Prime p)] (hp : ¬p ∣ RingOfIntegers.exponent θ) {Q : Polynomial (ZMod p)} (hQ : Q ∈ RingOfIntegers.monicFactorsMod θ p) : (Ideal.span {↑p}).inertiaDeg ↑((NumberField.Ideal.primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q, hQ⟩) = Q.natDegree

theorem DedekindKummer.NF.ramificationIdx_eq_multiplicity {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {p : ℕ} [Fact (Nat.Prime p)] (hp : ¬p ∣ RingOfIntegers.exponent θ) {Q : Polynomial (ZMod p)} (hQ : Q ∈ RingOfIntegers.monicFactorsMod θ p) : (Ideal.span {↑p}).ramificationIdx ↑((NumberField.Ideal.primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q, hQ⟩) = multiplicity Q (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))