import Definitions.Def_NumberField_AdelicLevel import Mathlib.NumberTheory.Padics.HeightOneSpectrum set_option autoImplicit false noncomputable section open NumberField IsDedekindDomain IsDedekindDomain.HeightOneSpectrum WithZero open Rat.HeightOneSpectrum NumberField.AdelicLevel namespace RatIdele local notation "π”Έβ„š" => AdeleRing (π“ž β„š) β„š local notation "π”Έβ„šf" => FiniteAdeleRing (π“ž β„š) β„š section Primes theorem natCast_mem_asIdeal_iff (v : HeightOneSpectrum (π“ž β„š)) (n : β„•) : ((n : π“ž β„š)) ∈ v.asIdeal ↔ natGenerator v ∣ n := by rw [natGenerator_dvd_iff, show ((n : β„•) : β„€) = Rat.IsIntegralClosure.intEquiv (π“ž β„š) ((n : π“ž β„š)) from (map_natCast _ n).symm] exact Ideal.apply_mem_of_equiv_iff.symm theorem natCast_natGenerator_ne_zero (v : HeightOneSpectrum (π“ž β„š)) : ((natGenerator v : β„•) : π“ž β„š) β‰  0 := Nat.cast_ne_zero.mpr (prime_natGenerator v).ne_zero theorem prime_natCast_natGenerator (v : HeightOneSpectrum (π“ž β„š)) : Prime ((natGenerator v : β„•) : π“ž β„š) := by have hcast : ((natGenerator v : β„•) : π“ž β„š) = Rat.ringOfIntegersEquiv.symm ((natGenerator v : β„•) : β„€) := (map_natCast (Rat.ringOfIntegersEquiv.symm : β„€ β†’+* π“ž β„š) _).symm rw [hcast] exact (MulEquiv.prime_iff Rat.ringOfIntegersEquiv.symm.toMulEquiv).mpr (Nat.prime_iff_prime_int.mp (prime_natGenerator v)) theorem asIdeal_eq_span_natGenerator (v : HeightOneSpectrum (π“ž β„š)) : v.asIdeal = Ideal.span {((natGenerator v : β„•) : π“ž β„š)} := by have hmax : (Ideal.span {((natGenerator v : β„•) : π“ž β„š)}).IsMaximal := ((Ideal.span_singleton_prime (natCast_natGenerator_ne_zero v)).mpr (prime_natCast_natGenerator v)).isMaximal ((Ideal.span_singleton_eq_bot (Ξ± := π“ž β„š)).not.mpr (natCast_natGenerator_ne_zero v)) exact (hmax.eq_of_le v.isPrime.ne_top ((Ideal.span_singleton_le_iff_mem _).mpr ((natCast_mem_asIdeal_iff v _).mpr dvd_rfl))).symm theorem valuation_natGenerator (v : HeightOneSpectrum (π“ž β„š)) : v.valuation β„š ((natGenerator v : β„•) : β„š) = exp (-1 : β„€) := by rw [show ((natGenerator v : β„•) : β„š) = algebraMap (π“ž β„š) β„š ((natGenerator v : β„•) : π“ž β„š) from (map_natCast (algebraMap (π“ž β„š) β„š) _).symm, valuation_of_algebraMap] exact intValuation_singleton v (natCast_natGenerator_ne_zero v) (asIdeal_eq_span_natGenerator v) theorem valuation_natCast_of_not_dvd (v : HeightOneSpectrum (π“ž β„š)) {n : β„•} (h : Β¬ natGenerator v ∣ n) : v.valuation β„š ((n : β„•) : β„š) = 1 := by rw [show ((n : β„•) : β„š) = algebraMap (π“ž β„š) β„š ((n : β„•) : π“ž β„š) from (map_natCast (algebraMap (π“ž β„š) β„š) _).symm, valuation_of_algebraMap] exact intValuation_eq_one_iff.mpr fun hmem => h ((natCast_mem_asIdeal_iff v n).mp hmem) theorem eq_of_natGenerator_eq {v w : HeightOneSpectrum (π“ž β„š)} (h : natGenerator v = natGenerator w) : v = w := (primesEquiv (R := π“ž β„š)).injective (Subtype.ext h) theorem valuation_natGenerator_of_ne {v w : HeightOneSpectrum (π“ž β„š)} (h : v β‰  w) : w.valuation β„š ((natGenerator v : β„•) : β„š) = 1 := valuation_natCast_of_not_dvd w fun hd => h (eq_of_natGenerator_eq ((Nat.prime_dvd_prime_iff_eq (prime_natGenerator w) (prime_natGenerator v)).mp hd)).symm theorem natGenerator_primesEquiv_symm (p : Nat.Primes) : natGenerator ((primesEquiv (R := π“ž β„š)).symm p) = (p : β„•) := congrArg Subtype.val ((primesEquiv (R := π“ž β„š)).apply_symm_apply p) theorem valued_algebraMap_rat (v : HeightOneSpectrum (π“ž β„š)) (q : β„š) : Valued.v (algebraMap β„š (v.adicCompletion β„š) q) = v.valuation β„š q := by rw [algebraMap_adicCompletion] exact valuedAdicCompletion_eq_valuation' v q theorem algebraMap_adeleRing_snd (q : β„š) (v : HeightOneSpectrum (π“ž β„š)) : (algebraMap β„š π”Έβ„š q).2 v = algebraMap β„š (v.adicCompletion β„š) q := by rw [AdeleRing.algebraMap_snd_apply, algebraMap_adicCompletion] rfl theorem natCast_adicCompletion_ne_zero (v : HeightOneSpectrum (π“ž β„š)) {n : β„•} (hn : n β‰  0) : ((n : β„•) : v.adicCompletion β„š) β‰  0 := by rw [← map_natCast (algebraMap β„š (v.adicCompletion β„š)) n] exact (map_ne_zero (algebraMap β„š (v.adicCompletion β„š))).mpr (Nat.cast_ne_zero.mpr hn) end Primes section Arch def archCoord (x : (π”Έβ„š)Λ£) : ℝ := InfinitePlace.Completion.ringEquivRealOfIsReal Rat.isReal_infinitePlace ((x : π”Έβ„š).1 Rat.infinitePlace) theorem archCoord_mul (x y : (π”Έβ„š)Λ£) : archCoord (x * y) = archCoord x * archCoord y := by unfold archCoord rw [← map_mul] rfl theorem archCoord_one : archCoord 1 = 1 := by unfold archCoord rw [show ((1 : (π”Έβ„š)Λ£) : π”Έβ„š).1 Rat.infinitePlace = 1 from rfl, map_one] theorem archCoord_ne_zero (x : (π”Έβ„š)Λ£) : archCoord x β‰  0 := by intro h have h1 := archCoord_mul x x⁻¹ rw [mul_inv_cancel, archCoord_one, h, zero_mul] at h1 exact one_ne_zero h1 theorem archCoord_principal (q : β„šΛ£) : archCoord (Units.map (algebraMap β„š π”Έβ„š : β„š β†’* π”Έβ„š) q) = ((q : β„š) : ℝ) := eq_ratCast ((InfinitePlace.Completion.ringEquivRealOfIsReal Rat.isReal_infinitePlace : Rat.infinitePlace.Completion ≃+* ℝ).toRingHom.comp ((Pi.evalRingHom (fun w : InfinitePlace β„š => w.Completion) Rat.infinitePlace).comp ((RingHom.fst _ _).comp (algebraMap β„š π”Έβ„š)))) (q : β„š) theorem archCoord_finIncl (y : (π”Έβ„šf)Λ£) : archCoord (Units.map (finIncl (π“ž β„š) β„š) y) = 1 := by unfold archCoord rw [Units.coe_map, finIncl_apply_fst, show (1 : InfiniteAdeleRing β„š) Rat.infinitePlace = 1 from rfl, map_one] end Arch section Order def finPart : (π”Έβ„š)Λ£ β†’* (π”Έβ„šf)Λ£ := Units.map (RingHom.snd (InfiniteAdeleRing β„š) π”Έβ„šf).toMonoidHom theorem finPart_apply (x : (π”Έβ„š)Λ£) (v : HeightOneSpectrum (π“ž β„š)) : ((finPart x : (π”Έβ„šf)Λ£) : π”Έβ„šf) v = (x : π”Έβ„š).2 v := rfl theorem valued_snd_mul (x y : (π”Έβ„š)Λ£) (v : HeightOneSpectrum (π“ž β„š)) : Valued.v ((((x * y : (π”Έβ„š)Λ£)) : π”Έβ„š).2 v) = Valued.v ((x : π”Έβ„š).2 v) * Valued.v ((y : π”Έβ„š).2 v) := by rw [← map_mul] rfl theorem valued_snd_ne_zero (x : (π”Έβ„š)Λ£) (v : HeightOneSpectrum (π“ž β„š)) : Valued.v ((x : π”Έβ„š).2 v) β‰  0 := by rw [ne_eq, map_eq_zero] intro h have h1 : (((x * x⁻¹ : (π”Έβ„š)Λ£)) : π”Έβ„š).2 v = 1 := by rw [mul_inv_cancel] rfl rw [show (((x * x⁻¹ : (π”Έβ„š)Λ£)) : π”Έβ„š).2 v = (x : π”Έβ„š).2 v * (((x⁻¹ : (π”Έβ„š)Λ£)) : π”Έβ„š).2 v from rfl, h, zero_mul] at h1 exact zero_ne_one h1 theorem valued_snd_inv_mul (x : (π”Έβ„š)Λ£) (v : HeightOneSpectrum (π“ž β„š)) : Valued.v ((((x⁻¹ : (π”Έβ„š)Λ£)) : π”Έβ„š).2 v) * Valued.v ((x : π”Έβ„š).2 v) = 1 := by rw [← valued_snd_mul, inv_mul_cancel] show Valued.v ((1 : π”Έβ„šf) v) = 1 rw [show ((1 : π”Έβ„šf)) v = 1 from rfl, map_one] def ordAt (v : HeightOneSpectrum (π“ž β„š)) (x : (π”Έβ„š)Λ£) : β„€ := -log (Valued.v ((x : π”Έβ„š).2 v)) theorem valued_snd_eq (v : HeightOneSpectrum (π“ž β„š)) (x : (π”Έβ„š)Λ£) : Valued.v ((x : π”Έβ„š).2 v) = exp (-ordAt v x) := by rw [ordAt, neg_neg, exp_log (valued_snd_ne_zero x v)] theorem ordAt_mul (v : HeightOneSpectrum (π“ž β„š)) (x y : (π”Έβ„š)Λ£) : ordAt v (x * y) = ordAt v x + ordAt v y := by unfold ordAt rw [valued_snd_mul, log_mul (valued_snd_ne_zero x v) (valued_snd_ne_zero y v), neg_add] theorem ordAt_one (v : HeightOneSpectrum (π“ž β„š)) : ordAt v 1 = 0 := by unfold ordAt rw [show ((1 : (π”Έβ„š)Λ£) : π”Έβ„š).2 v = 1 from rfl, map_one, log_one, neg_zero] theorem ordAt_eq_zero_of_le_one {v : HeightOneSpectrum (π“ž β„š)} {x : (π”Έβ„š)Λ£} (hx : Valued.v ((x : π”Έβ„š).2 v) ≀ 1) (hxi : Valued.v ((((x⁻¹ : (π”Έβ„š)Λ£)) : π”Έβ„š).2 v) ≀ 1) : ordAt v x = 0 := by have hmul := valued_snd_inv_mul x v have h1 : Valued.v ((x : π”Έβ„š).2 v) = 1 := le_antisymm hx (by calc (1 : ℀ᡐ⁰) = Valued.v ((((x⁻¹ : (π”Έβ„š)Λ£)) : π”Έβ„š).2 v) * Valued.v ((x : π”Έβ„š).2 v) := hmul.symm _ ≀ 1 * Valued.v ((x : π”Έβ„š).2 v) := mul_le_mul_left hxi _ _ = Valued.v ((x : π”Έβ„š).2 v) := one_mul _) unfold ordAt rw [h1, log_one, neg_zero] theorem finite_setOf_ordAt_ne_zero (x : (π”Έβ„š)Λ£) : {v : HeightOneSpectrum (π“ž β„š) | ordAt v x β‰  0}.Finite := by have hx : βˆ€αΆ  v in Filter.cofinite, ((x : π”Έβ„š).2 : π”Έβ„šf) v ∈ v.adicCompletionIntegers β„š := ((x : π”Έβ„š).2).2 have hxi : βˆ€αΆ  v in Filter.cofinite, ((((x⁻¹ : (π”Έβ„š)Λ£)) : π”Έβ„š).2 : π”Έβ„šf) v ∈ v.adicCompletionIntegers β„š := ((((x⁻¹ : (π”Έβ„š)Λ£)) : π”Έβ„š).2).2 have hboth := hx.and hxi rw [Filter.eventually_cofinite] at hboth refine hboth.subset ?_ intro v hv simp only [Set.mem_setOf_eq] at hv ⊒ intro hcon exact hv (ordAt_eq_zero_of_le_one ((mem_adicCompletionIntegers (π“ž β„š) β„š v).mp hcon.1) ((mem_adicCompletionIntegers (π“ž β„š) β„š v).mp hcon.2)) end Order section Normalizer def IsNormalizer (x : (π”Έβ„š)Λ£) (r : β„š) : Prop := (βˆ€ v : HeightOneSpectrum (π“ž β„š), Valued.v ((x : π”Έβ„š).2 v) = v.valuation β„š r) ∧ 0 < archCoord x * (r : ℝ) theorem IsNormalizer.ne_zero {x : (π”Έβ„š)Λ£} {r : β„š} (h : IsNormalizer x r) : r β‰  0 := by rintro rfl have := h.2 rw [Rat.cast_zero, mul_zero] at this exact lt_irrefl _ this def archSign (x : (π”Έβ„š)Λ£) : β„š := if 0 < archCoord x then 1 else -1 theorem archCoord_mul_archSign_pos (x : (π”Έβ„š)Λ£) : 0 < archCoord x * (archSign x : ℝ) := by unfold archSign split_ifs with h Β· rw [Rat.cast_one, mul_one] exact h Β· rw [Rat.cast_neg, Rat.cast_one, mul_neg, mul_one] exact neg_pos.mpr (lt_of_le_of_ne (not_lt.mp h) (archCoord_ne_zero x)) theorem valuation_archSign (w : HeightOneSpectrum (π“ž β„š)) (x : (π”Έβ„š)Λ£) : w.valuation β„š (archSign x) = 1 := by unfold archSign split_ifs Β· exact map_one _ Β· rw [Valuation.map_neg, map_one] def ρ (x : (π”Έβ„š)Λ£) : β„š := archSign x * ∏ᢠ v : HeightOneSpectrum (π“ž β„š), ((natGenerator v : β„•) : β„š) ^ ordAt v x theorem mulSupport_subset_toFinset (x : (π”Έβ„š)Λ£) : (Function.mulSupport fun v : HeightOneSpectrum (π“ž β„š) => ((natGenerator v : β„•) : β„š) ^ ordAt v x) βŠ† ((finite_setOf_ordAt_ne_zero x).toFinset : Set (HeightOneSpectrum (π“ž β„š))) := by intro v hv rw [Set.Finite.coe_toFinset, Set.mem_setOf_eq] intro h0 rw [Function.mem_mulSupport, h0, zpow_zero] at hv exact hv rfl theorem finprod_pow_ordAt_pos (x : (π”Έβ„š)Λ£) : (0 : β„š) < ∏ᢠ v : HeightOneSpectrum (π“ž β„š), ((natGenerator v : β„•) : β„š) ^ ordAt v x := finprod_induction (fun r : β„š => 0 < r) one_pos (fun _ _ => mul_pos) fun v => zpow_pos (Nat.cast_pos.mpr (prime_natGenerator v).pos) _ theorem valuation_ρ (w : HeightOneSpectrum (π“ž β„š)) (x : (π”Έβ„š)Λ£) : w.valuation β„š (ρ x) = Valued.v ((x : π”Έβ„š).2 w) := by classical rw [ρ, map_mul, valuation_archSign, one_mul, finprod_eq_prod_of_mulSupport_subset _ (mulSupport_subset_toFinset x), map_prod, valued_snd_eq, Finset.prod_eq_single w] Β· rw [map_zpowβ‚€, valuation_natGenerator, ← exp_zsmul, smul_eq_mul, mul_neg_one] Β· intro v _ hvw rw [map_zpowβ‚€, valuation_natGenerator_of_ne hvw, one_zpow] Β· intro hw have h0 : ordAt w x = 0 := by by_contra h0 exact hw ((Set.Finite.mem_toFinset _).mpr h0) rw [h0, zpow_zero, map_one] theorem ρ_spec (x : (π”Έβ„š)Λ£) : IsNormalizer x (ρ x) := by refine ⟨fun v => (valuation_ρ v x).symm, ?_⟩ rw [ρ, Rat.cast_mul, ← mul_assoc] exact mul_pos (archCoord_mul_archSign_pos x) (by exact_mod_cast finprod_pow_ordAt_pos x) theorem exists_isNormalizer (x : (π”Έβ„š)Λ£) : βˆƒ r : β„š, IsNormalizer x r := ⟨ρ x, ρ_spec x⟩ theorem rat_eq_one_of_valuation_eq_one {q : β„š} (hq : 0 < q) (h : βˆ€ v : HeightOneSpectrum (π“ž β„š), v.valuation β„š q = 1) : q = 1 := by have hq0 : q β‰  0 := hq.ne' obtain ⟨z, hz⟩ := mem_integers_of_valuation_le_one β„š q fun v => (h v).le obtain ⟨z', hz'⟩ := mem_integers_of_valuation_le_one β„š q⁻¹ fun v => by rw [map_invβ‚€, h v, inv_one] have hzz' : z * z' = 1 := IsFractionRing.injective (π“ž β„š) β„š (by rw [map_mul, hz, hz', map_one, mul_inv_cancelβ‚€ hq0]) have hu : IsUnit z := isUnit_iff_exists_inv.mpr ⟨z', hzz'⟩ have hzq : (z : β„š) = q := by rw [RingOfIntegers.coe_eq_algebraMap]; exact hz rcases Rat.RingOfIntegers.isUnit_iff.mp hu with h1 | h1 Β· rw [← hzq]; exact h1 Β· exfalso rw [hzq] at h1 rw [h1] at hq exact absurd hq (by norm_num) theorem IsNormalizer.unique {x : (π”Έβ„š)Λ£} {r r' : β„š} (h : IsNormalizer x r) (h' : IsNormalizer x r') : r = r' := by have hr' := h'.ne_zero have hq : 0 < r / r' := by have h3 : (0 : ℝ) < (archCoord x * r) / (archCoord x * r') := div_pos h.2 h'.2 rw [mul_div_mul_left _ _ (archCoord_ne_zero x)] at h3 exact_mod_cast h3 have hval : βˆ€ v : HeightOneSpectrum (π“ž β„š), v.valuation β„š (r / r') = 1 := fun v => by rw [map_divβ‚€, ← h.1 v, ← h'.1 v, div_self (valued_snd_ne_zero x v)] have := rat_eq_one_of_valuation_eq_one hq hval rwa [div_eq_one_iff_eq hr'] at this theorem ρ_ne_zero (x : (π”Έβ„š)Λ£) : ρ x β‰  0 := (ρ_spec x).ne_zero theorem ρ_eq_of_isNormalizer {x : (π”Έβ„š)Λ£} {r : β„š} (h : IsNormalizer x r) : ρ x = r := (ρ_spec x).unique h theorem ρ_mul (x y : (π”Έβ„š)Λ£) : ρ (x * y) = ρ x * ρ y := by refine ρ_eq_of_isNormalizer ⟨fun v => ?_, ?_⟩ Β· rw [valued_snd_mul, (ρ_spec x).1 v, (ρ_spec y).1 v, map_mul] Β· rw [archCoord_mul, Rat.cast_mul, show archCoord x * archCoord y * (((ρ x : β„š) : ℝ) * ((ρ y : β„š) : ℝ)) = (archCoord x * ((ρ x : β„š) : ℝ)) * (archCoord y * ((ρ y : β„š) : ℝ)) by ring] exact mul_pos (ρ_spec x).2 (ρ_spec y).2 theorem ρ_principal (q : β„šΛ£) : ρ (Units.map (algebraMap β„š π”Έβ„š : β„š β†’* π”Έβ„š) q) = (q : β„š) := by refine ρ_eq_of_isNormalizer ⟨fun v => ?_, ?_⟩ Β· rw [Units.coe_map, MonoidHom.coe_coe, algebraMap_adeleRing_snd, valued_algebraMap_rat] Β· rw [archCoord_principal] exact mul_self_pos.mpr (by exact_mod_cast q.ne_zero) theorem ρ_one : ρ 1 = 1 := by have := ρ_principal 1 rwa [map_one, Units.val_one] at this theorem ρ_finIncl_localUnit (v : HeightOneSpectrum (π“ž β„š)) (t : (v.adicCompletion β„š)Λ£) (ht : Valued.v (t : v.adicCompletion β„š) = exp (-1 : β„€)) : ρ (Units.map (finIncl (π“ž β„š) β„š) (localUnit (π“ž β„š) β„š v t)) = ((natGenerator v : β„•) : β„š) := by refine ρ_eq_of_isNormalizer ⟨fun w => ?_, ?_⟩ Β· rw [Units.coe_map, finIncl_apply_snd] by_cases hw : w = v Β· subst hw rw [localUnit_apply_self, ht, valuation_natGenerator] Β· rw [localUnit_apply_of_ne (π“ž β„š) β„š v t hw, map_one, valuation_natGenerator_of_ne (Ne.symm hw)] Β· rw [archCoord_finIncl, one_mul] exact_mod_cast (prime_natGenerator v).pos theorem ρ_finIncl_localUnit_of_valued_one (v : HeightOneSpectrum (π“ž β„š)) (t : (v.adicCompletion β„š)Λ£) (ht : Valued.v (t : v.adicCompletion β„š) = 1) : ρ (Units.map (finIncl (π“ž β„š) β„š) (localUnit (π“ž β„š) β„š v t)) = 1 := by refine ρ_eq_of_isNormalizer ⟨fun w => ?_, ?_⟩ Β· rw [Units.coe_map, finIncl_apply_snd, map_one] by_cases hw : w = v Β· subst hw rw [localUnit_apply_self, ht] Β· rw [localUnit_apply_of_ne (π“ž β„š) β„š v t hw, map_one] Β· rw [archCoord_finIncl, one_mul, Rat.cast_one] exact one_pos theorem ρ_eq_archSign_of_snd_eq_one {x : (π”Έβ„š)Λ£} (hx : βˆ€ w : HeightOneSpectrum (π“ž β„š), (x : π”Έβ„š).2 w = 1) : ρ x = archSign x := by refine ρ_eq_of_isNormalizer ⟨fun w => ?_, archCoord_mul_archSign_pos x⟩ rw [hx w, map_one, valuation_archSign] end Normalizer section UnitAt def unitAt (v : HeightOneSpectrum (π“ž β„š)) (x : (π”Έβ„š)Λ£) : v.adicCompletion β„š := (x : π”Έβ„š).2 v * (algebraMap β„š (v.adicCompletion β„š) (ρ x))⁻¹ theorem valued_unitAt (v : HeightOneSpectrum (π“ž β„š)) (x : (π”Έβ„š)Λ£) : Valued.v (unitAt v x) = 1 := by unfold unitAt rw [map_mul, map_invβ‚€, valued_algebraMap_rat, ← (ρ_spec x).1 v, mul_inv_cancelβ‚€ (valued_snd_ne_zero x v)] theorem unitAt_mul (v : HeightOneSpectrum (π“ž β„š)) (x y : (π”Έβ„š)Λ£) : unitAt v (x * y) = unitAt v x * unitAt v y := by unfold unitAt rw [ρ_mul, map_mul, mul_inv, show (((x * y : (π”Έβ„š)Λ£)) : π”Έβ„š).2 v = (x : π”Έβ„š).2 v * (y : π”Έβ„š).2 v from rfl] ring theorem unitAt_one (v : HeightOneSpectrum (π“ž β„š)) : unitAt v 1 = 1 := by unfold unitAt rw [ρ_one, map_one, inv_one, mul_one] rfl theorem unitAt_principal (v : HeightOneSpectrum (π“ž β„š)) (q : β„šΛ£) : unitAt v (Units.map (algebraMap β„š π”Έβ„š : β„š β†’* π”Έβ„š) q) = 1 := by unfold unitAt rw [ρ_principal, Units.coe_map, MonoidHom.coe_coe, algebraMap_adeleRing_snd, mul_inv_cancelβ‚€ ((map_ne_zero _).mpr q.ne_zero)] theorem unitAt_finIncl_localUnit_self (v : HeightOneSpectrum (π“ž β„š)) (t : (v.adicCompletion β„š)Λ£) (ht : Valued.v (t : v.adicCompletion β„š) = 1) : unitAt v (Units.map (finIncl (π“ž β„š) β„š) (localUnit (π“ž β„š) β„š v t)) = t := by unfold unitAt rw [ρ_finIncl_localUnit_of_valued_one v t ht, map_one, inv_one, mul_one, Units.coe_map, finIncl_apply_snd, localUnit_apply_self] theorem unitAt_finIncl_localUnit_of_ne (v : HeightOneSpectrum (π“ž β„š)) (t : (v.adicCompletion β„š)Λ£) (ht : Valued.v (t : v.adicCompletion β„š) = 1) {w : HeightOneSpectrum (π“ž β„š)} (hw : w β‰  v) : unitAt w (Units.map (finIncl (π“ž β„š) β„š) (localUnit (π“ž β„š) β„š v t)) = 1 := by unfold unitAt rw [ρ_finIncl_localUnit_of_valued_one v t ht, map_one, inv_one, mul_one, Units.coe_map, finIncl_apply_snd, localUnit_apply_of_ne (π“ž β„š) β„š v t hw] def unitIntAt (v : HeightOneSpectrum (π“ž β„š)) (x : (π”Έβ„š)Λ£) : v.adicCompletionIntegers β„š := ⟨unitAt v x, (mem_adicCompletionIntegers (π“ž β„š) β„š v).mpr (valued_unitAt v x).le⟩ theorem coe_unitIntAt (v : HeightOneSpectrum (π“ž β„š)) (x : (π”Έβ„š)Λ£) : (unitIntAt v x : v.adicCompletion β„š) = unitAt v x := rfl theorem unitIntAt_mul (v : HeightOneSpectrum (π“ž β„š)) (x y : (π”Έβ„š)Λ£) : unitIntAt v (x * y) = unitIntAt v x * unitIntAt v y := Subtype.ext (unitAt_mul v x y) theorem unitIntAt_one (v : HeightOneSpectrum (π“ž β„š)) : unitIntAt v 1 = 1 := Subtype.ext (unitAt_one v) theorem isUnit_unitIntAt (v : HeightOneSpectrum (π“ž β„š)) (x : (π”Έβ„š)Λ£) : IsUnit (unitIntAt v x) := isUnit_iff_exists_inv.mpr ⟨unitIntAt v x⁻¹, by rw [← unitIntAt_mul, mul_inv_cancel, unitIntAt_one]⟩ theorem natCast_mul_unitIntAt_eq_one {v : HeightOneSpectrum (π“ž β„š)} {x : (π”Έβ„š)Λ£} {n : β„•} (h : ((n : β„•) : v.adicCompletion β„š) * unitAt v x = 1) : ((n : β„•) : v.adicCompletionIntegers β„š) * unitIntAt v x = 1 := Subtype.ext (by rw [MulMemClass.coe_mul, SubringClass.coe_natCast, OneMemClass.coe_one]; exact h) end UnitAt end RatIdele end