theorem traceDual_smul_mem {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] (I : Submodule B L) (b : B) (x : L) (hx : x ∈ Submodule.traceDual A K I) : b • x ∈ Submodule.traceDual A K I

theorem traceDual_ne_zero (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L} (hI : I ≠ 0) : FractionalIdeal.dual A K I ≠ 0

theorem mem_traceDual_iff (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L} (hI : I ≠ 0) {x : L} : x ∈ FractionalIdeal.dual A K I ↔ ∀ m ∈ I, ((Algebra.traceForm K L) x) m ∈ (algebraMap A K).range

noncomputable def traceDualB (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] : FractionalIdeal (nonZeroDivisors B) L

theorem traceDual_restrictScalars_eq_coe_dual (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain B] : Submodule.restrictScalars A (Submodule.traceDual A K 1) = Submodule.restrictScalars A ↑(FractionalIdeal.dual A K 1)

theorem mem_traceDualB (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain B] {x : L} : x ∈ traceDualB A K ↔ ∀ b ∈ 1, ((Algebra.traceForm K L) x) b ∈ (algebraMap A K).range

theorem one_le_traceDualB (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain B] : 1 ≤ traceDualB A K

theorem traceDualB_inv_le_one (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain B] : (traceDualB A K)⁻¹ ≤ 1

@[reducible, inline]

noncomputable abbrev different (A : Type u_1) (B : Type u_3) [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] : Ideal B

theorem different_eq_traceDual_inv (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain B] [Module.IsTorsionFree A B] : ↑(differentIdeal A B) = (FractionalIdeal.dual A K 1)⁻¹

theorem different_inv_eq_traceDual (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain B] [Module.IsTorsionFree A B] : (↑(differentIdeal A B))⁻¹ = FractionalIdeal.dual A K 1

