progress

Author: riccardobrasca

FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean

@@ -379,6 +379,10 @@ theorem unit_inv_conj_not_neg_zeta_runity (h : p ≠ 2) (u : Rˣ) (n : ℕ) (hp
 lemma NumberField.RingOfIntegers.eq_iff {K : Type*} [Field K] {x y : 𝓞 K} :
     (x : K) = (y : K) ↔ x = y :=
   NumberField.RingOfIntegers.ext_iff.symm
+instance {K L : Type*} [Field K] [Ring L] [Algebra K L] : Algebra (𝓞 K) L :=
+  inferInstanceAs (Algebra (integralClosure _ _) L)
+instance {K L : Type*} [Field K] [Ring L] [Algebra K L] :  IsScalarTower (𝓞 K) K L :=
+  inferInstanceAs (IsScalarTower (integralClosure _ _) K L)
 
 -- this proof has mild coe annoyances rn
 theorem unit_inv_conj_is_root_of_unity (h : p ≠ 2) (hp : (p : ℕ).Prime) (u : Rˣ) :

FltRegular/NumberTheory/Hilbert92.lean

@@ -234,16 +234,16 @@ variable
     (hKL : finrank k K = p) (σ : K ≃ₐ[k] K) (hσ : ∀ x, x ∈ Subgroup.zpowers σ)
 
 def RelativeUnits (k K : Type*) [Field k] [Field K] [Algebra k K] :=
-  ((𝓞 K)ˣ ⧸ (MonoidHom.range <| Units.map (algebraMap ↥(𝓞 k) ↥(𝓞 K) : ↥(𝓞 k) →* ↥(𝓞 K))))
+  ((𝓞 K)ˣ ⧸ (MonoidHom.range <| Units.map (algebraMap (𝓞 k) (𝓞 K) : (𝓞 k) →* (𝓞 K))))
 
 instance : CommGroup (RelativeUnits k K) := by delta RelativeUnits; infer_instance
 
 attribute [local instance] IsCyclic.commGroup
 
 attribute [local instance 2000] inst_ringOfIntegersAlgebra Algebra.toSMul Algebra.toModule
 
-instance : IsScalarTower ↥(𝓞 k) ↥(𝓞 K) K := IsScalarTower.of_algebraMap_eq (fun _ ↦ rfl)
-instance : IsIntegralClosure ↥(𝓞 K) ↥(𝓞 k) K := IsIntegralClosure.of_isIntegrallyClosed _ _ _
+instance : IsScalarTower (𝓞 k) (𝓞 K) K := IsScalarTower.of_algebraMap_eq (fun _ ↦ rfl)
+instance : IsIntegralClosure (𝓞 K) (𝓞 k) K := IsIntegralClosure.of_isIntegrallyClosed _ _ _
   (fun x ↦ IsIntegral.tower_top (IsIntegralClosure.isIntegral ℤ K x))
 
 lemma coe_galRestrictHom_apply (σ : K →ₐ[k] K) (x) :
@@ -328,7 +328,7 @@ lemma isTors' : Module.IsTorsionBySet ℤ[X]
     Subalgebra.coe_toSubsemiring, Algebra.norm_eq_prod_automorphisms]
   rw [← hKL, ← IsGalois.card_aut_eq_finrank, ← orderOf_eq_card_of_forall_mem_zpowers hσ,
     ← Fin.prod_univ_eq_prod_range, ← (finEquivZPowers σ <| isOfFinOrder_of_finite _).symm.prod_comp]
-  simp only [pow_finEquivZPowers_symm_apply, coe_galRestrictHom_apply, AlgHom.coe_coe]
+  simp only [pow_finEquivZPowers_symm_apply, coe_galRestrictHom_apply, AlgHom.coe_coe, map_prod]
   rw [Finset.prod_set_coe (α := K ≃ₐ[k] K) (β := K) (f := fun i ↦ i ↑x) (Subgroup.zpowers σ)]
   congr
   ext x
@@ -406,7 +406,7 @@ lemma NumberField.Units.finrank_eq : finrank ℤ (Additive (𝓞 k)ˣ) = NumberF
 local instance : Module.Finite ℤ (Additive <| RelativeUnits k K) := by
   delta RelativeUnits
   show Module.Finite ℤ (Additive (𝓞 K)ˣ ⧸ AddSubgroup.toIntSubmodule (Subgroup.toAddSubgroup
-    (MonoidHom.range <| Units.map (algebraMap ↥(𝓞 k) ↥(𝓞 K) : ↥(𝓞 k) →* ↥(𝓞 K)))))
+    (MonoidHom.range <| Units.map (algebraMap (𝓞 k) (𝓞 K) : (𝓞 k) →* (𝓞 K)))))
   infer_instance
 
 local instance : Module.Finite ℤ (Additive <| relativeUnitsWithGenerator p hp hKL σ hσ) := by
@@ -432,10 +432,10 @@ lemma finrank_G : finrank ℤ G = (Units.rank k + 1) * (↑p - 1) := by
   rw [← Submodule.torsion_int]
   refine (FiniteDimensional.finrank_quotient_of_le_torsion _ le_rfl).trans ?_
   show finrank ℤ (Additive (𝓞 K)ˣ ⧸ AddSubgroup.toIntSubmodule (Subgroup.toAddSubgroup
-    (MonoidHom.range <| Units.map (algebraMap ↥(𝓞 k) ↥(𝓞 K) : ↥(𝓞 k) →* ↥(𝓞 K))))) = _
+    (MonoidHom.range <| Units.map (algebraMap (𝓞 k) (𝓞 K) : (𝓞 k) →* (𝓞 K))))) = _
   rw [FiniteDimensional.finrank_quotient]
   show _ - finrank ℤ (LinearMap.range <| AddMonoidHom.toIntLinearMap <|
-    MonoidHom.toAdditive <| Units.map (algebraMap ↥(𝓞 k) ↥(𝓞 K) : ↥(𝓞 k) →* ↥(𝓞 K))) = _
+    MonoidHom.toAdditive <| Units.map (algebraMap (𝓞 k) (𝓞 K) : (𝓞 k) →* (𝓞 K))) = _
   rw [LinearMap.finrank_range_of_inj, NumberField.Units.finrank_eq, NumberField.Units.finrank_eq,
     NumberField.Units.rank_of_isUnramified (k := k), add_mul, one_mul, mul_tsub, mul_one, mul_comm,
       add_tsub_assoc_of_le, tsub_add_eq_add_tsub, hKL]
