Taylor–Wiles patching

StructureLevel of a Taylor–Wiles patching datum#✓fully proved

One level of a Taylor–Wiles patching datum: a finite module N over the power series ring 𝒪⟦X₁, …, Xᵣ⟧, with a surjective algebra map ψ to R killing the φ-images of the variables, a surjective ψ-semilinear map π : N → M whose kernel is the span of the φ (Xᵢ), and a finite family b spanning N with relations exactly J.

Algebra.PatchingLevel · 19 lines

structure Algebra.PatchingLevel (𝒪 : Type) [CommRing 𝒪] (r : ℕ) (R : Type)
    [CommRing R] [Algebra 𝒪 R] (M : Type) [AddCommGroup M] [Module R M]
    (J : Ideal (MvPowerSeries (Fin r) 𝒪)) : Type 1 where
  N : Type
  [instAddCommGroup : AddCommGroup N]
  [instModule : Module (MvPowerSeries (Fin r) 𝒪) N]
  φ : MvPowerSeries (Fin r) 𝒪 →ₐ[𝒪] MvPowerSeries (Fin r) 𝒪
  ψ : MvPowerSeries (Fin r) 𝒪 →ₐ[𝒪] R
  ψ_surjective : Function.Surjective ψ
  ψ_φ_X : ∀ i : Fin r, ψ (φ (MvPowerSeries.X i)) = 0
  π : N →ₛₗ[ψ.toRingHom] M
  π_surjective : Function.Surjective π
  ker_π : LinearMap.ker π =
    (Ideal.span (Set.range fun i : Fin r => φ (MvPowerSeries.X i))) •
      (⊤ : Submodule (MvPowerSeries (Fin r) 𝒪) N)
  d : ℕ
  b : Fin d → N
  b_span : ∀ x : N, ∃ c : Fin d → MvPowerSeries (Fin r) 𝒪, x = ∑ i, φ (c i) • b i
  b_rel : ∀ c : Fin d → MvPowerSeries (Fin r) 𝒪, ∑ i, φ (c i) • b i = 0 ↔ ∀ i, c i ∈ J

Used by 1

Used byTaylor–Wiles patching datum

StructureTaylor–Wiles patching datum#✓fully proved

A Taylor–Wiles patching datum: a patching level for every n, with the relation ideal at level n generated by (1 + Xⱼ)^(ℓⁿ) - 1. This structure records an indexed family of finite-level data.

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) 𝒪)))

Uses 1

Statement usesLevel of a Taylor–Wiles patching datum

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.