Eichler-Shimura material from FLT

LeanPool/FLTEichlerShimura.lean

@@ -0,0 +1,114 @@
+/-
+Copyright (c) 2026 Lean Pool contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lean Pool contributors
+-/
+
+module
+
+public import LeanPool.FLTEichlerShimura.Theorems.Thm_HeckeEis_exists_eichlerShimura_heckeEquivariant
+public import LeanPool.FLTEichlerShimura.Theorems.Thm_ModularCurve_explicitFunctionFieldModels
+public import LeanPool.FLTEichlerShimura.Theorems.Thm_ModularCurve_twelve_mul_genusFF_laurentBaseChange_gamma1_add_six_mul_natCard_doubleCoset_eq_index_add_twelve_of_isAlgClosed
+public import LeanPool.FLTEichlerShimura.Theorems.Thm_WeierstrassCurve_isogenyEnd_eq_zsmul_of_transcendental_j
+public import LeanPool.FLTEichlerShimura.Theorems.Thm_WeierstrassCurve_tateModuleRep_charpoly_frobenius
+
+/-!
+# FLT Eichler-Shimura
+
+Source: url:https://github.com/loefflerd/KN-scratch
+Authors: David Loeffler
+Status: verified
+Main declarations: `HeckeEis.exists_eichlerShimura_heckeEquivariant`
+Tags: number-theory, modular-forms, elliptic-curves, galois-representations
+MSC: 11F11
+-/
+
+/-!
+## Upstream attribution
+
+This project adapts material from David Loeffler’s loefflerd/KN-scratch fork and the original
+anthropics/fermats-last-theorem release at commit aa2d8b34692b16c70f699536de0d8e75b9a3e9ef.
+
+Fermat's Last Theorem in Lean 4
+Copyright 2026 Anthropic, PBC
+
+The original release is made available under the Apache License, Version 2.0. Its NOTICE and
+ATTRIBUTION.md identify material adapted from the Imperial College London FLT project and Mathlib.
+The applicable per-file notices below are reproduced from that frozen ATTRIBUTION.md; they
+supplement the notices already retained in the individual imported modules.
+
+Frozen source notices:
+https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/NOTICE
+https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/ATTRIBUTION.md
+
+Path mapping: Definitions/Def_*.lean keeps the same suffix under
+LeanPool/FLTEichlerShimura/Definitions/. An original P2M/Sol/S_*.lean file is imported under
+LeanPool/FLTEichlerShimura/Theorems/Thm_*.lean with the same suffix.
+
+### Applicable FLT and Mathlib per-file notices
+
+- `Definitions/Def_DedekindDomain_AdicValuation_InlineSpecific.lean`
+  `FLT/DedekindDomain/AdicValuation.lean` — © 2025 Matthew Jasper; authors: Matthew Jasper
+  `FLT/Mathlib/RingTheory/Valuation/ValuationSubring.lean` — © 2025 Ruben Van de Velde; authors:
+  Ruben Van de Velde, Kevin Buzzard, Salvatore Mercuri
+  `FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean` — © 2025 Kevin Buzzard; authors:
+  Kevin Buzzard, Salvatore Mercuri
+
+- `P2M/Sol/S_AlgebraicCurve_residueTheoremK_of_isAlgClosed.lean`
+  `FLT/Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean` — © 2025 Salvatore Mercuri; authors:
+  Salvatore Mercuri, Kevin Buzzard
+
+- `P2M/Sol/S_AlgebraicCurve_tateAgreement.lean`
+  `FLT/Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean` — © 2025 Salvatore Mercuri; authors:
+  Salvatore Mercuri, Kevin Buzzard
+
+- `P2M/Sol/S_AlgebraicCurve_tateChainRule.lean`
+  `FLT/Mathlib/RingTheory/Valuation/ValuationSubring.lean` — © 2025 Ruben Van de Velde; authors:
+  Ruben Van de Velde, Kevin Buzzard, Salvatore Mercuri
+  `FLT/Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean` — © 2025 Salvatore Mercuri; authors:
+  Salvatore Mercuri, Kevin Buzzard
+
+- `P2M/Sol/S_AlgebraicCurve_tateCommFinite.lean`
+  `FLT/Mathlib/RingTheory/Valuation/ValuationSubring.lean` — © 2025 Ruben Van de Velde; authors:
+  Ruben Van de Velde, Kevin Buzzard, Salvatore Mercuri
+  `FLT/Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean` — © 2025 Salvatore Mercuri; authors:
+  Salvatore Mercuri, Kevin Buzzard
+
+- `P2M/Sol/S_AlgebraicCurve_tateTraceCompat_of_isSeparable.lean`
+  `FLT/Mathlib/RingTheory/Valuation/ValuationSubring.lean` — © 2025 Ruben Van de Velde; authors:
+  Ruben Van de Velde, Kevin Buzzard, Salvatore Mercuri
+  `FLT/Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean` — © 2025 Salvatore Mercuri; authors:
+  Salvatore Mercuri, Kevin Buzzard
+
+- `P2M/Sol/S_WeierstrassCurve_exists_intermediateField_countable_map_eq_and_finrankAlong_eq.lean`
+  `FLT/Mathlib/LinearAlgebra/Countable.lean` — © 2025 Kevin Buzzard; authors: Kevin Buzzard
+
+- `Definitions/Def_FLTPrelim_FreyPackage.lean`
+  `FLT/Basic/FreyPackage.lean` — authors recorded in our intermediate port: Kevin Buzzard, Ruben
+  Van de Velde, Pietro Monticone (path as recorded in our port)
+
+- `Definitions/Def_FLTPrelim_GaloisRep.lean`
+  `FLT/EllipticCurve/Torsion.lean` (commit 7a87d3b25db1) — © 2024 Kevin Buzzard; authors: Kevin
+  Buzzard (path as recorded in our port; the notice retained inside our file is our May port's
+  generic one, the upstream notice is reproduced here)
+
+- `P2M/Sol/S_EisensteinSeries_exists_modularForm_coe_eq_eisensteinG.lean`
+  `Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean` — Copyright (c)
+  2024 Chris Birkbeck; Authors: Chris Birkbeck
+  Material identified by upstream: the proof of
+  `EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF` with its auxiliary norm bound, adapted
+  to this repository's `eisensteinG` (≈15 lines)
+
+- `P2M/Sol/S_EisensteinSeries_qExpansion_eisensteinG_coeff.lean`
+  `Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean` — Copyright (c)
+  2024 Chris Birkbeck; Authors: Chris Birkbeck
+  Material identified by upstream: the same proof of
+  `EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF`, adapted (≈15 lines)
+
+The frozen upstream table records approximate extents and acknowledges incomplete detection of
+small passages. Its §2 paths and author lists are recorded intermediate-port notes, except that
+the FLT/EllipticCurve/Torsion.lean notice was checked at commit
+7a87d3b25db19d008cd45b29edd2b92803e785b1. The table records the main FLT source snapshot as
+2026-05-21 without a commit hash. This attribution preserves those limits; it is not an
+independent completeness certificate for the historical provenance search.
+-/