@@ -470,16 +470,13 @@ lemma unitlifts_spec (S : systemOfUnits p G (NumberField.Units.rank k + 1)) (i)
   simp only [toMul_ofMul, Quotient.out_eq', ofMul_toMul]
   exact Quotient.out_eq' _
 
-set_option synthInstance.maxHeartbeats 80000 in
 lemma u_lemma2 (u v : (𝓞 K)ˣ) (hu : u = v / (σ v : K)) : (mkG u) = (1 - zeta p : A) • (mkG v) := by
   rw [sub_smul, one_smul, relativeUnitsModule_zeta_smul, ← unit_to_U_div]
   congr
   rw [eq_div_iff_mul_eq']
   ext
-  simp only [Units.val_mul, Units.coe_map, MonoidHom.coe_coe, Submonoid.coe_mul,
-    Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring, coe_galRestrictHom_apply, hu]
-  refine div_mul_cancel₀ _ ?_
-  simp only [ne_eq, map_eq_zero, ZeroMemClass.coe_eq_zero, Units.ne_zero, not_false_eq_true]
+  simp only [Units.val_mul, Units.coe_map, MonoidHom.coe_coe, map_mul, coe_galRestrictHom_apply, hu]
+  exact div_mul_cancel₀ _ (by simp)
 
 open multiplicity in
 theorem padicValNat_dvd_iff_le' {p : ℕ} (hp : p ≠ 1) {a n : ℕ} (ha : a ≠ 0) :
@@ -701,11 +698,9 @@ lemma Hilbert92ish_aux1 (n : ℕ) (H : Fin n → Additive (𝓞 K)ˣ) (ζ : (
     letI J : (𝓞 K)ˣ := (Additive.toMul (∑ i : Fin n, ι i • H i)) *
       (Units.map (algebraMap (𝓞 k) (𝓞 K)).toMonoidHom ζ) ^ (-a)
     Algebra.norm k (S := K) ((J : (𝓞 K)ˣ) : K) = 1 := by
-  simp only [toMul_sum, toMul_zsmul, RingHom.toMonoidHom_eq_coe, zpow_neg, Units.val_mul,
-    Units.coe_prod, Submonoid.coe_mul, Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring,
-    Submonoid.coe_finset_prod, Units.coe_zpow, map_mul, map_prod, ← Units.coe_val_inv,
-    norm_map_inv, norm_map_zpow, hKL, Units.coe_map, MonoidHom.coe_coe,
-    RingOfInteger.coe_algebraMap_apply, Algebra.norm_algebraMap]
+  simp only [toMul_sum, toMul_zsmul, zpow_neg, Units.val_mul, Units.coe_prod, map_mul, map_prod,
+    Units.coe_zpow, map_mul, map_prod, ← Units.coe_val_inv, norm_map_inv, norm_map_zpow, hKL,
+    Units.coe_map, RingOfInteger.coe_algebraMap_apply, Algebra.norm_algebraMap]
   apply_fun Additive.toMul at ha
   apply_fun ((↑) : (𝓞 k)ˣ → k) at ha
   simp only [toMul_sum, toMul_zsmul, Units.coe_prod, Submonoid.coe_finset_prod, hη,
@@ -768,7 +763,7 @@ lemma unit_to_U_neg (x) : mkG (-x) = mkG x := by
   simp only [Units.val_neg, Units.val_one, OneMemClass.coe_one,
     Units.coe_map, MonoidHom.coe_coe, map_neg, map_one]
 
-instance : CommGroup (↥(𝓞 k))ˣ := inferInstance
+instance : CommGroup ((𝓞 k))ˣ := inferInstance
 
 lemma IsPrimitiveRoot.one_left_iff {M} [CommMonoid M] {n : ℕ} :
     IsPrimitiveRoot (1 : M) n ↔ n = 1 :=

FltRegular/NumberTheory/KummersLemma/Field.lean

@@ -108,12 +108,6 @@ lemma irreducible_map_poly :
   rw [mul_pow, (hpri.out.odd_of_ne_two (PNat.coe_injective.ne hp)).neg_pow, hb, neg_neg,
     div_mul_cancel₀ _ (pow_ne_zero _ (hζ.sub_one_ne_zero hpri.out.one_lt))]
 
---Add to mathlib
-instance {K L : Type*} [Field K] [Ring L] [Algebra K L] : Algebra (𝓞 K) L :=
-  inferInstanceAs (Algebra (integralClosure _ _) L)
-instance {K L : Type*} [Field K] [Ring L] [Algebra K L] :  IsScalarTower (𝓞 K) K L :=
-  inferInstanceAs (IsScalarTower (integralClosure _ _) K L)
-
 theorem aeval_poly {L : Type*} [Field L] [Algebra K L] (α : L)
     (e : α ^ (p : ℕ) = algebraMap K L u) (m : ℕ) :
     aeval (((1 : L) - ζ ^ m • α) / (algebraMap K L (ζ - 1))) (poly hp hζ u hcong) = 0 := by