From dab307a1dd2f1d42ba3687ec487586b6aac9f7d1 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Wed, 20 Dec 2023 14:14:53 +0100 Subject: [PATCH] bump --- FltRegular/NumberTheory/AuxLemmas.lean | 16 ----- FltRegular/NumberTheory/Different.lean | 89 ++---------------------- FltRegular/NumberTheory/Finrank.lean | 24 ++----- FltRegular/NumberTheory/GaloisPrime.lean | 61 ++++------------ FltRegular/NumberTheory/Hilbert90.lean | 4 +- FltRegular/NumberTheory/Hilbert92.lean | 12 ++-- FltRegular/NumberTheory/Hilbert94.lean | 12 ++-- FltRegular/NumberTheory/Unramified.lean | 2 +- lake-manifest.json | 4 +- 9 files changed, 43 insertions(+), 181 deletions(-) diff --git a/FltRegular/NumberTheory/AuxLemmas.lean b/FltRegular/NumberTheory/AuxLemmas.lean index 141a75eb..4dd8a9ec 100644 --- a/FltRegular/NumberTheory/AuxLemmas.lean +++ b/FltRegular/NumberTheory/AuxLemmas.lean @@ -264,22 +264,6 @@ lemma Matrix.mulVec_injective {n R} [CommRing R] [Fintype n] [DecidableEq n] (M : Matrix n n R) (hM : IsUnit M.det) : Function.Injective (mulVec M) := (M.mulVec_bijective hM).injective --- Mathlib/RingTheory/FractionalIdeal.lean -namespace FractionalIdeal - -open nonZeroDivisors - -variable {R K} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] -variable {I J : FractionalIdeal R⁰ K} - -lemma le_inv_comm (hI : I ≠ 0) (hJ : J ≠ 0) : I ≤ J⁻¹ ↔ J ≤ I⁻¹ := by - rw [inv_eq_one_div, inv_eq_one_div, le_div_iff_mul_le hI, le_div_iff_mul_le hJ, mul_comm] - -lemma inv_le_comm (hI : I ≠ 0) (hJ : J ≠ 0) : I⁻¹ ≤ J ↔ J⁻¹ ≤ I := by - simpa using le_inv_comm (inv_ne_zero hI) (inv_ne_zero hJ) - -end FractionalIdeal - -- -- Mathlib/RingTheory/Localization/FractionRing.lean -- noncomputable -- instance {A B} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDomain B] diff --git a/FltRegular/NumberTheory/Different.lean b/FltRegular/NumberTheory/Different.lean index 6df9b35c..cfbe2621 100644 --- a/FltRegular/NumberTheory/Different.lean +++ b/FltRegular/NumberTheory/Different.lean @@ -189,89 +189,9 @@ lemma FractionalIdeal.le_dual₂_inv_aux (I J: FractionalIdeal B⁰ L) (hI) (hIJ variable [IsDedekindDomain B] [IsFractionRing B L] variable (A K) - -lemma FractionalIdeal.inv_le_dual₂ (I : FractionalIdeal B⁰ L) (hI) : - I⁻¹ ≤ dual₂ A K I hI := - le_dual₂_inv_aux _ _ _ (le_of_eq (mul_inv_cancel hI)) - -lemma FractionalIdeal.dual₂_inv_le (I : FractionalIdeal B⁰ L) (hI) : - (dual₂ A K I hI)⁻¹ ≤ I := by - convert mul_right_mono ((dual₂ A K I hI)⁻¹) - (mul_left_mono I (FractionalIdeal.inv_le_dual₂ A K I hI)) using 1 - · simp only [mul_inv_cancel hI, one_mul] - · simp only [mul_inv_cancel (FractionalIdeal.dual₂_ne_zero (hI := hI)), mul_assoc, mul_one] - variable (B) - -def differentIdeal [NoZeroSMulDivisors A B] : Ideal B := - (1 / traceFormDualSubmodule A (FractionRing A) 1 : Submodule B (FractionRing B)).comap - (Algebra.linearMap B (FractionRing B)) - -lemma coeSubmodule_differentIdeal' [NoZeroSMulDivisors A B] (hAB : Algebra.IsIntegral A B) - [IsSeparable (FractionRing A) (FractionRing B)] - [FiniteDimensional (FractionRing A) (FractionRing B)] : - coeSubmodule (FractionRing B) (differentIdeal A B) = - 1 / traceFormDualSubmodule A (FractionRing A) 1 := by - have : IsIntegralClosure B A (FractionRing B) := - isIntegralClosure_of_isIntegrallyClosed _ _ _ hAB - rw [coeSubmodule, differentIdeal, Submodule.map_comap_eq, inf_eq_right] - have := FractionalIdeal.dual₂_inv_le A (FractionRing A) (1 : FractionalIdeal B⁰ (FractionRing B)) - one_ne_zero - have : _ ≤ ((1 : FractionalIdeal B⁰ (FractionRing B)) : Submodule B (FractionRing B)) := this - simp only [← one_div, FractionalIdeal.val_eq_coe, - FractionalIdeal.coe_div FractionalIdeal.dual₂_ne_zero] at this - dsimp [FractionalIdeal.dual₂] at this - simpa only [FractionalIdeal.coe_one] using this - -lemma coeSubmodule_differentIdeal [NoZeroSMulDivisors A B] : - coeSubmodule L (differentIdeal A B) = 1 / traceFormDualSubmodule A K 1 := by - have : (FractionRing.algEquiv B L).toLinearEquiv.comp (Algebra.linearMap B (FractionRing B)) = - Algebra.linearMap B L := by ext; simp - rw [coeSubmodule, ← this] - have H : RingHom.comp (algebraMap (FractionRing A) (FractionRing B)) - ↑(FractionRing.algEquiv A K).symm.toRingEquiv = - RingHom.comp ↑(FractionRing.algEquiv B L).symm.toRingEquiv (algebraMap K L) - · apply IsLocalization.ringHom_ext A⁰ - ext - simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_comp, RingHom.coe_coe, - AlgEquiv.coe_ringEquiv, Function.comp_apply, AlgEquiv.commutes, - ← IsScalarTower.algebraMap_apply] - rw [IsScalarTower.algebraMap_apply A B L, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply] - have : IsSeparable (FractionRing A) (FractionRing B) := IsSeparable_of_equiv_equiv _ _ H - have : FiniteDimensional (FractionRing A) (FractionRing B) := Module.Finite_of_equiv_equiv _ _ H - simp only [AlgEquiv.toLinearEquiv_toLinearMap, Submodule.map_comp] - rw [← coeSubmodule, coeSubmodule_differentIdeal' _ _ (IsIntegralClosure.isIntegral_algebra _ L), - Submodule.map_div, ← AlgEquiv.toAlgHom_toLinearMap, Submodule.map_one] - congr 1 - refine (map_equiv_traceFormDualSubmodule A K _).trans ?_ - congr 1 - ext - simp - variable (L) -lemma coeIdeal_different_ideal [NoZeroSMulDivisors A B] : - ↑(differentIdeal A B) = - (FractionalIdeal.dual₂ A K (1 : FractionalIdeal B⁰ L) one_ne_zero)⁻¹ := by - apply FractionalIdeal.coeToSubmodule_injective - simp only [FractionalIdeal.coe_div FractionalIdeal.dual₂_ne_zero, - FractionalIdeal.coe_coeIdeal, coeSubmodule_differentIdeal A K, inv_eq_one_div] - simp only [FractionalIdeal.dual₂, FractionalIdeal.coe_mk, FractionalIdeal.coe_one] - -lemma differentialIdeal_le_fractionalIdeal_iff - (I : FractionalIdeal B⁰ L) (hI : I ≠ 0) [NoZeroSMulDivisors A B] : - differentIdeal A B ≤ I ↔ (((I⁻¹ : _) : Submodule B L).restrictScalars A).map - ((Algebra.trace K L).restrictScalars A) ≤ 1 := by - rw [coeIdeal_different_ideal A K B L, FractionalIdeal.inv_le_comm FractionalIdeal.dual₂_ne_zero hI] - refine le_traceFormDualSubmodule.trans ?_ - simp - -lemma differentialIdeal_le_iff (I : Ideal B) (hI : I ≠ ⊥) [NoZeroSMulDivisors A B] : - differentIdeal A B ≤ I ↔ (((I⁻¹ : FractionalIdeal B⁰ L) : Submodule B L).restrictScalars A).map - ((Algebra.trace K L).restrictScalars A) ≤ 1 := - (FractionalIdeal.coeIdeal_le_coeIdeal _).symm.trans - (differentialIdeal_le_fractionalIdeal_iff A K B L (I : FractionalIdeal B⁰ L) (by simpa)) - lemma pow_sub_one_dvd_differentIdeal_aux [IsDedekindDomain A] [NoZeroSMulDivisors A B] [Module.Finite A B] {p : Ideal A} [p.IsMaximal] (P : Ideal B) (e : ℕ) (he : 0 < e) (hp : p ≠ ⊥) @@ -297,7 +217,7 @@ lemma pow_sub_one_dvd_differentIdeal_aux simp only [inv_inv, ha, FractionalIdeal.coeIdeal_mul, inv_div, ne_eq, FractionalIdeal.coeIdeal_eq_zero, mul_div_assoc] rw [div_self (by simpa), mul_one] - rw [Ideal.dvd_iff_le, differentialIdeal_le_iff A K B L _ (pow_ne_zero _ hPbot), hP, + rw [Ideal.dvd_iff_le, differentialIdeal_le_iff (K := K) (L := L) (pow_ne_zero _ hPbot), hP, Submodule.map_le_iff_le_comap] intro x hx rw [Submodule.restrictScalars_mem, FractionalIdeal.mem_coe, @@ -411,12 +331,13 @@ lemma conductor_mul_differentIdeal [NoZeroSMulDivisors A B] (x : B) (hx : Algebra.adjoin K {algebraMap B L x} = ⊤) : (conductor A x) * differentIdeal A B = Ideal.span {aeval x (derivative (minpoly A x))} := by classical + have onz := one_ne_zero (α := FractionalIdeal B⁰ L) have hAx : IsIntegral A x := IsIntegralClosure.isIntegral A L x haveI := IsIntegralClosure.isFractionRing_of_finite_extension A K L B apply FractionalIdeal.coeIdeal_injective (K := L) simp only [FractionalIdeal.coeIdeal_mul, FractionalIdeal.coeIdeal_span_singleton] - rw [coeIdeal_different_ideal A K B L, - mul_inv_eq_iff_eq_mul₀ FractionalIdeal.dual₂_ne_zero] + rw [coeIdeal_differentIdeal A K L B, + mul_inv_eq_iff_eq_mul₀ (FractionalIdeal.dual_ne_zero A K onz)] apply FractionalIdeal.coeToSubmodule_injective simp only [FractionalIdeal.coe_coeIdeal, FractionalIdeal.coe_mul, FractionalIdeal.coe_spanSingleton, Submodule.span_singleton_mul] @@ -426,7 +347,7 @@ lemma conductor_mul_differentIdeal [NoZeroSMulDivisors A B] have : algebraMap B L (aeval x (derivative (minpoly A x))) ≠ 0 · rwa [minpoly.isIntegrallyClosed_eq_field_fractions K L hAx, derivative_map, aeval_map_algebraMap, aeval_algebraMap_apply] at hne₁ - rw [Submodule.mem_smul_iff_inv this, FractionalIdeal.mem_coe, FractionalIdeal.mem_dual₂, + rw [Submodule.mem_smul_iff_inv this, FractionalIdeal.mem_coe, FractionalIdeal.mem_dual onz, mem_coeIdeal_conductor] have hne₂ : (aeval (algebraMap B L x) (derivative (minpoly K (algebraMap B L x))))⁻¹ ≠ 0 · rwa [ne_eq, inv_eq_zero] diff --git a/FltRegular/NumberTheory/Finrank.lean b/FltRegular/NumberTheory/Finrank.lean index 222b9154..a2fe7f19 100644 --- a/FltRegular/NumberTheory/Finrank.lean +++ b/FltRegular/NumberTheory/Finrank.lean @@ -160,8 +160,9 @@ lemma Module.finite_iff_rank_lt_aleph0 [Module R M] [Module.Free R M] : Set.finite_coe_iff.mpr ((Module.Free.chooseBasis R M).finite_index_of_rank_lt_aleph0 H) exact Module.Finite.of_basis (Module.Free.chooseBasis R M) -lemma Module.finite_of_finrank_pos [Module.Free R M] (hf : 0 < FiniteDimensional.finrank R M) : - Module.Finite R M := Module.finite_iff_rank_lt_aleph0.mpr (Cardinal.toNat_pos.mp hf).2 +@[deprecated Module.finite_of_finrank_pos] +lemma Module.finite_of_finrank_pos' [Module.Free R M] (hf : 0 < FiniteDimensional.finrank R M) : + Module.Finite R M := finite_of_finrank_pos hf lemma FiniteDimensional.finrank_quotient_of_le_torsion (hN : N ≤ Submodule.torsion R M) : finrank R (M ⧸ N) = finrank R M := by @@ -211,21 +212,10 @@ lemma FiniteDimensional.finrank_of_surjective_of_le_torsion {M'} [AddCommGroup M rw [← LinearMap.range_eq_map l, LinearMap.range_eq_top.mpr hl] at this simpa only [finrank_top] using this -lemma FiniteDimensional.finrank_eq_zero_iff [IsDomain R] : - finrank R M = 0 ↔ Module.IsTorsion R M := by - constructor - · delta Module.IsTorsion - contrapose! - rintro ⟨x, hx⟩ - rw [← Nat.one_le_iff_ne_zero] - have : LinearIndependent R (fun _ : Unit ↦ x) - · exact linearIndependent_iff.mpr (fun l hl ↦ Finsupp.unique_ext <| not_not.mp fun H ↦ - hx ⟨_, mem_nonZeroDivisors_of_ne_zero H⟩ ((Finsupp.total_unique _ _ _).symm.trans hl)) - exact FiniteDimensional.fintype_card_le_finrank_of_linearIndependent' this - · intro h - rw [← FiniteDimensional.finrank_quotient_of_le_torsion _ - ((Submodule.isTorsion'_iff_torsion'_eq_top (R := R) _).mp h).ge] - exact finrank_zero_of_subsingleton +@[deprecated FiniteDimensional.finrank_eq_zero_iff_isTorsion] +lemma FiniteDimensional.finrank_eq_zero_iff' [IsDomain R] : + finrank R M = 0 ↔ Module.IsTorsion R M := + FiniteDimensional.finrank_eq_zero_iff_isTorsion lemma FiniteDimensional.finrank_add_finrank_quotient_of_free [IsDomain R] [IsPrincipalIdealRing R] [Module.Free R M] diff --git a/FltRegular/NumberTheory/GaloisPrime.lean b/FltRegular/NumberTheory/GaloisPrime.lean index 0f5547a7..fe046c74 100644 --- a/FltRegular/NumberTheory/GaloisPrime.lean +++ b/FltRegular/NumberTheory/GaloisPrime.lean @@ -1,4 +1,5 @@ import FltRegular.NumberTheory.AuxLemmas +import Mathlib.RingTheory.IntegralRestrict /-! # Galois action on primes @@ -110,37 +111,8 @@ variable (R K S L : Type*) [CommRing R] [CommRing S] [Algebra R S] [Field K] [Fi [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] -- [IsNoetherian R S] [IsIntegralClosure S R L] [FiniteDimensional K L] -noncomputable -def galRestrictHom : (L →ₐ[K] L) →* (S →ₐ[R] S) where - toFun := fun f ↦ (IsIntegralClosure.equiv R (integralClosure R L) L S).toAlgHom.comp - (((f.restrictScalars R).comp (IsScalarTower.toAlgHom R S L)).codRestrict - (integralClosure R L) (fun x ↦ IsIntegral.map _ (IsIntegralClosure.isIntegral R L x))) - map_one' := by - ext x - apply (IsIntegralClosure.equiv R (integralClosure R L) L S).symm.injective - ext - dsimp - simp only [AlgEquiv.symm_apply_apply, AlgHom.coe_codRestrict, AlgHom.coe_comp, - AlgHom.coe_restrictScalars', IsScalarTower.coe_toAlgHom', Function.comp_apply, - AlgHom.one_apply] - exact (IsIntegralClosure.algebraMap_equiv R S L (integralClosure R L) x).symm - map_mul' := by - intros σ₁ σ₂ - ext x - apply (IsIntegralClosure.equiv R (integralClosure R L) L S).symm.injective - ext - dsimp - simp only [AlgEquiv.symm_apply_apply, AlgHom.coe_codRestrict, AlgHom.coe_comp, - AlgHom.coe_restrictScalars', IsScalarTower.coe_toAlgHom', Function.comp_apply, - AlgHom.mul_apply, IsIntegralClosure.algebraMap_equiv, Subalgebra.algebraMap_eq] - dsimp - -lemma algebraMap_galRestrictHom_apply (σ : L →ₐ[K] L) (x : S) : - algebraMap S L (galRestrictHom R K S L σ x) = σ (algebraMap S L x) := by - simp [galRestrictHom, Subalgebra.algebraMap_eq] - lemma prod_galRestrictHom_eq_norm [IsGalois K L] (x) : - (∏ σ : L ≃ₐ[K] L, galRestrictHom R K S L σ x) = + (∏ σ : L ≃ₐ[K] L, galRestrictHom R K L S σ x) = algebraMap R S (IsIntegralClosure.mk' (R := R) R (Algebra.norm K <| algebraMap S L x) (Algebra.isIntegral_norm K (IsIntegralClosure.isIntegral R L x).algebraMap)) := by apply IsIntegralClosure.algebraMap_injective S R L @@ -148,16 +120,11 @@ lemma prod_galRestrictHom_eq_norm [IsGalois K L] (x) : simp only [map_prod, algebraMap_galRestrictHom_apply, IsIntegralClosure.algebraMap_mk', Algebra.norm_eq_prod_automorphisms, AlgHom.coe_coe, RingHom.coe_comp, Function.comp_apply] -noncomputable -def galRestrict : (L ≃ₐ[K] L) →* (S ≃ₐ[R] S) := - MonoidHom.comp (algHomUnitsEquiv R S) - ((Units.map <| galRestrictHom R K S L).comp (algHomUnitsEquiv K L).symm) - noncomputable instance (p : Ideal R) : MulAction (L ≃ₐ[K] L) (primesOver S p) where - smul := fun σ P ↦ ⟨Ideal.comap (galRestrict R K S L σ⁻¹) P, P.2.1.comap _, by + smul := fun σ P ↦ ⟨Ideal.comap (galRestrict R K L S σ⁻¹) P, P.2.1.comap _, by refine Eq.trans ?_ P.2.2 - rw [← Ideal.comap_coe (galRestrict R K S L _), Ideal.comap_comap, + rw [← Ideal.comap_coe (galRestrict R K L S _), Ideal.comap_comap, ← AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_algebraMap]⟩ one_smul := by intro p @@ -169,12 +136,12 @@ instance (p : Ideal R) : MulAction (L ≃ₐ[K] L) (primesOver S p) where intro σ₁ σ₂ p ext1 show Ideal.comap _ _ = Ideal.comap _ (Ideal.comap _ _) - rw [← Ideal.comap_coe (galRestrict R K S L _), ← Ideal.comap_coe (galRestrict R K S L _), - ← Ideal.comap_coe (galRestrict R K S L _), Ideal.comap_comap, mul_inv_rev, map_mul] + rw [← Ideal.comap_coe (galRestrict R K L S _), ← Ideal.comap_coe (galRestrict R K L S _), + ← Ideal.comap_coe (galRestrict R K L S _), Ideal.comap_comap, mul_inv_rev, map_mul] rfl lemma coe_smul_primesOver {p : Ideal R} (σ : L ≃ₐ[K] L) (P : primesOver S p) : - (↑(σ • P) : Ideal S) = Ideal.comap (galRestrict R K S L σ⁻¹) P := rfl + (↑(σ • P) : Ideal S) = Ideal.comap (galRestrict R K L S σ⁻¹) P := rfl open BigOperators @@ -221,7 +188,7 @@ instance [IsGalois K L] (p : Ideal R) : have hQ := Q.prop.1 -- Then `σ y ∉ Q` for all `σ`, or else `1 = x + y ∈ σ⁻¹ • Q`. -- This implies that `∏ σ y ∉ Q`. - have : ∏ σ : L ≃ₐ[K] L, galRestrictHom R K S L σ y ∉ (Q : Ideal S) + have : ∏ σ : L ≃ₐ[K] L, galRestrictHom R K L S σ y ∉ (Q : Ideal S) · apply prod_mem (S := (Q : Ideal S).primeCompl) intro σ _ hσ apply (isMaximal_of_mem_primesOver hp (σ⁻¹ • Q).prop).ne_top @@ -229,7 +196,7 @@ instance [IsGalois K L] (p : Ideal R) : apply add_mem · suffices ↑(σ⁻¹ • Q) ∣ I from (Ideal.dvd_iff_le.mp this) hx exact Finset.dvd_prod_of_mem _ (Finset.mem_univ _) - · show galRestrictHom R K S L ↑(σ⁻¹⁻¹) y ∈ (Q : Ideal S) + · show galRestrictHom R K L S ↑(σ⁻¹⁻¹) y ∈ (Q : Ideal S) rwa [inv_inv] -- OTOH we show that `∏ σ y ∈ Q`. -- Since `∏ σ y` is the norm of `y ∈ P`, it falls in `R ∩ Q = p = R ∩ P` as desired. @@ -240,14 +207,14 @@ instance [IsGalois K L] (p : Ideal R) : apply hy rw [Ideal.mem_span_singleton] refine dvd_trans ?_ (Finset.dvd_prod_of_mem _ (Finset.mem_univ 1)) - show y ∣ galRestrictHom R K S L 1 y + show y ∣ galRestrictHom R K L S 1 y rw [map_one] exact dvd_rfl -- Which gives a contradiction and hence there is some `σ` such that `σ • P = Q`. lemma exists_comap_galRestrict_eq [IsGalois K L] {p : Ideal R} {P₁ P₂ : Ideal S} (hP₁ : P₁ ∈ primesOver S p) (hP₂ : P₂ ∈ primesOver S p) : - ∃ σ, P₁.comap (galRestrict R K S L σ) = P₂ := + ∃ σ, P₁.comap (galRestrict R K L S σ) = P₂ := ⟨_, congr_arg Subtype.val (MulAction.exists_smul_eq (L ≃ₐ[K] L) (⟨P₁, hP₁⟩ : primesOver S p) ⟨P₂, hP₂⟩).choose_spec⟩ @@ -298,7 +265,7 @@ lemma Ideal.ramificationIdxIn_eq_ramificationIdx [IsGalois K L] (p : Ideal R) (P rw [dif_pos this] have ⟨σ, hσ⟩ := exists_comap_galRestrict_eq R K S L hP this.choose_spec rw [← hσ] - exact Ideal.ramificationIdx_comap_eq (galRestrict R K S L σ) p P + exact Ideal.ramificationIdx_comap_eq (galRestrict R K L S σ) p P lemma Ideal.inertiaDegIn_eq_inertiaDeg [IsGalois K L] (p : Ideal R) (P : Ideal S) (hP : P ∈ primesOver S p) [p.IsMaximal] : @@ -308,7 +275,7 @@ lemma Ideal.inertiaDegIn_eq_inertiaDeg [IsGalois K L] (p : Ideal R) (P : Ideal S rw [dif_pos this] have ⟨σ, hσ⟩ := exists_comap_galRestrict_eq R K S L hP this.choose_spec rw [← hσ] - exact Ideal.inertiaDeg_comap_eq (galRestrict R K S L σ) p P + exact Ideal.inertiaDeg_comap_eq (galRestrict R K L S σ) p P open FiniteDimensional @@ -393,7 +360,7 @@ lemma prod_smul_primesOver [IsGalois K L] (p : Ideal R) (P : primesOver S p) [p. simp_rw [primesOver_bot (S := S) (IsIntegralClosure.isIntegral_algebra R L), Set.mem_singleton_iff] at this simp_rw [coe_smul_primesOver, this, - Ideal.comap_bot_of_injective _ (galRestrict R K S L _).injective, Finset.prod_const, + Ideal.comap_bot_of_injective _ (galRestrict R K L S _).injective, Finset.prod_const, Ideal.map_bot, Ideal.inertiaDegIn_bot R S (IsIntegralClosure.isIntegral_algebra R L)] refine (zero_pow ?_).trans (zero_pow ?_).symm · rw [pos_iff_ne_zero, Finset.card_univ, Ne.def, Fintype.card_eq_zero_iff] diff --git a/FltRegular/NumberTheory/Hilbert90.lean b/FltRegular/NumberTheory/Hilbert90.lean index aa4846bf..e676d265 100644 --- a/FltRegular/NumberTheory/Hilbert90.lean +++ b/FltRegular/NumberTheory/Hilbert90.lean @@ -131,7 +131,7 @@ variable [IsIntegralClosure B A L] [IsDomain B] lemma Hilbert90_integral (σ : L ≃ₐ[K] L) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) (η : B) (hη : Algebra.norm K (algebraMap B L η) = 1) : - ∃ ε : B, ε ≠ 0 ∧ η * galRestrict A K B L σ ε = ε := by + ∃ ε : B, ε ≠ 0 ∧ η * galRestrict A K L B σ ε = ε := by haveI : NoZeroSMulDivisors A L := by rw [NoZeroSMulDivisors.iff_algebraMap_injective, IsScalarTower.algebraMap_eq A K L] exact (algebraMap K L).injective.comp (IsFractionRing.injective A K) @@ -157,7 +157,7 @@ lemma Hilbert90_integral (σ : L ≃ₐ[K] L) (hσ : ∀ x, x ∈ Subgroup.zpowe apply IsIntegralClosure.algebraMap_injective B A L rw [map_mul, ← hε] congr 1 - exact algebraMap_galRestrictHom_apply A K B L σ x + exact algebraMap_galRestrictHom_apply A K L B σ x · intro e rw [(map_eq_zero _).mp e, zero_div] at hε rw [hε, Algebra.norm_zero] at hη diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean index a8b027e2..cf05c519 100644 --- a/FltRegular/NumberTheory/Hilbert92.lean +++ b/FltRegular/NumberTheory/Hilbert92.lean @@ -42,7 +42,7 @@ def systemOfUnits.isMaximal {r} (hf : finrank ℤ G = r * (p - 1)) [Module A G] apply Nonempty.some apply (@nonempty_fintype _ ?_) apply Module.finite_of_fg_torsion - rw [← FiniteDimensional.finrank_eq_zero_iff, finrank_quotient', + rw [← FiniteDimensional.finrank_eq_zero_iff_isTorsion, finrank_quotient', finrank_spanA p hp _ _ sys.linearIndependent, hf, mul_comm, Nat.sub_self] noncomputable @@ -256,13 +256,13 @@ instance : IsIntegralClosure ↥(𝓞 K) ↥(𝓞 k) K := isIntegralClosure_of_i (fun x ↦ IsIntegral.tower_top (IsIntegralClosure.isIntegral ℤ K x)) lemma coe_galRestrictHom_apply (σ : K →ₐ[k] K) (x) : - (galRestrictHom (𝓞 k) k (𝓞 K) K σ x : K) = σ x := - algebraMap_galRestrictHom_apply (𝓞 k) k (𝓞 K) K σ x + (galRestrictHom (𝓞 k) k K (𝓞 K) σ x : K) = σ x := + algebraMap_galRestrictHom_apply (𝓞 k) k K (𝓞 K) σ x noncomputable def relativeUnitsMap (σ : K →ₐ[k] K) : RelativeUnits k K →* RelativeUnits k K := by apply QuotientGroup.lift _ - ((QuotientGroup.mk' _).comp (Units.map (galRestrictHom (𝓞 k) k (𝓞 K) K σ))) + ((QuotientGroup.mk' _).comp (Units.map (galRestrictHom (𝓞 k) k K (𝓞 K) σ))) rintro _ ⟨i, rfl⟩ simp only [MonoidHom.mem_ker, MonoidHom.coe_comp, QuotientGroup.coe_mk', Function.comp_apply, QuotientGroup.eq_one_iff, MonoidHom.mem_range, Units.ext_iff, Units.coe_map, MonoidHom.coe_coe, @@ -270,7 +270,7 @@ def relativeUnitsMap (σ : K →ₐ[k] K) : RelativeUnits k K →* RelativeUnits lemma relativeUnitsMap_mk (σ : K →ₐ[k] K) (x : (𝓞 K)ˣ) : relativeUnitsMap σ (QuotientGroup.mk x) = - QuotientGroup.mk (Units.map (galRestrictHom (𝓞 k) k (𝓞 K) K σ) x) := rfl + QuotientGroup.mk (Units.map (galRestrictHom (𝓞 k) k K (𝓞 K) σ) x) := rfl @[simps] noncomputable @@ -390,7 +390,7 @@ noncomputable abbrev CyclotomicIntegers.mk : Polynomial ℤ →+* CyclotomicIntegers p := AdjoinRoot.mk _ lemma relativeUnitsModule_zeta_smul (x) : - (zeta p) • mkG x = mkG (Units.map (galRestrictHom (𝓞 k) k (𝓞 K) K σ) x) := by + (zeta p) • mkG x = mkG (Units.map (galRestrictHom (𝓞 k) k K (𝓞 K) σ) x) := by let φ := (addMonoidEndRingEquivInt _ (Monoid.EndAdditive <| relativeUnitsMap <| ((algHomUnitsEquiv _ _).symm σ).val)) show QuotientAddGroup.mk ((Module.AEval'.of φ).symm <| diff --git a/FltRegular/NumberTheory/Hilbert94.lean b/FltRegular/NumberTheory/Hilbert94.lean index 53c5cf69..0065c20c 100644 --- a/FltRegular/NumberTheory/Hilbert94.lean +++ b/FltRegular/NumberTheory/Hilbert94.lean @@ -20,16 +20,16 @@ variable {A B} [CommRing A] [CommRing B] [Algebra A B] [Algebra A L] [Algebra A [Algebra B L] [IsScalarTower A B L] [IsScalarTower A K L] [IsFractionRing A K] [IsIntegralClosure B A L] -lemma comap_span_galRestrict_eq_of_cyclic (β : B) (η : Bˣ) (hβ : η * (galRestrict A K B L σ) β = β) +lemma comap_span_galRestrict_eq_of_cyclic (β : B) (η : Bˣ) (hβ : η * (galRestrict A K L B σ) β = β) (σ' : L ≃ₐ[K] L) : - (Ideal.span {β}).comap (galRestrict A K B L σ') = Ideal.span {β} := by + (Ideal.span {β}).comap (galRestrict A K L B σ') = Ideal.span {β} := by suffices : (Ideal.span {β}).map - (galRestrict A K B L σ'⁻¹).toRingEquiv.toRingHom = Ideal.span {β} + (galRestrict A K L B σ'⁻¹).toRingEquiv.toRingHom = Ideal.span {β} · rwa [RingEquiv.toRingHom_eq_coe, Ideal.map_comap_of_equiv, map_inv] at this apply_fun (Ideal.span {·}) at hβ rw [← Ideal.span_singleton_mul_span_singleton, Ideal.span_singleton_eq_top.mpr η.isUnit, ← Ideal.one_eq_top, one_mul, ← Set.image_singleton, ← Ideal.map_span] at hβ - change Ideal.map (galRestrict A K B L σ : B →+* B) _ = _ at hβ + change Ideal.map (galRestrict A K L B σ : B →+* B) _ = _ at hβ generalize σ'⁻¹ = σ' obtain ⟨n, rfl : σ ^ n = σ'⟩ := mem_powers_iff_mem_zpowers.mpr (hσ σ') rw [map_pow] @@ -61,10 +61,10 @@ theorem exists_not_isPrincipal_and_isPrincipal_map_aux apply hη' use a conv_rhs => enter [1]; rw [← hβ] - rw [map_mul, ← AlgHom.coe_coe σ, ← algebraMap_galRestrictHom_apply A K B L σ a] + rw [map_mul, ← AlgHom.coe_coe σ, ← algebraMap_galRestrictHom_apply A K L B σ a] refine (mul_div_cancel _ ?_).symm · rw [ne_eq, (injective_iff_map_eq_zero' _).mp (IsIntegralClosure.algebraMap_injective B A L), - (injective_iff_map_eq_zero' _).mp (galRestrict A K B L σ).injective] + (injective_iff_map_eq_zero' _).mp (galRestrict A K L B σ).injective] exact a.isUnit.ne_zero · exact (mul_ne_zero_iff.mp hβ_zero).1 · rw [hβ'] diff --git a/FltRegular/NumberTheory/Unramified.lean b/FltRegular/NumberTheory/Unramified.lean index 759de786..8b5f9163 100644 --- a/FltRegular/NumberTheory/Unramified.lean +++ b/FltRegular/NumberTheory/Unramified.lean @@ -52,7 +52,7 @@ lemma prod_primesOverFinset_of_isUnramified [IsUnramified R S] [IsDedekindDomain exact IsUnramified.isUnramifiedAt _ hp _ hP lemma comap_map_eq_of_isUnramified [IsGalois K L] [IsUnramified R S] (I : Ideal S) - (hI : ∀ σ : L ≃ₐ[K] L, I.comap (galRestrict R K S L σ) = I) : + (hI : ∀ σ : L ≃ₐ[K] L, I.comap (galRestrict R K L S σ) = I) : (I.comap (algebraMap R S)).map (algebraMap R S) = I := by classical have : IsDomain S := diff --git a/lake-manifest.json b/lake-manifest.json index 283c739a..041399c6 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "9dd24a3493cceefa2bede383f21e4ef548990b68", + "rev": "71e11a6be0e43dabcba416e1af15b5bbbbfc9dde", "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "d61c95e1653dffe3f92c8927a905826929f50bce", + "rev": "3f93618efe0e23ebaa39b88e28a5297940088690", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,