funlean.
Step 61 / 64

Master’s level

Patching

Compatible pieces must produce one object satisfying all the required relationships.

Start with a concrete example

Two map pieces may each be accurate but disagree on the shared street. To glue them into one map, their overlapping information must agree. Mathematical patching also needs specified compatibility conditions, not only valid separate pieces.

A small check: try the idea

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

Are individually correct map pieces enough if they disagree on their shared street?

Read the answer and reasoning

No; compatibility on overlaps matters too. Put the shared street on top of itself. The pieces must agree there. The proof likewise needs its specified compatibility conditions.

Build the idea in three steps

  1. Collect a system of local pieces. Each piece comes with algebraic conditions.
  2. Also specify agreement between related pieces: individually valid data can be incompatible.
  3. A patching theorem constructs one coherent object under the full assumptions. This construction contributes to lifting, rather than proving modularity by itself.

A small example

A pile of correct quilt squares is not a finished quilt. The edge constraints are part of the input.

Lean definition · original excerpt

FLT · aa2d8b3 · Def_Algebra_PatchingDatum.lean

structure Algebra.PatchingDatum (𝒪 : Type) [CommRing 𝒪] (ℓ r : ℕ) (R : Type) [CommRing R]    [Algebra 𝒪 R] (M : Type) [AddCommGroup M] [Module R M] : Type 1 where   level : ∀ n : ℕ, Algebra.PatchingLevel 𝒪 r R M    (Ideal.span (Set.range fun j : Fin r =>      ((1 + MvPowerSeries.X j) ^ (ℓ ^ n) - 1 : MvPowerSeries (Fin r) 𝒪)))

How to read this Lean

level supplies data at each n. Each PatchingLevel contains the algebraic constraints. This is structured input, not arbitrary glue.

Original source ↗ · L39–44Open the complete saved source

Where this idea is used

13. Pip’s impossible quilt
I’m lost · Help

Mika’s help desk

Patching

One thing at a time

Read the three explanation steps first. The Lean source is there for a closer look afterwards; you do not have to read it first.

In simpler words

Compatible pieces must produce one object satisfying all the required relationships.

Earlier ideas are listed under “Start with these ideas” on this page.

A small clue

A pile of correct quilt squares is not a finished quilt. The edge constraints are part of the input.

Close this panel to return to the exact place you were reading. These are prepared hints for this page.

Start with the first small story →