theorem localization_dual_comm_axiom (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (S : Submonoid A) (hS : S ≤ nonZeroDivisors A) (SA : Type u_4) [CommRing SA] [IsDomain SA] [Algebra A SA] [IsLocalization S SA] (SB : Type u_5) [CommRing SB] [IsDomain SB] [Algebra B SB] [IsLocalization (Algebra.algebraMapSubmonoid B S) SB] [Algebra SA SB] [Algebra A SB] [Algebra SA L] [Algebra SA K] [Algebra SB L] [IsScalarTower A SA SB] [IsScalarTower A B SB] [IsScalarTower B SB L] [IsScalarTower A SA L] [IsScalarTower A SA K] [IsScalarTower SA SB L] [IsScalarTower SA K L] [IsFractionRing SA K] [IsIntegrallyClosed SA] [IsFractionRing SB L] [IsDedekindDomain SB] [Module.IsTorsionFree SA SB] [Module.IsTorsionFree B SB] [IsIntegralClosure SB SA L] [Nontrivial SB] [NoZeroDivisors SB] : (FractionalIdeal.extendedHomₐ L SB) (FractionalIdeal.dual A K 1) = FractionalIdeal.dual SA K 1

theorem differentIdeal_localization (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (S : Submonoid A) (hS : S ≤ nonZeroDivisors A) (SA : Type u_4) [CommRing SA] [IsDomain SA] [Algebra A SA] [IsLocalization S SA] (SB : Type u_5) [CommRing SB] [IsDomain SB] [Algebra B SB] [IsLocalization (Algebra.algebraMapSubmonoid B S) SB] [Algebra SA SB] [Algebra A SB] [Algebra SA L] [Algebra SA K] [Algebra SB L] [IsScalarTower A SA SB] [IsScalarTower A B SB] [IsScalarTower B SB L] [IsScalarTower A SA L] [IsScalarTower A SA K] [IsScalarTower SA SB L] [IsScalarTower SA K L] [IsFractionRing SA K] [IsIntegrallyClosed SA] [IsFractionRing SB L] [IsDedekindDomain SB] [Module.IsTorsionFree SA SB] [Module.IsTorsionFree B SB] [IsIntegralClosure SB SA L] [Nontrivial SB] [NoZeroDivisors SB] : Ideal.map (algebraMap B SB) (differentIdeal A B) = differentIdeal SA SB

theorem trace_completion_compat (A : Type u_7) (K : Type u_8) (L : Type u) (B : Type u_9) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (Khat : Type u_10) [Field Khat] (Lhat : Type u) [Field Lhat] (Ahat : Type u_11) [CommRing Ahat] [IsDomain Ahat] (Bhat : Type u_12) [CommRing Bhat] [IsDomain Bhat] [Algebra A Ahat] [Algebra B Bhat] [Algebra Ahat Khat] [Algebra Bhat Lhat] [Algebra Ahat Bhat] [Algebra A Bhat] [Algebra Khat Lhat] [Algebra Ahat Lhat] [Algebra B Lhat] [Algebra K Khat] [Algebra L Lhat] [Algebra A Khat] [Algebra K Lhat] [IsScalarTower A Ahat Bhat] [IsScalarTower A B Bhat] [IsScalarTower Ahat Khat Lhat] [IsScalarTower Ahat Bhat Lhat] [IsScalarTower B Bhat Lhat] [IsScalarTower A K Khat] [IsScalarTower K Khat Lhat] [IsScalarTower K L Lhat] [IsFractionRing Ahat Khat] [IsFractionRing Bhat Lhat] [FiniteDimensional Khat Lhat] [Algebra.IsSeparable Khat Lhat] [IsIntegralClosure Bhat Ahat Lhat] [IsDedekindDomain Bhat] [Module.IsTorsionFree Ahat Bhat] [Module.IsTorsionFree B Bhat] [Nontrivial Bhat] [NoZeroDivisors Bhat] (e : Lhat ≃ₐ[Khat] TensorProduct K Khat L) (he : ∀ (y : L), e ((algebraMap L Lhat) y) = 1 ⊗ₜ[K] y) (x : L) : (algebraMap K Khat) ((Algebra.trace K L) x) = (Algebra.trace Khat Lhat) ((algebraMap L Lhat) x)

theorem completion_Bhat_span (A : Type u_7) (K : Type u_8) (L : Type u) (B : Type u_9) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (Khat : Type u_10) [Field Khat] (Lhat : Type u) [Field Lhat] (Ahat : Type u_11) [CommRing Ahat] [IsDomain Ahat] (Bhat : Type u_12) [CommRing Bhat] [IsDomain Bhat] [Algebra A Ahat] [Algebra B Bhat] [Algebra Ahat Khat] [Algebra Bhat Lhat] [Algebra Ahat Bhat] [Algebra A Bhat] [Algebra Khat Lhat] [Algebra Ahat Lhat] [Algebra B Lhat] [IsScalarTower A Ahat Bhat] [IsScalarTower A B Bhat] [IsScalarTower Ahat Khat Lhat] [IsScalarTower Ahat Bhat Lhat] [IsScalarTower B Bhat Lhat] [IsFractionRing Ahat Khat] [IsIntegrallyClosed Ahat] [IsFractionRing Bhat Lhat] [FiniteDimensional Khat Lhat] [Algebra.IsSeparable Khat Lhat] [IsIntegralClosure Bhat Ahat Lhat] [IsDedekindDomain Bhat] [Module.IsTorsionFree Ahat Bhat] [Module.IsTorsionFree B Bhat] [Nontrivial Bhat] [NoZeroDivisors Bhat] : Submodule.span Ahat (Set.range ⇑(algebraMap B Bhat)) = ⊤

theorem completion_dual_span (A : Type u_7) (K : Type u_8) (L : Type u) (B : Type u_9) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (Khat : Type u_10) [Field Khat] (Lhat : Type u) [Field Lhat] (Ahat : Type u_11) [CommRing Ahat] [IsDomain Ahat] (Bhat : Type u_12) [CommRing Bhat] [IsDomain Bhat] [Algebra A Ahat] [Algebra B Bhat] [Algebra Ahat Khat] [Algebra Bhat Lhat] [Algebra Ahat Bhat] [Algebra A Bhat] [Algebra Khat Lhat] [Algebra Ahat Lhat] [Algebra B Lhat] [Algebra L Lhat] [IsScalarTower A Ahat Bhat] [IsScalarTower A B Bhat] [IsScalarTower Ahat Khat Lhat] [IsScalarTower Ahat Bhat Lhat] [IsScalarTower B Bhat Lhat] [IsFractionRing Ahat Khat] [IsIntegrallyClosed Ahat] [IsFractionRing Bhat Lhat] [FiniteDimensional Khat Lhat] [Algebra.IsSeparable Khat Lhat] [IsIntegralClosure Bhat Ahat Lhat] [IsDedekindDomain Bhat] [Module.IsTorsionFree Ahat Bhat] [Module.IsTorsionFree B Bhat] [Nontrivial Bhat] [NoZeroDivisors Bhat] (x : Lhat) (hx : x ∈ FractionalIdeal.dual Ahat Khat 1) : x ∈ Submodule.span Bhat (⇑(algebraMap L Lhat) '' ↑(FractionalIdeal.dual A K 1))

theorem completion_dual_comm_axiom (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (Khat : Type u_4) [Field Khat] (Lhat : Type u) [Field Lhat] (Ahat : Type u_5) [CommRing Ahat] [IsDomain Ahat] (Bhat : Type u_6) [CommRing Bhat] [IsDomain Bhat] [Algebra A Ahat] [Algebra B Bhat] [Algebra Ahat Khat] [Algebra Bhat Lhat] [Algebra Ahat Bhat] [Algebra A Bhat] [Algebra Khat Lhat] [Algebra Ahat Lhat] [Algebra B Lhat] [IsScalarTower A Ahat Bhat] [IsScalarTower A B Bhat] [IsScalarTower Ahat Khat Lhat] [IsScalarTower Ahat Bhat Lhat] [IsScalarTower B Bhat Lhat] [IsFractionRing Ahat Khat] [IsIntegrallyClosed Ahat] [IsFractionRing Bhat Lhat] [FiniteDimensional Khat Lhat] [Algebra.IsSeparable Khat Lhat] [IsIntegralClosure Bhat Ahat Lhat] [IsDedekindDomain Bhat] [Module.IsTorsionFree Ahat Bhat] [Module.IsTorsionFree B Bhat] [Nontrivial Bhat] [NoZeroDivisors Bhat] [Algebra K Khat] [Algebra L Lhat] [Algebra A Khat] [Algebra K Lhat] [IsScalarTower A K Khat] [IsScalarTower K Khat Lhat] [IsScalarTower K L Lhat] [IsScalarTower B L Lhat] [Algebra.IsIntegral B Bhat] [IsScalarTower A K Khat] [IsScalarTower A Ahat Khat] [IsScalarTower K Khat Lhat] [IsScalarTower K L Lhat] [IsScalarTower B L Lhat] [Algebra.IsIntegral B Bhat] (e : Lhat ≃ₐ[Khat] TensorProduct K Khat L) (he : ∀ (y : L), e ((algebraMap L Lhat) y) = 1 ⊗ₜ[K] y) : (FractionalIdeal.extendedHomₐ Lhat Bhat) (FractionalIdeal.dual A K 1) = FractionalIdeal.dual Ahat Khat 1

theorem differentIdeal_completion (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (Khat : Type u_4) [Field Khat] (Lhat : Type u) [Field Lhat] (Ahat : Type u_5) [CommRing Ahat] [IsDomain Ahat] (Bhat : Type u_6) [CommRing Bhat] [IsDomain Bhat] [Algebra A Ahat] [Algebra B Bhat] [Algebra Ahat Khat] [Algebra Bhat Lhat] [Algebra Ahat Bhat] [Algebra A Bhat] [Algebra Khat Lhat] [Algebra Ahat Lhat] [Algebra B Lhat] [IsScalarTower A Ahat Bhat] [IsScalarTower A B Bhat] [IsScalarTower Ahat Khat Lhat] [IsScalarTower Ahat Bhat Lhat] [IsScalarTower B Bhat Lhat] [IsFractionRing Ahat Khat] [IsIntegrallyClosed Ahat] [IsFractionRing Bhat Lhat] [FiniteDimensional Khat Lhat] [Algebra.IsSeparable Khat Lhat] [IsIntegralClosure Bhat Ahat Lhat] [IsDedekindDomain Bhat] [Module.IsTorsionFree Ahat Bhat] [Module.IsTorsionFree B Bhat] [Nontrivial Bhat] [NoZeroDivisors Bhat] [Algebra K Khat] [Algebra L Lhat] [Algebra A Khat] [Algebra K Lhat] [IsScalarTower A K Khat] [IsScalarTower K Khat Lhat] [IsScalarTower K L Lhat] [IsScalarTower B L Lhat] [Algebra.IsIntegral B Bhat] [IsScalarTower A K Khat] [IsScalarTower A Ahat Khat] [IsScalarTower K Khat Lhat] [IsScalarTower K L Lhat] [IsScalarTower B L Lhat] [Algebra.IsIntegral B Bhat] (e : Lhat ≃ₐ[Khat] TensorProduct K Khat L) (he : ∀ (y : L), e ((algebraMap L Lhat) y) = 1 ⊗ₜ[K] y) : Ideal.map (algebraMap B Bhat) (differentIdeal A B) = differentIdeal Ahat Bhat

noncomputable def disc {n : ℕ} (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (x : Fin n → S) : R

theorem disc_eq_det_traceMatrix {n : ℕ} (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (x : Fin n → S) : disc R x = (Algebra.traceMatrix R x).det

theorem disc_traceMatrix_entry {n : ℕ} (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (x : Fin n → S) (i j : Fin n) : Algebra.traceMatrix R x i j = (Algebra.trace R S) (x i * x j)

theorem discr_eq_det_embeddingsMatrix_sq (K : Type u_1) {L : Type u_2} (E : Type u_3) [Field K] [Field L] [Field E] [Algebra K L] [Algebra K E] [Module.Finite K L] [IsAlgClosed E] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (b : ι → L) [Algebra.IsSeparable K L] (e : ι ≃ (L →ₐ[K] E)) : (algebraMap K E) (Algebra.discr K b) = (Algebra.embeddingsMatrixReindex K E b e).det ^ 2

theorem discr_powerBasis_eq_prod (K : Type u_1) {L : Type u_2} (E : Type u_3) [Field K] [Field L] [Field E] [Algebra K L] [Algebra K E] [Module.Finite K L] [IsAlgClosed E] (pb : PowerBasis K L) (e : Fin pb.dim ≃ (L →ₐ[K] E)) [Algebra.IsSeparable K L] : (algebraMap K E) (Algebra.discr K ⇑pb.basis) = ∏ i : Fin pb.dim, ∏ j ∈ Finset.Ioi i, ((e j) pb.gen - (e i) pb.gen) ^ 2

noncomputable def polyDiscr {R : Type u_1} [CommRing R] (f : Polynomial R) : R

theorem polyDiscr_eq_discr {R : Type u_1} [CommRing R] (f : Polynomial R) : polyDiscr f = f.discr

theorem polyDiscr_resultant {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : 0 < f.degree) : f.resultant (Polynomial.derivative f) f.natDegree (f.natDegree - 1) = (-1) ^ (f.natDegree * (f.natDegree - 1) / 2) * f.leadingCoeff * polyDiscr f

def latticeDiscrSet (A : Type u_1) (K : Type u_2) {L : Type u} [CommRing A] [Field K] [Field L] [Algebra K L] [Algebra A L] (M : Submodule A L) : Set K

def latticeDiscriminant (A : Type u_1) (K : Type u_2) {L : Type u} [CommRing A] [Field K] [Field L] [Algebra A K] [Algebra K L] [Algebra A L] (M : Submodule A L) : Submodule A K

theorem latticeDiscriminant_eq_span (A : Type u_1) (K : Type u_2) {L : Type u} [CommRing A] [Field K] [Field L] [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] (M : Submodule A L) : latticeDiscriminant A K M = Submodule.span A (latticeDiscrSet A K M)

theorem discr_mem_latticeDiscriminant (A : Type u_1) (K : Type u_2) {L : Type u} [CommRing A] [Field K] [Field L] [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] {M : Submodule A L} {b : Fin (Module.finrank K L) → L} (hb : ∀ (i : Fin (Module.finrank K L)), b i ∈ M) : Algebra.discr K b ∈ latticeDiscriminant A K M

theorem latticeDiscriminant_mono (A : Type u_1) (K : Type u_2) {L : Type u} [CommRing A] [Field K] [Field L] [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] {M N : Submodule A L} (h : M ≤ N) : latticeDiscriminant A K M ≤ latticeDiscriminant A K N

theorem discr_change_of_basis (K : Type u_2) {L : Type u} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (bK : Module.Basis (Fin (Module.finrank K L)) K L) (x : Fin (Module.finrank K L) → L) : Algebra.discr K x = (bK.toMatrix x).det ^ 2 * Algebra.discr K ⇑bK

theorem discr_mem_span_of_basis (A : Type u_1) (K : Type u_2) {L : Type u} [CommRing A] [Field K] [Field L] [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] (bK : Module.Basis (Fin (Module.finrank K L)) K L) (M : Submodule A L) (hM : ∀ x ∈ M, x ∈ Submodule.span A (Set.range ⇑bK)) (x : Fin (Module.finrank K L) → L) (hx : ∀ (i : Fin (Module.finrank K L)), x i ∈ M) : Algebra.discr K x ∈ A ∙ Algebra.discr K ⇑bK

theorem latticeDiscriminant_principal (A : Type u_1) (K : Type u_2) {L : Type u} [CommRing A] [Field K] [Field L] [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] (bK : Module.Basis (Fin (Module.finrank K L)) K L) (M : Submodule A L) (hM_le : ∀ x ∈ M, x ∈ Submodule.span A (Set.range ⇑bK)) (hM_ge : ∀ (i : Fin (Module.finrank K L)), bK i ∈ M) : latticeDiscriminant A K M = A ∙ Algebra.discr K ⇑bK

theorem latticeDiscriminant_ne_bot (A : Type u_1) (K : Type u_2) {L : Type u} [CommRing A] [Field K] [Field L] [Algebra A K] [Algebra K L] [Algebra A L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (bK : Module.Basis (Fin (Module.finrank K L)) K L) (M : Submodule A L) (hM_ge : ∀ (i : Fin (Module.finrank K L)), bK i ∈ M) : latticeDiscriminant A K M ≠ ⊥

theorem latticeDiscriminant_eq_imp_eq (A : Type u_1) (K : Type u_2) {L : Type u} [CommRing A] [Field K] [Field L] [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (hAK : Function.Injective ⇑(algebraMap A K)) (M M' : Submodule A L) (hle : M' ≤ M) (bK : Module.Basis (Fin (Module.finrank K L)) K L) (hM_le : ∀ x ∈ M, x ∈ Submodule.span A (Set.range ⇑bK)) (hM_ge : ∀ (i : Fin (Module.finrank K L)), bK i ∈ M) (bK' : Module.Basis (Fin (Module.finrank K L)) K L) (hM'_le : ∀ x ∈ M', x ∈ Submodule.span A (Set.range ⇑bK')) (hM'_ge : ∀ (i : Fin (Module.finrank K L)), bK' i ∈ M') (hD : latticeDiscriminant A K M' = latticeDiscriminant A K M) : M' = M

theorem latticeDiscriminant_isFractional (A : Type u_1) (K : Type u_2) {L : Type u} [CommRing A] [Field K] [Field L] [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsFractionRing A K] [FiniteDimensional K L] (M : Submodule A L) (bN : Module.Basis (Fin (Module.finrank K L)) K L) (hMN : ∀ x ∈ M, x ∈ Submodule.span A (Set.range ⇑bN)) : IsFractional (nonZeroDivisors A) (latticeDiscriminant A K M)

theorem latticeDiscriminant_ne_bot_of_basis (A : Type u_1) (K : Type u_2) {L : Type u} [CommRing A] [Field K] [Field L] [Algebra A K] [Algebra K L] [Algebra A L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (M : Submodule A L) (bK : Module.Basis (Fin (Module.finrank K L)) K L) (hM_ge : ∀ (i : Fin (Module.finrank K L)), bK i ∈ M) : latticeDiscriminant A K M ≠ ⊥

theorem latticeDiscriminant_isFractional_and_ne_bot (A : Type u_1) (K : Type u_2) {L : Type u} [CommRing A] [Field K] [Field L] [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] (M : Submodule A L) (bK : Module.Basis (Fin (Module.finrank K L)) K L) (hM_ge : ∀ (i : Fin (Module.finrank K L)), bK i ∈ M) (bN : Module.Basis (Fin (Module.finrank K L)) K L) (hMN : ∀ x ∈ M, x ∈ Submodule.span A (Set.range ⇑bN)) : IsFractional (nonZeroDivisors A) (latticeDiscriminant A K M) ∧ latticeDiscriminant A K M ≠ ⊥

theorem differentIdeal_eq_span_derivative (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (α : B) (hα_gen : A[α] = ⊤) (hα_field : K[(algebraMap B L) α] = ⊤) : differentIdeal A B = Ideal.span {(Polynomial.aeval α) (Polynomial.derivative (minpoly A α))}

theorem differentIdeal_eq_span_derivative_powerBasis (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (pb : PowerBasis A B) (hpb_field : K[(algebraMap B L) pb.gen] = ⊤) : differentIdeal A B = Ideal.span {(Polynomial.aeval pb.gen) (Polynomial.derivative (minpoly A pb.gen))}

noncomputable def elementDifferent (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] (α : L) : L

theorem elementDifferent_of_adjoin_eq_top (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] {α : L} (h : K⟮α⟯ = ⊤) : elementDifferent K α = (Polynomial.aeval α) (Polynomial.derivative (minpoly K α))

theorem elementDifferent_of_adjoin_ne_top (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] {α : L} (h : K⟮α⟯ ≠ ⊤) : elementDifferent K α = 0

theorem elementDifferent_of_powerBasis (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] (pb : PowerBasis K L) : elementDifferent K pb.gen = (Polynomial.aeval pb.gen) (Polynomial.derivative (minpoly K pb.gen))

noncomputable def elementDifferentB (A : Type u_1) (K : Type u_2) {L : Type u} (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra B L] [Algebra A B] [Algebra K L] (α : B) : B

theorem elementDifferentB_of_adjoin_eq_top (A : Type u_1) (K : Type u_2) {L : Type u} (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra B L] [Algebra A B] [Algebra K L] {α : B} (h : K[(algebraMap B L) α] = ⊤) : elementDifferentB A K B α = (Polynomial.aeval α) (Polynomial.derivative (minpoly A α))

theorem elementDifferentB_of_adjoin_ne_top (A : Type u_1) (K : Type u_2) {L : Type u} (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra B L] [Algebra A B] [Algebra K L] {α : B} (h : K[(algebraMap B L) α] ≠ ⊤) : elementDifferentB A K B α = 0

theorem span_elementDifferentB_le_differentIdeal (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsDedekindDomain B] [Module.IsTorsionFree A B] : Ideal.span (Set.range (elementDifferentB A K B)) ≤ differentIdeal A B

theorem iSup_conductor_primitive_eq_top (A : Type u_4) (K : Type u_5) (L : Type u) (B : Type u_6) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsDedekindDomain B] [Module.IsTorsionFree A B] : ⨆ (x : B), ⨆ (_ : K[(algebraMap B L) x] = ⊤), conductor A x = ⊤

theorem conductor_mul_differentIdeal_le_span (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsDedekindDomain B] [Module.IsTorsionFree A B] (x : B) (hx : K[(algebraMap B L) x] = ⊤) : conductor A x * differentIdeal A B ≤ Ideal.span (Set.range (elementDifferentB A K B))

theorem differentIdeal_le_span_elementDifferentB (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsDedekindDomain B] [Module.IsTorsionFree A B] : differentIdeal A B ≤ Ideal.span (Set.range (elementDifferentB A K B))

theorem differentIdeal_eq_span_elementDifferent (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsDedekindDomain B] [Module.IsTorsionFree A B] : differentIdeal A B = Ideal.span (Set.range (elementDifferentB A K B))

noncomputable def idealValuation (B : Type u_2) [CommRing B] (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (I : Ideal B) : ℕ

noncomputable def ramificationIndex (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] (𝔮 : IsDedekindDomain.HeightOneSpectrum B) : ℕ

def IsTamelyRamified (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] (𝔮 : IsDedekindDomain.HeightOneSpectrum B) : Prop

noncomputable def valuationOfRamIdx (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] (𝔮 : IsDedekindDomain.HeightOneSpectrum B) : ℕ

theorem different_valuation_lower_bound (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (hsep : Algebra.IsSeparable (A ⧸ Ideal.comap (algebraMap A B) 𝔮.asIdeal) (B ⧸ 𝔮.asIdeal)) : ramificationIndex A B 𝔮 - 1 ≤ idealValuation B 𝔮 (differentIdeal A B)

theorem different_valuation_exact (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (hsep : Algebra.IsSeparable (A ⧸ Ideal.comap (algebraMap A B) 𝔮.asIdeal) (B ⧸ 𝔮.asIdeal)) : idealValuation B 𝔮 (differentIdeal A B) = ramificationIndex A B 𝔮 - 1 + valuationOfRamIdx A B 𝔮

theorem different_valuation_upper_bound (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (hsep : Algebra.IsSeparable (A ⧸ Ideal.comap (algebraMap A B) 𝔮.asIdeal) (B ⧸ 𝔮.asIdeal)) : idealValuation B 𝔮 (differentIdeal A B) ≤ ramificationIndex A B 𝔮 - 1 + valuationOfRamIdx A B 𝔮

theorem different_valuation_eq_iff_tamelyRamified (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (hsep : Algebra.IsSeparable (A ⧸ Ideal.comap (algebraMap A B) 𝔮.asIdeal) (B ⧸ 𝔮.asIdeal)) : idealValuation B 𝔮 (differentIdeal A B) = ramificationIndex A B 𝔮 - 1 ↔ IsTamelyRamified A B 𝔮

theorem different_ne_bot_of_AKLB (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] : differentIdeal A B ≠ ⊥

theorem finite_ramified_primes (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] : {𝔮 : IsDedekindDomain.HeightOneSpectrum B | 𝔮.asIdeal ∣ differentIdeal A B}.Finite

theorem finite_ramified_primes_of_base (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] : ((fun (𝔮 : IsDedekindDomain.HeightOneSpectrum B) => Ideal.comap (algebraMap A B) 𝔮.asIdeal) '' {𝔮 : IsDedekindDomain.HeightOneSpectrum B | 𝔮.asIdeal ∣ differentIdeal A B}).Finite

def imageOfB (A : Type u_1) (L : Type u) (B : Type u_3) [CommRing A] [CommRing B] [Field L] [Algebra B L] [Algebra A B] [Algebra A L] [IsScalarTower A B L] : Submodule A L

theorem mem_imageOfB (A : Type u_1) (L : Type u) (B : Type u_3) [CommRing A] [CommRing B] [Field L] [Algebra B L] [Algebra A B] [Algebra A L] [IsScalarTower A B L] {x : L} : x ∈ imageOfB A L B ↔ ∃ (b : B), (algebraMap B L) b = x

instance imageOfB_finite (A : Type u_1) (L : Type u) (B : Type u_3) [CommRing A] [CommRing B] [Field L] [Algebra B L] [Algebra A B] [Algebra A L] [IsScalarTower A B L] [Module.Finite A B] : Module.Finite A ↥(imageOfB A L B)

def extensionDiscriminant (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A B L] : Submodule A K

theorem extensionDiscriminant_eq (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A B L] : extensionDiscriminant A K L B = latticeDiscriminant A K (imageOfB A L B)

theorem discr_mem_extensionDiscriminant (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [FiniteDimensional K L] {b : Fin (Module.finrank K L) → L} (hb : ∀ (i : Fin (Module.finrank K L)), b i ∈ imageOfB A L B) : Algebra.discr K b ∈ extensionDiscriminant A K L B

theorem discr_factorization_at_completions (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] (Ahat : Type u_4) (Khat : Type u_5) [CommRing Ahat] [IsDomain Ahat] [Field Khat] [Algebra Ahat Khat] [Algebra A Ahat] [Algebra A Khat] [Algebra K Khat] [IsScalarTower A Ahat Khat] [IsScalarTower A K Khat] [IsFractionRing Ahat Khat] [IsDedekindDomain Ahat] (𝔔 : Type u_6) [Fintype 𝔔] [DecidableEq 𝔔] (Bhat : 𝔔 → Type u_7) (Lhat : 𝔔 → Type u) [(𝔮 : 𝔔) → CommRing (Bhat 𝔮)] [∀ (𝔮 : 𝔔), IsDomain (Bhat 𝔮)] [(𝔮 : 𝔔) → Field (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra (Bhat 𝔮) (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsFractionRing (Bhat 𝔮) (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra Ahat (Bhat 𝔮)] [(𝔮 : 𝔔) → Algebra Ahat (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra Khat (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower Ahat Khat (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower Ahat (Bhat 𝔮) (Lhat 𝔮)] [∀ (𝔮 : 𝔔), FiniteDimensional Khat (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra K (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra L (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower K L (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower K Khat (Lhat 𝔮)] (k : K) : k ∈ latticeDiscrSet A K (imageOfB A L B) → ∃ (d : 𝔔 → Khat), (∀ (𝔮 : 𝔔), d 𝔮 ∈ ↑(extensionDiscriminant Ahat Khat (Lhat 𝔮) (Bhat 𝔮))) ∧ (algebraMap K Khat) k = ∏ 𝔮 : 𝔔, d 𝔮

def discriminantBaseChange (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A B L] (Ahat : Type u_4) (Khat : Type u_5) [CommRing Ahat] [Field Khat] [Algebra Ahat Khat] [Algebra K Khat] : Submodule Ahat Khat

theorem discr_generator_mem_local_product (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] (Ahat : Type u_4) (Khat : Type u_5) [CommRing Ahat] [IsDomain Ahat] [Field Khat] [Algebra Ahat Khat] [Algebra A Ahat] [Algebra A Khat] [Algebra K Khat] [IsScalarTower A Ahat Khat] [IsScalarTower A K Khat] [IsFractionRing Ahat Khat] [IsDedekindDomain Ahat] (𝔔 : Type u_6) [Fintype 𝔔] [DecidableEq 𝔔] (Bhat : 𝔔 → Type u_7) (Lhat : 𝔔 → Type u) [(𝔮 : 𝔔) → CommRing (Bhat 𝔮)] [∀ (𝔮 : 𝔔), IsDomain (Bhat 𝔮)] [(𝔮 : 𝔔) → Field (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra (Bhat 𝔮) (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsFractionRing (Bhat 𝔮) (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra Ahat (Bhat 𝔮)] [(𝔮 : 𝔔) → Algebra Ahat (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra Khat (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower Ahat Khat (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower Ahat (Bhat 𝔮) (Lhat 𝔮)] [∀ (𝔮 : 𝔔), FiniteDimensional Khat (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra K (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra L (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower K L (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower K Khat (Lhat 𝔮)] (k : K) (hk : k ∈ latticeDiscrSet A K (imageOfB A L B)) : (algebraMap K Khat) k ∈ ∏ 𝔮 : 𝔔, extensionDiscriminant Ahat Khat (Lhat 𝔮) (Bhat 𝔮)

theorem discr_baseChange_mem_local_product (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] (Ahat : Type u_4) (Khat : Type u_5) [CommRing Ahat] [IsDomain Ahat] [Field Khat] [Algebra Ahat Khat] [Algebra A Ahat] [Algebra A Khat] [Algebra K Khat] [IsScalarTower A Ahat Khat] [IsScalarTower A K Khat] [IsFractionRing Ahat Khat] [IsDedekindDomain Ahat] (𝔔 : Type u_6) [Fintype 𝔔] [DecidableEq 𝔔] (Bhat : 𝔔 → Type u_7) (Lhat : 𝔔 → Type u) [(𝔮 : 𝔔) → CommRing (Bhat 𝔮)] [∀ (𝔮 : 𝔔), IsDomain (Bhat 𝔮)] [(𝔮 : 𝔔) → Field (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra (Bhat 𝔮) (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsFractionRing (Bhat 𝔮) (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra Ahat (Bhat 𝔮)] [(𝔮 : 𝔔) → Algebra Ahat (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra Khat (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower Ahat Khat (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower Ahat (Bhat 𝔮) (Lhat 𝔮)] [∀ (𝔮 : 𝔔), FiniteDimensional Khat (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra K (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra L (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower K L (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower K Khat (Lhat 𝔮)] (d : Khat) (hd : d ∈ ⇑(algebraMap K Khat) '' ↑(extensionDiscriminant A K L B)) : d ∈ ∏ 𝔮 : 𝔔, extensionDiscriminant Ahat Khat (Lhat 𝔮) (Bhat 𝔮)

theorem weak_approx_local_discr_bound (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] (Ahat : Type u_4) (Khat : Type u_5) [CommRing Ahat] [IsDomain Ahat] [Field Khat] [Algebra Ahat Khat] [Algebra A Ahat] [Algebra A Khat] [Algebra K Khat] [IsScalarTower A Ahat Khat] [IsScalarTower A K Khat] [IsFractionRing Ahat Khat] [IsDedekindDomain Ahat] (𝔔 : Type u_6) [Fintype 𝔔] [DecidableEq 𝔔] (Bhat : 𝔔 → Type u_7) (Lhat : 𝔔 → Type u) [(𝔮 : 𝔔) → CommRing (Bhat 𝔮)] [∀ (𝔮 : 𝔔), IsDomain (Bhat 𝔮)] [(𝔮 : 𝔔) → Field (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra (Bhat 𝔮) (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsFractionRing (Bhat 𝔮) (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra Ahat (Bhat 𝔮)] [(𝔮 : 𝔔) → Algebra Ahat (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra Khat (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower Ahat Khat (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower Ahat (Bhat 𝔮) (Lhat 𝔮)] [∀ (𝔮 : 𝔔), FiniteDimensional Khat (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra K (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra L (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower K L (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower K Khat (Lhat 𝔮)] : ∃ d ∈ latticeDiscrSet A K (imageOfB A L B), ∏ 𝔮 : 𝔔, extensionDiscriminant Ahat Khat (Lhat 𝔮) (Bhat 𝔮) ≤ Ahat ∙ (algebraMap K Khat) d

theorem local_discr_principal_generator (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] (Ahat : Type u_4) (Khat : Type u_5) [CommRing Ahat] [IsDomain Ahat] [Field Khat] [Algebra Ahat Khat] [Algebra A Ahat] [Algebra A Khat] [Algebra K Khat] [IsScalarTower A Ahat Khat] [IsScalarTower A K Khat] [IsFractionRing Ahat Khat] [IsDedekindDomain Ahat] (𝔔 : Type u_6) [Fintype 𝔔] [DecidableEq 𝔔] (Bhat : 𝔔 → Type u_7) (Lhat : 𝔔 → Type u) [(𝔮 : 𝔔) → CommRing (Bhat 𝔮)] [∀ (𝔮 : 𝔔), IsDomain (Bhat 𝔮)] [(𝔮 : 𝔔) → Field (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra (Bhat 𝔮) (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsFractionRing (Bhat 𝔮) (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra Ahat (Bhat 𝔮)] [(𝔮 : 𝔔) → Algebra Ahat (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra Khat (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower Ahat Khat (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower Ahat (Bhat 𝔮) (Lhat 𝔮)] [∀ (𝔮 : 𝔔), FiniteDimensional Khat (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra K (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra L (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower K L (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower K Khat (Lhat 𝔮)] : ∃ d ∈ extensionDiscriminant A K L B, ∏ 𝔮 : 𝔔, extensionDiscriminant Ahat Khat (Lhat 𝔮) (Bhat 𝔮) ≤ Ahat ∙ (algebraMap K Khat) d

theorem local_discr_product_le_baseChange (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] (Ahat : Type u_4) (Khat : Type u_5) [CommRing Ahat] [IsDomain Ahat] [Field Khat] [Algebra Ahat Khat] [Algebra A Ahat] [Algebra A Khat] [Algebra K Khat] [IsScalarTower A Ahat Khat] [IsScalarTower A K Khat] [IsFractionRing Ahat Khat] [IsDedekindDomain Ahat] (𝔔 : Type u_6) [Fintype 𝔔] [DecidableEq 𝔔] (Bhat : 𝔔 → Type u_7) (Lhat : 𝔔 → Type u) [(𝔮 : 𝔔) → CommRing (Bhat 𝔮)] [∀ (𝔮 : 𝔔), IsDomain (Bhat 𝔮)] [(𝔮 : 𝔔) → Field (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra (Bhat 𝔮) (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsFractionRing (Bhat 𝔮) (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra Ahat (Bhat 𝔮)] [(𝔮 : 𝔔) → Algebra Ahat (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra Khat (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower Ahat Khat (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower Ahat (Bhat 𝔮) (Lhat 𝔮)] [∀ (𝔮 : 𝔔), FiniteDimensional Khat (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra K (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra L (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower K L (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower K Khat (Lhat 𝔮)] : ∏ 𝔮 : 𝔔, extensionDiscriminant Ahat Khat (Lhat 𝔮) (Bhat 𝔮) ≤ discriminantBaseChange A K L B Ahat Khat

theorem discriminantBaseChange_eq_prod (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] (Ahat : Type u_4) (Khat : Type u_5) [CommRing Ahat] [IsDomain Ahat] [Field Khat] [Algebra Ahat Khat] [Algebra A Ahat] [Algebra A Khat] [Algebra K Khat] [IsScalarTower A Ahat Khat] [IsScalarTower A K Khat] [IsFractionRing Ahat Khat] [IsDedekindDomain Ahat] (𝔔 : Type u_6) [Fintype 𝔔] [DecidableEq 𝔔] (Bhat : 𝔔 → Type u_7) (Lhat : 𝔔 → Type u) [(𝔮 : 𝔔) → CommRing (Bhat 𝔮)] [∀ (𝔮 : 𝔔), IsDomain (Bhat 𝔮)] [(𝔮 : 𝔔) → Field (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra (Bhat 𝔮) (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsFractionRing (Bhat 𝔮) (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra Ahat (Bhat 𝔮)] [(𝔮 : 𝔔) → Algebra Ahat (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra Khat (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower Ahat Khat (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower Ahat (Bhat 𝔮) (Lhat 𝔮)] [∀ (𝔮 : 𝔔), FiniteDimensional Khat (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra K (Lhat 𝔮)] [(𝔮 : 𝔔) → Algebra L (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower K L (Lhat 𝔮)] [∀ (𝔮 : 𝔔), IsScalarTower K Khat (Lhat 𝔮)] : discriminantBaseChange A K L B Ahat Khat = ∏ 𝔮 : 𝔔, extensionDiscriminant Ahat Khat (Lhat 𝔮) (Bhat 𝔮)

theorem extensionDiscriminant_isIntegral (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] : ∃ (D : Ideal A), extensionDiscriminant A K L B = IsLocalization.coeSubmodule K D

theorem discr_coeIdeal_count_eq_det_spanSingleton (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] (D : Ideal A) (hD : extensionDiscriminant A K L B = IsLocalization.coeSubmodule K D) (v : IsDedekindDomain.HeightOneSpectrum A) (φ : L →ₗ[A] L) (hφ : ∀ (x : L), x ∈ Submodule.restrictScalars A (Submodule.traceDual A K 1) ↔ φ x ∈ imageOfB A L B) : FractionalIdeal.count K v ↑D = FractionalIdeal.count K v (FractionalIdeal.spanSingleton (nonZeroDivisors A) ((algebraMap A K) (LinearMap.det φ)))

theorem discr_count_eq_traceDualIndex_count_local (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite A L] (D : Ideal A) (hD : extensionDiscriminant A K L B = IsLocalization.coeSubmodule K D) (v : IsDedekindDomain.HeightOneSpectrum A) : FractionalIdeal.count K v ↑D = FractionalIdeal.count K v (moduleIndex K (Submodule.restrictScalars A (Submodule.traceDual A K 1)) (imageOfB A L B))

theorem discr_eq_traceDualIndex (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite A L] (D : Ideal A) (hD : extensionDiscriminant A K L B = IsLocalization.coeSubmodule K D) : ↑D = moduleIndex K (Submodule.restrictScalars A (Submodule.traceDual A K 1)) (imageOfB A L B)

theorem discr_count_eq_traceDualIndex_count (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite A L] (D : Ideal A) (hD : extensionDiscriminant A K L B = IsLocalization.coeSubmodule K D) (v : IsDedekindDomain.HeightOneSpectrum A) : FractionalIdeal.count K v ↑D = FractionalIdeal.count K v (moduleIndex K (Submodule.restrictScalars A (Submodule.traceDual A K 1)) (imageOfB A L B))

theorem discr_ideal_ne_zero (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] (D : Ideal A) (hD : extensionDiscriminant A K L B = IsLocalization.coeSubmodule K D) : ↑D ≠ 0

theorem relNorm_different_count_eq_traceDual_det (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite A L] (v : IsDedekindDomain.HeightOneSpectrum A) (φ : L →ₗ[A] L) (hφ : ∀ (x : L), x ∈ Submodule.restrictScalars A (Submodule.traceDual A K 1) ↔ φ x ∈ imageOfB A L B) : FractionalIdeal.count K v ↑((Ideal.relNorm A) (differentIdeal A B)) = FractionalIdeal.count K v (FractionalIdeal.spanSingleton (nonZeroDivisors A) ((algebraMap A K) (LinearMap.det φ)))

theorem traceDual_moduleIndex_count_eq_relNorm_different_count (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite A L] (v : IsDedekindDomain.HeightOneSpectrum A) : FractionalIdeal.count K v (moduleIndex K (Submodule.restrictScalars A (Submodule.traceDual A K 1)) (imageOfB A L B)) = FractionalIdeal.count K v ↑((Ideal.relNorm A) (differentIdeal A B))

theorem traceDualIndex_eq_relNorm_different (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite A L] : moduleIndex K (Submodule.restrictScalars A (Submodule.traceDual A K 1)) (imageOfB A L B) = ↑((Ideal.relNorm A) (differentIdeal A B))

theorem discr_localEq_relNorm_different_at_maximal (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite A L] (D : Ideal A) (hD : extensionDiscriminant A K L B = IsLocalization.coeSubmodule K D) (P : Ideal A) (hP : P.IsMaximal) : Ideal.map (algebraMap A (Localization.AtPrime P)) D = Ideal.map (algebraMap A (Localization.AtPrime P)) ((Ideal.relNorm A) (differentIdeal A B))

theorem extensionDiscriminant_eq_coeSubmodule_relNorm_different (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite A L] : extensionDiscriminant A K L B = IsLocalization.coeSubmodule K ((Ideal.relNorm A) (differentIdeal A B))

theorem discr_eq_relNorm_different (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite A L] (D : Ideal A) (hD : extensionDiscriminant A K L B = IsLocalization.coeSubmodule K D) : D = (Ideal.relNorm A) (differentIdeal A B)

theorem extensionDiscriminant_local_eq_relNorm (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite A L] (D : Ideal A) (hD : extensionDiscriminant A K L B = IsLocalization.coeSubmodule K D) (P : Ideal A) (hP : P.IsMaximal) : Ideal.map (algebraMap A (Localization.AtPrime P)) D = Ideal.map (algebraMap A (Localization.AtPrime P)) ((Ideal.relNorm A) (differentIdeal A B))

theorem extensionDiscriminant_eq_relNorm_different (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Module.Finite A L] : extensionDiscriminant A K L B = IsLocalization.coeSubmodule K ((Ideal.relNorm A) (differentIdeal A B))

theorem discr_ne_zero_iff_traceForm_nondegenerate {ι : Type u_1} [DecidableEq ι] [Fintype ι] (K : Type u_2) {R : Type u_3} [Field K] [CommRing R] [Algebra K R] (b : Module.Basis ι K R) : Algebra.discr K ⇑b ≠ 0 ↔ (Algebra.traceForm K R).Nondegenerate

theorem discr_ne_zero_iff_isFiniteEtale {ι : Type u_1} [DecidableEq ι] [Fintype ι] (K : Type u_2) {R : Type u_3} [Field K] [CommRing R] [Algebra K R] (b : Module.Basis ι K R) (thm_5_20 : EtaleAlgebra.IsFiniteEtaleAlgebra K R ↔ (Algebra.traceForm K R).Nondegenerate) : Algebra.discr K ⇑b ≠ 0 ↔ EtaleAlgebra.IsFiniteEtaleAlgebra K R

theorem discr_ne_zero_of_isFiniteEtale {ι : Type u_1} [DecidableEq ι] [Fintype ι] (K : Type u_2) {R : Type u_3} [Field K] [CommRing R] [Algebra K R] (b : Module.Basis ι K R) (thm_5_20 : EtaleAlgebra.IsFiniteEtaleAlgebra K R ↔ (Algebra.traceForm K R).Nondegenerate) (hR : EtaleAlgebra.IsFiniteEtaleAlgebra K R) : Algebra.discr K ⇑b ≠ 0

theorem isFiniteEtale_of_discr_ne_zero {ι : Type u_1} [DecidableEq ι] [Fintype ι] (K : Type u_2) {R : Type u_3} [Field K] [CommRing R] [Algebra K R] (b : Module.Basis ι K R) (thm_5_20 : EtaleAlgebra.IsFiniteEtaleAlgebra K R ↔ (Algebra.traceForm K R).Nondegenerate) (h : Algebra.discr K ⇑b ≠ 0) : EtaleAlgebra.IsFiniteEtaleAlgebra K R

theorem not_dvd_differentIdeal_iff_unramified {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDomain B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] (𝔮 : IsDedekindDomain.HeightOneSpectrum B) : ¬𝔮.asIdeal ∣ differentIdeal A B ↔ Algebra.IsUnramifiedAt A 𝔮.asIdeal

theorem dvd_differentIdeal_iff_ramified {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDomain B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] (𝔮 : IsDedekindDomain.HeightOneSpectrum B) : 𝔮.asIdeal ∣ differentIdeal A B ↔ ¬Algebra.IsUnramifiedAt A 𝔮.asIdeal

theorem unramified_iff_not_dvd_discriminant (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) : (∀ (𝔮 : IsDedekindDomain.HeightOneSpectrum B), 𝔮.asIdeal.LiesOver 𝔭.asIdeal → Algebra.IsUnramifiedAt A 𝔮.asIdeal) ↔ ¬extensionDiscriminant A K L B ≤ Submodule.map (Algebra.linearMap A K) (Submodule.restrictScalars A 𝔭.asIdeal)

theorem unramified_iff_not_dvd_different_and_discriminant (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A L] : (∀ (𝔮 : IsDedekindDomain.HeightOneSpectrum B), ¬𝔮.asIdeal ∣ differentIdeal A B ↔ Algebra.IsUnramifiedAt A 𝔮.asIdeal) ∧ ∀ (𝔭 : IsDedekindDomain.HeightOneSpectrum A), (∀ (𝔮 : IsDedekindDomain.HeightOneSpectrum B), 𝔮.asIdeal.LiesOver 𝔭.asIdeal → Algebra.IsUnramifiedAt A 𝔮.asIdeal) ↔ ¬extensionDiscriminant A K L B ≤ Submodule.map (Algebra.linearMap A K) (Submodule.restrictScalars A 𝔭.asIdeal)

def subalgebraConductor {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (𝒪 : Subalgebra A B) : Ideal B

theorem mem_subalgebraConductor_iff {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {𝒪 : Subalgebra A B} {a : B} : a ∈ subalgebraConductor 𝒪 ↔ ∀ (b : B), a * b ∈ 𝒪

theorem subalgebraConductor_le {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (𝒪 : Subalgebra A B) : ↑(subalgebraConductor 𝒪) ⊆ ↑𝒪

def imageOfSubalgebra (A : Type u_1) (L : Type u) (B : Type u_3) [CommRing A] [CommRing B] [Field L] [Algebra B L] [Algebra A B] [Algebra A L] [IsScalarTower A B L] (𝒪 : Subalgebra A B) : Submodule A L

def orderDiscriminant (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A B L] (𝒪 : Subalgebra A B) : Submodule A K

theorem orderDiscriminant_eq_norm_conductor_mul (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] (𝒪 : Subalgebra A B) : orderDiscriminant A K L B 𝒪 = Submodule.map (Algebra.linearMap A K) (Ideal.spanNorm A (subalgebraConductor 𝒪)) * extensionDiscriminant A K L B