LeanPool/FLTEichlerShimura/Definitions/Def_AdicCompletionLocalRing.lean

@@ -0,0 +1,280 @@
+/-
+Copyright (c) 2026 Lean Pool contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lean Pool contributors
+-/
+
+/-
+Based on Prove2Me node AdicCompletionLocalRing
+(5df31c27-9646-52af-886e-7d5db1e0c5e5) by Claude (2026-09-05).
+
+Licensed under Apache License 2.0
+(https://www.apache.org/licenses/LICENSE-2.0).
+-/
+
+module
+
+public import Mathlib.RingTheory.AdicCompletion.Algebra
+public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs
+
+import Mathlib.RingTheory.AdicCompletion.LocalRing
+
+/-!
+# Adic completion of a Noetherian local ring
+
+Definition: `AdicCompletionLocalRing` (`5df31c27-9646-52af-886e-7d5db1e0c5e5`), by Claude,
+2026-09-05.
+
+Throughout, $A$ is a commutative ring and the objects are Mathlib's $I$-adic completion $\widehat{A}
+=$ `AdicCompletion I A` together with its level-$n$ evaluation maps `eval I A n` (linear) and `evalₐ
+I n` (as a ring/algebra map onto $A/I^n$).
+
+The first group of results identifies the kernels. `evalₐ_algebraMap` records that the composite of
+the structure map $A \to \widehat{A}$ with `evalₐ I n` is reduction modulo $I^n$;
+`mem_ker_evalₐ_iff` identifies the ring-theoretic kernel of `evalₐ I n` with the module-theoretic
+kernel of `eval I A n`; and, for $I$ finitely generated, `ker_evalₐ_eq_map_pow` states that this
+kernel is the ideal of $\widehat{A}$ generated by the image of $I^n$. Consequently
+`exists_eq_algebraMap_add` writes any $x \in \widehat{A}$ as $a + y$ with $a \in A$ and $y$ in the
+extension of $I^n$. For $I$ finitely generated, `isUnit_one_add_of_mem_map` shows $1+x$ is a unit
+when $x$ lies in the extension of $I$ (the extended ideal lies in the Jacobson radical,
+$\widehat{A}$ being adically complete), and `isUnit_add_of_mem_map` extends this to $u+x$ for $u$ a
+unit.
+
+In the local section $A$ is local with maximal ideal $\mathfrak m$, and then Noetherian.
+`isUnit_of_isUnit_algebraMap` descends unitness along $A \to \widehat{A}$; `maximalIdeal_fg` records
+that $\mathfrak m$ is finitely generated; an instance makes $\widehat{A}$ a local ring.
+`maximalIdeal_pow_eq_ker_evalₐ` states that the $n$-th power of the maximal ideal of $\widehat{A}$
+is the kernel of `evalₐ (maximalIdeal A) n`, with the cases $n=1$ and the membership criterion $x
+\in \mathfrak m_{\widehat A} \iff$ `evalₐ … 1 x = 0` spelled out separately. For a base ring $k$
+with $A$ a $k$-algebra, `quotientMaximalIdealPowAlgHom` is the induced $k$-algebra map
+$\widehat{A}/\mathfrak m_{\widehat A}^n \to A/\mathfrak m^n$; it is bijective, and
+`quotientMaximalIdealPowAlgEquiv` is the resulting $k$-algebra isomorphism, which sends the class of
+the image of $a \in A$ to the class of $a$.
+
+The transport section fixes a $k$-algebra isomorphism $\Phi : \widehat{A} \xrightarrow{\sim} B$ with
+$B$ a local ring. It records that $\Phi$ preserves unitness, that the maximal ideal of $B$ is the
+contraction-free image (and contraction) of $\mathfrak m_{\widehat A}$, that $\mathfrak m_B^n$ is
+the ideal generated by the image of $\mathfrak m^n$ under $A \to \widehat{A} \xrightarrow{\Phi} B$,
+that $\Phi$ carries the image of $\mathfrak m$ into $\mathfrak m_B$, and finally gives a $k$-algebra
+isomorphism `quotientMaximalIdealPowAlgEquivOfAlgEquiv` $: B/\mathfrak m_B^n \simeq A/\mathfrak m^n$
+sending the class of $\Phi(a)$ to the class of $a$.
+
+**Relation to Mathlib.** All of this is built on Mathlib's `AdicCompletion`, its evaluation maps
+`eval` and `evalₐ`, and Mathlib's local-ring results for adic completions (`isLocalRing_of_fg`,
+`maximalIdeal_eq_map`, `IsAdicComplete.le_jacobson_bot`); what is added here are the level-$n$
+kernel identifications, the unit criteria for $1+x$ and $u+x$, the $k$-algebra isomorphisms
+$\widehat{A}/\mathfrak m_{\widehat A}^n \simeq A/\mathfrak m^n$, and their transport along an
+algebra isomorphism of $\widehat A$ with another local algebra.
+
+**Where it is used.** These identifications are the basic bookkeeping for working with complete
+Noetherian local coefficient and deformation rings: they let one compute in $\widehat{A}$ modulo
+powers of its maximal ideal by computing in $A/\mathfrak m^n$, and to move such computations across
+an abstract presentation $\widehat{A} \simeq B$ of the completion.
+
+<!-- Generated by add_prove2me_provenance.py -->
+-/
+
+@[expose] public section publicSection
+
+open IsLocalRing
+
+namespace AdicCompletion
+
+variable {A : Type*} [CommRing A]
+
+section Kernel
+
+variable (I : Ideal A)
+
+theorem evalₐ_algebraMap (n : ℕ) (a : A) :
+    evalₐ I n (algebraMap A (AdicCompletion I A) a) = Ideal.Quotient.mk _ a := by
+  rw [algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply, evalₐ_of]
+
+theorem mem_ker_evalₐ_iff (n : ℕ) (x : AdicCompletion I A) :
+    x ∈ RingHom.ker (evalₐ I n) ↔ x ∈ LinearMap.ker (eval I A n) := by
+  have h : (I ^ n • ⊤ : Ideal A) = I ^ n := by rw [smul_eq_mul, Ideal.mul_top]
+  rw [RingHom.mem_ker, LinearMap.mem_ker]
+  constructor
+  · intro hx; rw [← factor_evalₐ_eq_eval I x h.ge, hx]; exact RingHom.map_zero _
+  · intro hx; rw [← factor_eval_eq_evalₐ I x h.le, hx]; exact LinearMap.map_zero _
+
+theorem ker_evalₐ_eq_map_pow (hI : I.FG) (n : ℕ) :
+    RingHom.ker (evalₐ I n) = (I ^ n).map (algebraMap A (AdicCompletion I A)) := by
+  ext x
+  rw [mem_ker_evalₐ_iff, ← pow_smul_top_eq_ker_eval hI, Ideal.smul_top_eq_map,
+    Submodule.restrictScalars_mem]
+
+theorem exists_eq_algebraMap_add (hI : I.FG) (n : ℕ) (x : AdicCompletion I A) :
+    ∃ a : A, ∃ y ∈ (I ^ n).map (algebraMap A (AdicCompletion I A)),
+      x = algebraMap A (AdicCompletion I A) a + y := by
+  obtain ⟨a, ha⟩ := Ideal.Quotient.mk_surjective (evalₐ I n x)
+  refine ⟨a, x - algebraMap A _ a, ?_, by ring⟩
+  rw [← ker_evalₐ_eq_map_pow I hI, RingHom.mem_ker, map_sub, evalₐ_algebraMap, ha, sub_self]
+
+theorem isUnit_one_add_of_mem_map (hI : I.FG) {x : AdicCompletion I A}
+    (hx : x ∈ I.map (algebraMap A (AdicCompletion I A))) : IsUnit (1 + x) := by
+  have : IsAdicComplete (I.map (algebraMap A (AdicCompletion I A))) (AdicCompletion I A) :=
+    (IsAdicComplete.map_algebraMap_iff I (AdicCompletion I A)).mpr (isAdicComplete hI)
+  have h := Ideal.mem_jacobson_bot.mp (IsAdicComplete.le_jacobson_bot _ hx) 1
+  rwa [mul_one, add_comm] at h
+
+theorem isUnit_add_of_mem_map (hI : I.FG) {u x : AdicCompletion I A} (hu : IsUnit u)
+    (hx : x ∈ I.map (algebraMap A (AdicCompletion I A))) : IsUnit (u + x) := by
+  have e : u + x = u * (1 + ↑hu.unit⁻¹ * x) := by
+    rw [mul_add, mul_one, ← mul_assoc, IsUnit.mul_val_inv, one_mul]
+  rw [e]
+  exact hu.mul (isUnit_one_add_of_mem_map I hI (Ideal.mul_mem_left _ _ hx))
+
+end Kernel
+
+section Local
+
+variable [IsLocalRing A]
+
+theorem isUnit_of_isUnit_algebraMap {a : A}
+    (h : IsUnit (algebraMap A (AdicCompletion (maximalIdeal A) A) a)) : IsUnit a := by
+  by_contra ha
+  have hmem : a ∈ maximalIdeal A ^ 1 := by
+    rw [pow_one]; exact (mem_maximalIdeal a).mpr ha
+  have h1 := h.map (evalₐ (maximalIdeal A) 1)
+  rw [evalₐ_algebraMap, Ideal.Quotient.eq_zero_iff_mem.mpr hmem, isUnit_zero_iff] at h1
+  exact (maximalIdeal.isMaximal A).ne_top
+    ((pow_one (maximalIdeal A)).symm.trans (Ideal.Quotient.zero_eq_one_iff.mp h1))
+
+theorem isUnit_one_add_of_mem_map_maximalIdeal (h𝔪 : (maximalIdeal A).FG)
+    {x : AdicCompletion (maximalIdeal A) A}
+    (hx : x ∈ (maximalIdeal A).map (algebraMap A (AdicCompletion (maximalIdeal A) A))) :
+    IsUnit (1 + x) :=
+  isUnit_one_add_of_mem_map _ h𝔪 hx
+
+variable [IsNoetherianRing A]
+
+theorem maximalIdeal_fg : (maximalIdeal A).FG := IsNoetherian.noetherian _
+
+instance instIsLocalRingMaximalIdeal : IsLocalRing (AdicCompletion (maximalIdeal A) A) :=
+  isLocalRing_of_fg maximalIdeal_fg
+
+theorem maximalIdeal_pow_eq_ker_evalₐ (n : ℕ) :
+    maximalIdeal (AdicCompletion (maximalIdeal A) A) ^ n = RingHom.ker (evalₐ (maximalIdeal A) n) :=
+      by
+  rw [maximalIdeal_eq_map, ← Ideal.map_pow, ker_evalₐ_eq_map_pow _ maximalIdeal_fg]
+
+theorem maximalIdeal_eq_ker_evalₐ_one :
+    maximalIdeal (AdicCompletion (maximalIdeal A) A) = RingHom.ker (evalₐ (maximalIdeal A) 1) := by
+  rw [← maximalIdeal_pow_eq_ker_evalₐ, pow_one]
+
+theorem mem_maximalIdeal_iff (x : AdicCompletion (maximalIdeal A) A) :
+    x ∈ maximalIdeal (AdicCompletion (maximalIdeal A) A) ↔ evalₐ (maximalIdeal A) 1 x = 0 := by
+  rw [maximalIdeal_eq_ker_evalₐ_one, RingHom.mem_ker]
+
+section Scalars
+
+variable (k : Type*) [CommRing k] [Algebra k A]
+
+/-- Evaluation from the completion modulo a power of its maximal ideal to the original quotient. -/
+noncomputable def quotientMaximalIdealPowAlgHom (n : ℕ) :
+    (AdicCompletion (maximalIdeal A) A ⧸ maximalIdeal (AdicCompletion (maximalIdeal A) A) ^ n)
+      →ₐ[k] A ⧸ maximalIdeal A ^ n :=
+  Ideal.Quotient.liftₐ _ ((evalₐ (maximalIdeal A) n).restrictScalars k) fun x hx => by
+    rwa [maximalIdeal_pow_eq_ker_evalₐ, RingHom.mem_ker] at hx
+
+theorem quotientMaximalIdealPowAlgHom_mk (n : ℕ) (x : AdicCompletion (maximalIdeal A) A) :
+    quotientMaximalIdealPowAlgHom k n (Ideal.Quotient.mk _ x) = evalₐ (maximalIdeal A) n x :=
+  rfl
+
+theorem quotientMaximalIdealPowAlgHom_bijective (n : ℕ) :
+    Function.Bijective (quotientMaximalIdealPowAlgHom (A := A) k n) := by
+  constructor
+  · intro x y hxy
+    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
+    obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y
+    rw [quotientMaximalIdealPowAlgHom_mk, quotientMaximalIdealPowAlgHom_mk] at hxy
+    refine Ideal.Quotient.eq.mpr ?_
+    rw [maximalIdeal_pow_eq_ker_evalₐ, RingHom.mem_ker, map_sub, hxy, sub_self]
+  · intro z
+    obtain ⟨x, rfl⟩ := surjective_evalₐ (maximalIdeal A) n z
+    exact ⟨Ideal.Quotient.mk _ x, rfl⟩
+
+/-- The algebra equivalence between the completion's maximal-ideal-power quotient and the
+original quotient. -/
+noncomputable def quotientMaximalIdealPowAlgEquiv (n : ℕ) :
+    (AdicCompletion (maximalIdeal A) A ⧸ maximalIdeal (AdicCompletion (maximalIdeal A) A) ^ n)
+      ≃ₐ[k] A ⧸ maximalIdeal A ^ n :=
+  AlgEquiv.ofBijective _ (quotientMaximalIdealPowAlgHom_bijective k n)
+
+theorem quotientMaximalIdealPowAlgEquiv_mk (n : ℕ) (x : AdicCompletion (maximalIdeal A) A) :
+    quotientMaximalIdealPowAlgEquiv k n (Ideal.Quotient.mk _ x) = evalₐ (maximalIdeal A) n x :=
+  rfl
+
+theorem quotientMaximalIdealPowAlgEquiv_mk_algebraMap (n : ℕ) (a : A) :
+    quotientMaximalIdealPowAlgEquiv k n (Ideal.Quotient.mk _ (algebraMap A _ a))
+      = Ideal.Quotient.mk _ a := by
+  rw [quotientMaximalIdealPowAlgEquiv_mk, evalₐ_algebraMap]
+
+end Scalars
+
+end Local
+
+section Transport
+
+variable [IsLocalRing A] [IsNoetherianRing A]
+variable {k : Type*} [CommRing k] [Algebra k A] {B : Type*} [CommRing B] [IsLocalRing B]
+    [Algebra k B]
+variable (Φ : AdicCompletion (maximalIdeal A) A ≃ₐ[k] B)
+
+omit [IsNoetherianRing A] [IsLocalRing B] in
+theorem isUnit_algEquiv_iff (x : AdicCompletion (maximalIdeal A) A) : IsUnit (Φ x) ↔ IsUnit x :=
+  ⟨fun h => by simpa using h.map Φ.symm, fun h => h.map Φ⟩
+
+theorem comap_maximalIdeal_algEquiv :
+    (maximalIdeal B).comap (Φ : AdicCompletion (maximalIdeal A) A →+* B)
+      = maximalIdeal (AdicCompletion (maximalIdeal A) A) := by
+  ext x
+  change Φ x ∈ maximalIdeal B ↔ x ∈ maximalIdeal _
+  rw [mem_maximalIdeal, mem_maximalIdeal, mem_nonunits_iff, mem_nonunits_iff, isUnit_algEquiv_iff]
+
+theorem map_maximalIdeal_algEquiv :
+    (maximalIdeal (AdicCompletion (maximalIdeal A) A)).map
+        (Φ : AdicCompletion (maximalIdeal A) A →+* B) = maximalIdeal B := by
+  rw [← comap_maximalIdeal_algEquiv Φ]
+  exact Ideal.map_comap_of_surjective _ Φ.surjective _
+
+theorem maximalIdeal_eq_map_algEquiv :
+    maximalIdeal B = (maximalIdeal A).map
+      ((Φ : AdicCompletion (maximalIdeal A) A →+* B).comp
+        (algebraMap A (AdicCompletion (maximalIdeal A) A))) := by
+  rw [← Ideal.map_map, ← maximalIdeal_eq_map, map_maximalIdeal_algEquiv]
+
+theorem maximalIdeal_pow_eq_map_algEquiv (n : ℕ) :
+    maximalIdeal B ^ n = (maximalIdeal A ^ n).map
+      ((Φ : AdicCompletion (maximalIdeal A) A →+* B).comp
+        (algebraMap A (AdicCompletion (maximalIdeal A) A))) := by
+  rw [Ideal.map_pow, ← maximalIdeal_eq_map_algEquiv]
+
+theorem algEquiv_algebraMap_mem_maximalIdeal {a : A} (ha : a ∈ maximalIdeal A) :
+    Φ (algebraMap A _ a) ∈ maximalIdeal B := by
+  rw [maximalIdeal_eq_map_algEquiv Φ]
+  exact Ideal.mem_map_of_mem _ ha
+
+/-- The maximal-ideal-power quotient equivalence transported along a chosen completion
+equivalence. -/
+noncomputable def quotientMaximalIdealPowAlgEquivOfAlgEquiv (n : ℕ) :
+    (B ⧸ maximalIdeal B ^ n) ≃ₐ[k] A ⧸ maximalIdeal A ^ n :=
+  (Ideal.quotientEquivAlg (maximalIdeal (AdicCompletion (maximalIdeal A) A) ^ n) (maximalIdeal B ^
+    n)
+    Φ (by rw [Ideal.map_pow, map_maximalIdeal_algEquiv])).symm.trans
+    (quotientMaximalIdealPowAlgEquiv k n)
+
+theorem quotientMaximalIdealPowAlgEquivOfAlgEquiv_mk (n : ℕ) (a : A) :
+    quotientMaximalIdealPowAlgEquivOfAlgEquiv Φ n (Ideal.Quotient.mk _ (Φ (algebraMap A _ a)))
+      = Ideal.Quotient.mk _ a := by
+  rw [quotientMaximalIdealPowAlgEquivOfAlgEquiv, AlgEquiv.trans_apply,
+    ← Ideal.quotientEquivAlg_mk (I := maximalIdeal (AdicCompletion (maximalIdeal A) A) ^ n)
+      (J := maximalIdeal B ^ n) (f := Φ) (hIJ := by rw [Ideal.map_pow, map_maximalIdeal_algEquiv]),
+    AlgEquiv.symm_apply_apply, quotientMaximalIdealPowAlgEquiv_mk_algebraMap]
+
+end Transport
+
+end AdicCompletion
+
+end publicSection