Merge branch 'DjangoPeeters-main'

Author: kbuzzard

FLT/AutomorphicRepresentation/Example.lean

@@ -340,9 +340,61 @@ noncomputable abbrev zHatsub : AddSubgroup QHat :=
 noncomputable abbrev zsub : AddSubgroup QHat :=
   (Int.castRingHom QHat : ℤ →+ QHat).range
 
-lemma rat_meet_zHat : ratsub ⊓ zHatsub = zsub := sorry
+lemma ZMod.isUnit_natAbs {z : ℤ} {N : ℕ} : IsUnit (z.natAbs : ZMod N) ↔ IsUnit (z : ZMod N) := by
+  cases z.natAbs_eq with
+  | inl h | inr h => rw [h]; simp [-Int.natCast_natAbs]
 
-lemma rat_join_zHat : ratsub ⊔ zHatsub = ⊤ := sorry
+@[simp]
+lemma _root_.Algebra.TensorProduct.one_tmul_intCast {R : Type*} {A : Type*} {B : Type*}
+    [CommRing R] [Ring A] [Algebra R A] [Ring B] [Algebra R B] {z : ℤ} :
+    (1 : A) ⊗ₜ[R] (z : B) = (z : TensorProduct R A B) := by
+  rw [← map_intCast (F := B →ₐ[R] TensorProduct R A B),
+    Algebra.TensorProduct.includeRight_apply]
+
+lemma rat_meet_zHat : ratsub ⊓ zHatsub = zsub := by
+  apply le_antisymm
+  · intro x ⟨⟨l, hl⟩, ⟨r, hr⟩⟩
+    simp only [AddMonoidHom.coe_coe, Algebra.TensorProduct.includeLeft_apply,
+      Algebra.TensorProduct.includeRight_apply] at hl hr
+    rcases lowestTerms x with ⟨⟨N, z, hNz, hx⟩, unique⟩
+    have cop1 : IsCoprime l.den.toPNat' l.num := by
+      simp_rw [IsCoprime, ZHat.intCast_val, ← ZMod.isUnit_natAbs, ZMod.isUnit_iff_coprime,
+        PNat.toPNat'_coe l.den_pos]
+      exact l.reduced
+    have cop2 : IsCoprime 1 r := by
+      simp only [IsCoprime, PNat.val_ofNat]
+      exact isUnit_of_subsingleton _
+    have hcanon : x = (1/(l.den : ℚ)) ⊗ₜ[ℤ] (l.num : ZHat) := by
+      nth_rw 1 [← hl, ← Rat.num_div_den l, ← mul_one ((l.num : ℚ) / l.den), div_mul_comm,
+      mul_comm, ← zsmul_eq_mul, TensorProduct.smul_tmul, zsmul_eq_mul, mul_one]
+    rw [← PNat.toPNat'_coe l.den_pos, hx] at hcanon
+    obtain ⟨rfl, rfl⟩ := unique _ _ _ _ ⟨hNz, cop1, hcanon⟩
+    have : 1 = 1 / (((1 : ℕ+) : ℕ) : ℚ) := by simp
+    nth_rw 1 [← hx, ← hr, this] at hcanon
+    use l.num; rw [hx, (unique _ 1 _ r ⟨hNz, cop2, hcanon.symm⟩).1]
+    simp
+  · exact fun x ⟨k, hk⟩ ↦ by constructor <;> (use k; simp; exact hk)
+
+lemma rat_join_zHat : ratsub ⊔ zHatsub = ⊤ := by
+  rw [eq_top_iff]
+  intro x _
+  rcases x.canonicalForm with ⟨N, z, hNz⟩
+  rcases ZHat.nat_dense N z with ⟨q, r, hz, _⟩
+  have h : z - r = N * q := sub_eq_of_eq_add hz
+  rw [AddSubgroup.mem_sup]
+  use ((r : ℤ) / N : ℚ) ⊗ₜ[ℤ] 1
+  constructor
+  · simp
+  use 1 ⊗ₜ[ℤ] q
+  constructor
+  · simp
+  nth_rw 1 [← mul_one ((r : ℤ) / N : ℚ), div_mul_comm,
+    mul_comm, ← zsmul_eq_mul, TensorProduct.smul_tmul, zsmul_eq_mul, mul_one]
+  have : 1 = 1 / (N : ℚ) * (N : ℤ) := by simp
+  nth_rw 2 [this]
+  rw [mul_comm, ← zsmul_eq_mul, TensorProduct.smul_tmul, zsmul_eq_mul]
+  norm_cast; rw [← h, ← TensorProduct.tmul_add]
+  simp [hNz]
 
 end additive_structure_of_QHat
 

blueprint/src/chapter/ch05automorphicformexample.tex

@@ -451,7 +451,7 @@ \section{Additive structure of \texorpdfstring{$\Qhat$}{Qhat}.}
     \leanok
     The intersection of $\Q$ and $\Zhat$ in $\Qhat$ is $\Z$.
 \end{lemma}
-\begin{proof}
+\begin{proof} \leanok
     Clearly $\Z\subseteq\Q\cap\Zhat$. Now suppose that $x\in\Q\cap\Zhat$.
     Because $x$ is rational we can write it as $\frac{A}{B}\otimes_t1$ for some
     fraction $A/B$ in lowest terms, and hence $x=A/B$ where now we regard $A\in\Zhat$
@@ -468,7 +468,7 @@ \section{Additive structure of \texorpdfstring{$\Qhat$}{Qhat}.}
     More precisely, every element of $\Qhat$ can be written as $q+z$ with $q\in\Q$ and $z\in\Zhat$,
     or more precisely as $q\otimes_t 1+1\otimes_t z$.
 \end{lemma}
-\begin{proof}
+\begin{proof} \leanok
     Write $x\in\Qhat$ as $x=z/N$ in lowest terms. Lift $z_N$ to an integer $t$ and observe
     that $(z-t)_N=0$, hence $z-t=Ny$ for some $y\in\Zhat$. Now $x=t/N+y\in\Q+\Zhat$.
 \end{proof}