From 0bffc113d2db1e0718d5a0192d00d0b8bec3207c Mon Sep 17 00:00:00 2001 From: maddycrim <58754954+maddycrim@users.noreply.github.com> Date: Sun, 8 Dec 2024 11:13:16 -0500 Subject: [PATCH] Task 232 (#270) * completed task, planning to simplify code * get rid of two rfls and a simp only * get rid of rest of rfl * change funext to refine to delete line * Update FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean Co-authored-by: Kevin Buzzard * Update FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean Co-authored-by: Kevin Buzzard * Update FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean Co-authored-by: Kevin Buzzard * Update FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean Co-authored-by: Kevin Buzzard * make changes --------- Co-authored-by: Kevin Buzzard --- .../FiniteAdeleRing/BaseChange.lean | 25 +++++++++++++++---- 1 file changed, 20 insertions(+), 5 deletions(-) diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean index 6ecd3312..248b1fb1 100644 --- a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean +++ b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean @@ -390,11 +390,26 @@ variable [Algebra K (ProdAdicCompletions B L)] noncomputable def ProdAdicCompletions.baseChange : ProdAdicCompletions A K →ₐ[K] ProdAdicCompletions B L where toFun kv w := (adicCompletionComapAlgHom A K L B _ w rfl (kv (comap A w))) - map_one' := sorry -- #232 is this and the next few sorries. There is probably a cleverer way to do this. - map_mul' := sorry - map_zero' := sorry - map_add' := sorry - commutes' := sorry + map_one' := by + dsimp only + exact funext fun w => by rw [Pi.one_apply, Pi.one_apply, map_one] + map_mul' x y := by + dsimp only + exact funext fun w => by rw [Pi.mul_apply, Pi.mul_apply, map_mul] + map_zero' := by + dsimp only + exact funext fun w => by rw [Pi.zero_apply, Pi.zero_apply, map_zero] + map_add' x y := by + dsimp only + funext w + letI : Module K (adicCompletion L w) := Algebra.toModule + rw [Pi.add_apply, Pi.add_apply, map_add] + commutes' r := by + funext w + rw [IsScalarTower.algebraMap_apply K L (ProdAdicCompletions B L)] + dsimp only [algebraMap_apply'] + exact adicCompletionComapAlgHom_coe A K L B _ w _ r + -- Note that this is only true because L/K is finite; in general tensor product doesn't -- commute with infinite products, but it does here.