R = T: matching the two workshops

One surjective map ties the ring built from lifts to the ring built from Hecke operators.

Start with a concrete example

Two shops may use different order books for the same kind of object. A map between the books and a proof that every required order is reached are steps toward comparison. Proving the two rings are isomorphic needs more than naming that map.

A small check: try the idea

Think with the concrete example above. You can try again.

Does naming a map R→T alone prove that the two rings are isomorphic?

Read the answer and reasoning

No; further properties and proofs are needed. An order-transfer rule is only a start. Surjectivity and the further comparison results must be established; an arbitrary map need not be invertible.

Build the idea in three steps

R records deformation data and T records Hecke operators. The notation R = T usually means a specified comparison map is an isomorphism of algebras, not that independently constructed types are literally equal. The excerpt on this page establishes only the surjective-map stage.
The summit theorem supplies the bridge at the level of maps: a surjective algebra map φ : R → T, with additional evidence that the representations carried along by φ match the Hecke representation after the appropriate base change.
Read the signature honestly: it carries pages of type-level hypotheses, because a real theorem must state every environment it lives in. The displayed proof is two moves: obtain the universal map from D.universal, then apply the datum’s own lemma to certify the remaining matches.

A small example

φ is surjective, and the remaining conjuncts certify that both sides carry the same representation. The ring isomorphism R ≅ T is a later, separately stated conclusion assembled on top of this map.

Use in Lean · original excerpt

FLT · aa2d8b3 · S_GaloisRep_DeformationRingData_exists_surjective_algHom_of_heckeGaloisRepDatum.lean

7theorem solution {𝒪 : Type} [CommRing 𝒪] [IsDomain 𝒪] [IsDiscreteValuationRing 𝒪] [IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪] {ρbar : ResidualGaloisRep (IsLocalRing.ResidueField 𝒪)} {𝒟 : ∀ ⦃A : Type⦄ [CommRing A] [IsLocalRing A] [Algebra 𝒪 A], GaloisRepAdic A → Prop} (D : GaloisRep.DeformationRingData 𝒪 ρbar 𝒟) {N : ℕ} [NeZero N] {S : Set ℕ} {θ : CuspForm.heckeAlgebra N 2 S →+* IsLocalRing.ResidueField 𝒪} {T : Type} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsAdicComplete (IsLocalRing.maximalIdeal T) T] [Algebra 𝒪 T] [IsLocalHom (algebraMap 𝒪 T)] [Module.Finite 𝒪 T] [Module.Free 𝒪 T] (H : CuspForm.HeckeGaloisRepDatum N S 𝒪 θ T) (hS : ∀ q : ℕ, q.Prime → q ∣ N → q ∈ S) (h𝒟 : 𝒟 H.ρ) (hres : H.ρ.residual.IsEquiv (ρbar.baseChangeAlong (IsLocalRing.ResidueField.map (algebraMap 𝒪 T)))) : ∃ φ : D.R →ₐ[𝒪] T, Function.Surjective φ ∧ ∃ hφ : IsLocalHom (φ : D.R →+* T), (D.ρ.baseChangeAlong (φ : D.R →+* T) hφ).IsEquiv H.ρ := by8  obtain ⟨φ, ⟨hφ, he⟩, -⟩ := D.universal T H.residue_surjective H.ρ h𝒟 hres9  exact ⟨φ, H.surjective_of_isEquiv_baseChangeAlong hS D.ρ φ hφ he, hφ, he⟩

How to read this Lean

D.universal is the same universality field displayed on the deformation-ring page; here it instantiates the map for the concrete datum H. The second line delegates the representation check to a lemma attached to the datum itself. Only three pages of type parameters precede the two-line argument.

Original source ↗ · L7–9 Open the complete saved source

Where this idea is used

12. The workshops agree 13. Pip’s impossible quilt

R = T: matching the two workshops

Start with a concrete example

A small check: try the idea

Build the idea in three steps

A small example

Use in Lean · original excerpt

How to read this Lean

Where this idea is used

Mika’s help desk

One thing at a time

In simpler words

A small clue