Proved QHat.rat_meet_zHat and QHat.rat_join_zHat.

FLT/AutomorphicRepresentation/Example.lean

@@ -321,9 +321,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}

lake-manifest.json

@@ -90,46 +90,6 @@
  "manifestFile": "lake-manifest.json",
  "inputRev": null,
  "inherited": false,
- "configFile": "lakefile.lean"},
- {"url": "https://github.com/acmepjz/md4lean",
- "type": "git",
- "subDir": null,
- "scope": "",
- "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
- "name": "MD4Lean",
- "manifestFile": "lake-manifest.json",
- "inputRev": "main",
- "inherited": true,
- "configFile": "lakefile.lean"},
- {"url": "https://github.com/fgdorais/lean4-unicode-basic",
- "type": "git",
- "subDir": null,
- "scope": "",
- "rev": "6d2e06515f1ed1f74208d5a1da3a9cc26c60a7a0",
- "name": "UnicodeBasic",
- "manifestFile": "lake-manifest.json",
- "inputRev": "main",
- "inherited": true,
- "configFile": "lakefile.lean"},
- {"url": "https://github.com/dupuisf/BibtexQuery",
- "type": "git",
- "subDir": null,
- "scope": "",
- "rev": "85e1e7143dd4cfa2b551826c27867bada60858e8",
- "name": "BibtexQuery",
- "manifestFile": "lake-manifest.json",
- "inputRev": "master",
- "inherited": true,
- "configFile": "lakefile.lean"},
- {"url": "https://github.com/leanprover/doc-gen4",
- "type": "git",
- "subDir": null,
- "scope": "",
- "rev": "ccb4e97ffb7ad0f9b1852e9669d5e2922f984175",
- "name": "«doc-gen4»",
- "manifestFile": "lake-manifest.json",
- "inputRev": "main",
- "inherited": false,
  "configFile": "lakefile.lean"}],
  "name": "FLT",
  "lakeDir": ".lake"}