From 9e3c0e8fc9767fa090b2b1aecacb065d511188aa Mon Sep 17 00:00:00 2001 From: WilliamCoram Date: Wed, 11 Dec 2024 20:21:21 +0000 Subject: [PATCH] Task #241 (#282) * Attempt 1 * Update FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean Co-authored-by: Kevin Buzzard --------- Co-authored-by: Kevin Buzzard --- .../FiniteAdeleRing/BaseChange.lean | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean index 4ebba11d..81655f9f 100644 --- a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean +++ b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean @@ -436,12 +436,17 @@ theorem ProdAdicCompletions.baseChangeEquiv_isFiniteAdele_iff ProdAdicCompletions.IsFiniteAdele (ProdAdicCompletions.baseChangeEquiv A K L B (1 ⊗ₜ x)) := sorry -- #240 --- Easy consequence of the previous result -theorem ProdAdicCompletions.baseChangeEquiv_isFiniteAdele_iff' - (x : ProdAdicCompletions A K) : - ProdAdicCompletions.IsFiniteAdele x ↔ - ∀ (l : L), ProdAdicCompletions.IsFiniteAdele - (ProdAdicCompletions.baseChangeEquiv A K L B (l ⊗ₜ x)) := sorry -- #241 +theorem ProdAdicCompletions.baseChangeEquiv_isFiniteAdele_iff' (x : ProdAdicCompletions A K) : + ProdAdicCompletions.IsFiniteAdele x ↔ ∀ (l : L), ProdAdicCompletions.IsFiniteAdele + (ProdAdicCompletions.baseChangeEquiv A K L B (l ⊗ₜ x)) := by + constructor + · simp_rw [ProdAdicCompletions.baseChangeEquiv_isFiniteAdele_iff A K L B, baseChangeEquiv, + AlgEquiv.coe_ofBijective, Algebra.TensorProduct.lift_tmul, map_one, one_mul] + intro h l + exact ProdAdicCompletions.IsFiniteAdele.mul (ProdAdicCompletions.IsFiniteAdele.algebraMap' l) h + · intro h + rw [ProdAdicCompletions.baseChangeEquiv_isFiniteAdele_iff A K L B] + exact h 1 -- Make ∏_w L_w into a K-algebra in a way compatible with the L-algebra structure variable [Algebra K (FiniteAdeleRing B L)]