Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CerednikDrinfeld_MumfordGlue.lean

definition module

Mumford gluing data for the formal upper half-plane

Fix a commutative ring \mathcal O, an element \pi\in\mathcal O, a field K_0 that is an \mathcal O-algebra, a natural number r, an element g_1\in GL_2(K_0) and a subgroup N\le PGL_2(K_0). Write \mathcal O_n=\mathcal O/(\pi^{n+1}), let A= chartERing π’ͺ Ο€ r be the localisation of \mathcal O[X_0,X_1]/(X_0X_1-\pi) away from (\xi^{r-1}-1)(\eta^{r-1}-1), where \xi,\eta are the images of X_0,X_1, and let A_n=A/(\pi^{n+1}A). The structure MumfordGlue records, as data and axioms: schemes Z_n (in universe 0) with morphisms \mathrm{zb}_n\colon Z_n\to\operatorname{Spec}\mathcal O_n, flat and separated, and transition morphisms \mathrm{zt}_n\colon Z_n\to Z_{n+1} making Z_n the fibre product of Z_{n+1} with \operatorname{Spec}\mathcal O_n over \operatorname{Spec}\mathcal O_{n+1}; and for every h\in GL_2(K_0) and every n a morphism \zeta_{h,n}\colon\operatorname{Spec}A_n\to Z_n which is an open immersion, lies over \operatorname{Spec}\mathcal O, and is compatible with the transition maps \operatorname{Spec}A_n\to\operatorname{Spec}A_{n+1} and \mathrm{zt}_n. Two finiteness/invariance axioms say that for each n some finite set of h's suffices for the images of the \zeta_{h,n} to cover the points of Z_n, and that \zeta_{gh,n}=\zeta_{h,n} whenever the class of g lies in N.

The remaining fields express the overlap law in terms of Deligne data. For an \mathcal O-algebra B and an \mathcal O-algebra map x\colon A_n\to B, the relevant data d over B are those whose line at the standard full lattice M_0 is spanned by x(\xi)\otimes e_0+1\otimes e_1, whose line at g_1M_0 is the corresponding image of the span of 1\otimes e_0+x(\eta)\otimes e_1, and which satisfy InEdgeChart for the pair (g_1M_0,M_0), i.e. at every prime of B the edge non-degeneracy conditions g_1M_0\subseteq M_0, \pi M_0\subseteq g_1M_0 and the two mod-\mathfrak p conditions on vectors of M_0 outside g_1M_0 and on vectors of g_1M_0 not divisible by \pi. With P, P' related to d, d' by DeligneDatum.IsPullback along h^{-1}, h'^{-1}: ΞΆ_rel asserts that if P and P' are related by some g whose class lies in N then \operatorname{Spec}(x) followed by \zeta_{h,n} equals \operatorname{Spec}(x') followed by \zeta_{h',n}; ΞΆ_overlap_local upgrades this to an equivalence when B is local; ΞΆ_overlap_zar asserts, for arbitrary B, that equality of the two composites yields a finite family f_i\in B generating the unit ideal such that over every localisation C of B away from f_i the base changes of P and P' are related by an element with class in N. Finally ΞΆ_univ is a universal property: any family t_h\colon\operatorname{Spec}A_n\to T satisfying the compatibility of ΞΆ_rel factors uniquely through a morphism Z_n\to T, so that Z_n with the family (\zeta_{h,n})_h is the colimit of the chart family in schemes. Thus the structure is a presentation of a formal quotient by N chosen model by model, with flatness, separatedness, the covering property and the overlap equivalences carried as fields rather than derived; no uniqueness of a MumfordGlue is asserted here.

Relation to Mathlib

The scheme-theoretic vocabulary is Mathlib's (Scheme, Spec, IsPullback, Flat, IsSeparated, IsOpenImmersion, IsLocalization.Away); the chart rings, Deligne data and the gluing structure itself are the project's own, Mathlib having no formal upper half-plane or Mumford-quotient notions.

Where it is used

The structure packages the gluing of edge charts of the formal upper half-plane along a discrete subgroup, the algebraic input to the Čerednik–Drinfeld description of Shimura curves and their reduction at a prime dividing the level, which in turn feeds the analysis of the bad-reduction fibres used in level lowering.

References

  1. D. Mumford, An analytic construction of degenerating curves over complete local rings, Compositio Mathematica 24 (1972), 129–174, Β§3
  2. L. Gerritzen and M. van der Put, Schottky groups and Mumford curves, Lecture Notes in Mathematics 817, Springer, 1980, Chapter III
  3. J.-F. Boutot and H. Carayol, Uniformisation p-adique des courbes de Shimura: les thΓ©orΓ¨mes de Čerednik et de Drinfeld, AstΓ©risque 196–197 (1991), 45–158

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_CerednikDrinfeld_MumfordGlue.lean

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_CerednikDrinfeld_FormalUpperHalfPlanePoints
import Definitions.Def_CerednikDrinfeld_FormalUpperHalfPlaneChartRings

set_option autoImplicit false

open scoped TensorProduct MatrixGroups
open CategoryTheory AlgebraicGeometry LT.LatticeTree

namespace CerednikDrinfeld
namespace FormalOmega

set_option genInjectivity false in
set_option genSizeOfSpec false in

structure MumfordGlue
    (π’ͺ : Type) [CommRing π’ͺ] (Ο€ : π’ͺ) (Kβ‚€ : Type) [Field Kβ‚€] [Algebra π’ͺ Kβ‚€] (r : β„•)
    (g₁ : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€) (N : Subgroup (PGL(2, Kβ‚€))) : Type 1 where

  Z : β„• β†’ Scheme.{0}

  zb : βˆ€ n : β„•, Z n ⟢ Spec (CommRingCat.of (π’ͺ β§Έ Ideal.span {Ο€ ^ (n + 1)}))

  zt : βˆ€ n : β„•, Z n ⟢ Z (n + 1)

  zt_isPullback : βˆ€ n : β„•, IsPullback (zt n) (zb n) (zb (n + 1))
    (Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor (Ideal.span_singleton_le_span_singleton.mpr (pow_dvd_pow Ο€ (Nat.le_succ (n + 1)))))))

  zb_flat : βˆ€ n : β„•, Flat (zb n)

  zb_isSeparated : βˆ€ n : β„•, IsSeparated (zb n)

  ΞΆ : βˆ€ (h : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€) (n : β„•), Spec (CommRingCat.of ((chartERing π’ͺ Ο€ r) β§Έ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) ⟢ Z n

  ΞΆ_over : βˆ€ (h : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€) (n : β„•),
    ΞΆ h n ≫ zb n ≫ Spec.map (CommRingCat.ofHom (algebraMap π’ͺ (π’ͺ β§Έ Ideal.span {Ο€ ^ (n + 1)}))) =
      Spec.map (CommRingCat.ofHom (algebraMap π’ͺ ((chartERing π’ͺ Ο€ r) β§Έ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))))

  ΞΆ_zt : βˆ€ (h : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€) (n : β„•),
    ΞΆ h n ≫ zt n = Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor
      (Ideal.span_singleton_le_span_singleton.mpr (pow_dvd_pow (algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) (Nat.le_succ (n + 1)))))) ≫ ΞΆ h (n + 1)

  ΞΆ_isOpenImmersion : βˆ€ (h : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€) (n : β„•), IsOpenImmersion (ΞΆ h n)

  ΞΆ_cover : βˆ€ n : β„•, βˆƒ S : Finset (Matrix.GeneralLinearGroup (Fin 2) Kβ‚€), βˆ€ z : Z n, βˆƒ h ∈ S, z ∈ Set.range (ΞΆ h n).base

  ΞΆ_inv : βˆ€ (g h : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€) (n : β„•), Matrix.ProjGenLinGroup.mk g ∈ N β†’ ΞΆ (g * h) n = ΞΆ h n

  ΞΆ_rel : βˆ€ (n : β„•) (B : Type) [CommRing B] [Algebra π’ͺ B]
    (h h' : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€) (xq xq' : ((chartERing π’ͺ Ο€ r) β§Έ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)})) →ₐ[π’ͺ] B) (d d' P P' : DeligneDatum (K := Kβ‚€) Ο€ B),
    (d.line (stdFullLattice Kβ‚€) =
          Submodule.span B {((xq.comp (Ideal.Quotient.mkₐ π’ͺ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) (chartERing.ΞΎ π’ͺ Ο€ r)) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + (1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1} ∧
        d.line (FullLattice.act g₁ (stdFullLattice Kβ‚€)) =
          (Submodule.span B {(1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + ((xq.comp (Ideal.Quotient.mkₐ π’ͺ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) (chartERing.Ξ· π’ͺ Ο€ r)) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1}).map
            (actBaseChange B g₁ (stdFullLattice Kβ‚€)).toLinearMap ∧
        d.InEdgeChart Ο€ (FullLattice.act g₁ (stdFullLattice Kβ‚€)) (stdFullLattice Kβ‚€)) β†’
    (d'.line (stdFullLattice Kβ‚€) =
          Submodule.span B {((xq'.comp (Ideal.Quotient.mkₐ π’ͺ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) (chartERing.ΞΎ π’ͺ Ο€ r)) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + (1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1} ∧
        d'.line (FullLattice.act g₁ (stdFullLattice Kβ‚€)) =
          (Submodule.span B {(1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + ((xq'.comp (Ideal.Quotient.mkₐ π’ͺ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) (chartERing.Ξ· π’ͺ Ο€ r)) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1}).map
            (actBaseChange B g₁ (stdFullLattice Kβ‚€)).toLinearMap ∧
        d'.InEdgeChart Ο€ (FullLattice.act g₁ (stdFullLattice Kβ‚€)) (stdFullLattice Kβ‚€)) β†’
    DeligneDatum.IsPullback (K := Kβ‚€) (Ο€ := Ο€) B h⁻¹ d P β†’ DeligneDatum.IsPullback (K := Kβ‚€) (Ο€ := Ο€) B h'⁻¹ d' P' β†’
    (βˆƒ g : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€, Matrix.ProjGenLinGroup.mk g ∈ N ∧ DeligneDatum.IsPullback (K := Kβ‚€) (Ο€ := Ο€) B g⁻¹ P P') β†’
    Spec.map (CommRingCat.ofHom xq.toRingHom) ≫ ΞΆ h n = Spec.map (CommRingCat.ofHom xq'.toRingHom) ≫ ΞΆ h' n

  ΞΆ_overlap_local : βˆ€ (n : β„•) (B : Type) [CommRing B] [IsLocalRing B] [Algebra π’ͺ B]
    (h h' : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€) (xq xq' : ((chartERing π’ͺ Ο€ r) β§Έ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)})) →ₐ[π’ͺ] B) (d d' P P' : DeligneDatum (K := Kβ‚€) Ο€ B),
    (d.line (stdFullLattice Kβ‚€) =
          Submodule.span B {((xq.comp (Ideal.Quotient.mkₐ π’ͺ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) (chartERing.ΞΎ π’ͺ Ο€ r)) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + (1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1} ∧
        d.line (FullLattice.act g₁ (stdFullLattice Kβ‚€)) =
          (Submodule.span B {(1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + ((xq.comp (Ideal.Quotient.mkₐ π’ͺ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) (chartERing.Ξ· π’ͺ Ο€ r)) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1}).map
            (actBaseChange B g₁ (stdFullLattice Kβ‚€)).toLinearMap ∧
        d.InEdgeChart Ο€ (FullLattice.act g₁ (stdFullLattice Kβ‚€)) (stdFullLattice Kβ‚€)) β†’
    (d'.line (stdFullLattice Kβ‚€) =
          Submodule.span B {((xq'.comp (Ideal.Quotient.mkₐ π’ͺ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) (chartERing.ΞΎ π’ͺ Ο€ r)) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + (1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1} ∧
        d'.line (FullLattice.act g₁ (stdFullLattice Kβ‚€)) =
          (Submodule.span B {(1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + ((xq'.comp (Ideal.Quotient.mkₐ π’ͺ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) (chartERing.Ξ· π’ͺ Ο€ r)) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1}).map
            (actBaseChange B g₁ (stdFullLattice Kβ‚€)).toLinearMap ∧
        d'.InEdgeChart Ο€ (FullLattice.act g₁ (stdFullLattice Kβ‚€)) (stdFullLattice Kβ‚€)) β†’
    DeligneDatum.IsPullback (K := Kβ‚€) (Ο€ := Ο€) B h⁻¹ d P β†’ DeligneDatum.IsPullback (K := Kβ‚€) (Ο€ := Ο€) B h'⁻¹ d' P' β†’
    (Spec.map (CommRingCat.ofHom xq.toRingHom) ≫ ΞΆ h n = Spec.map (CommRingCat.ofHom xq'.toRingHom) ≫ ΞΆ h' n ↔
      βˆƒ g : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€, Matrix.ProjGenLinGroup.mk g ∈ N ∧ DeligneDatum.IsPullback (K := Kβ‚€) (Ο€ := Ο€) B g⁻¹ P P')

  ΞΆ_overlap_zar : βˆ€ (n : β„•) (B : Type) [CommRing B] [Algebra π’ͺ B]
    (h h' : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€) (xq xq' : ((chartERing π’ͺ Ο€ r) β§Έ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)})) →ₐ[π’ͺ] B) (d d' P P' : DeligneDatum (K := Kβ‚€) Ο€ B),
    (d.line (stdFullLattice Kβ‚€) =
          Submodule.span B {((xq.comp (Ideal.Quotient.mkₐ π’ͺ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) (chartERing.ΞΎ π’ͺ Ο€ r)) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + (1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1} ∧
        d.line (FullLattice.act g₁ (stdFullLattice Kβ‚€)) =
          (Submodule.span B {(1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + ((xq.comp (Ideal.Quotient.mkₐ π’ͺ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) (chartERing.Ξ· π’ͺ Ο€ r)) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1}).map
            (actBaseChange B g₁ (stdFullLattice Kβ‚€)).toLinearMap ∧
        d.InEdgeChart Ο€ (FullLattice.act g₁ (stdFullLattice Kβ‚€)) (stdFullLattice Kβ‚€)) β†’
    (d'.line (stdFullLattice Kβ‚€) =
          Submodule.span B {((xq'.comp (Ideal.Quotient.mkₐ π’ͺ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) (chartERing.ΞΎ π’ͺ Ο€ r)) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + (1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1} ∧
        d'.line (FullLattice.act g₁ (stdFullLattice Kβ‚€)) =
          (Submodule.span B {(1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + ((xq'.comp (Ideal.Quotient.mkₐ π’ͺ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) (chartERing.Ξ· π’ͺ Ο€ r)) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1}).map
            (actBaseChange B g₁ (stdFullLattice Kβ‚€)).toLinearMap ∧
        d'.InEdgeChart Ο€ (FullLattice.act g₁ (stdFullLattice Kβ‚€)) (stdFullLattice Kβ‚€)) β†’
    DeligneDatum.IsPullback (K := Kβ‚€) (Ο€ := Ο€) B h⁻¹ d P β†’ DeligneDatum.IsPullback (K := Kβ‚€) (Ο€ := Ο€) B h'⁻¹ d' P' β†’
    Spec.map (CommRingCat.ofHom xq.toRingHom) ≫ ΞΆ h n = Spec.map (CommRingCat.ofHom xq'.toRingHom) ≫ ΞΆ h' n β†’
      βˆƒ (ΞΉ : Type) (_ : Finite ΞΉ) (f : ΞΉ β†’ B), Ideal.span (Set.range f) = ⊀ ∧
        βˆ€ (i : ΞΉ) (C : Type) [CommRing C] [Algebra π’ͺ C] [Algebra B C] [IsScalarTower π’ͺ B C] [IsLocalization.Away (f i) C],
          βˆƒ g : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€, Matrix.ProjGenLinGroup.mk g ∈ N ∧
            DeligneDatum.IsPullback (K := Kβ‚€) (Ο€ := Ο€) C g⁻¹ ((Omega Kβ‚€ Ο€).map (IsScalarTower.toAlgHom π’ͺ B C) P)
              ((Omega Kβ‚€ Ο€).map (IsScalarTower.toAlgHom π’ͺ B C) P')

  ΞΆ_univ : βˆ€ (n : β„•) (T : Scheme.{0}) (t : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€ β†’ (Spec (CommRingCat.of ((chartERing π’ͺ Ο€ r) β§Έ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) ⟢ T)),
    (βˆ€ (B : Type) [CommRing B] [Algebra π’ͺ B]
      (h h' : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€) (xq xq' : ((chartERing π’ͺ Ο€ r) β§Έ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)})) →ₐ[π’ͺ] B) (d d' P P' : DeligneDatum (K := Kβ‚€) Ο€ B),
      (d.line (stdFullLattice Kβ‚€) =
            Submodule.span B {((xq.comp (Ideal.Quotient.mkₐ π’ͺ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) (chartERing.ΞΎ π’ͺ Ο€ r)) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + (1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1} ∧
          d.line (FullLattice.act g₁ (stdFullLattice Kβ‚€)) =
            (Submodule.span B {(1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + ((xq.comp (Ideal.Quotient.mkₐ π’ͺ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) (chartERing.Ξ· π’ͺ Ο€ r)) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1}).map
              (actBaseChange B g₁ (stdFullLattice Kβ‚€)).toLinearMap ∧
          d.InEdgeChart Ο€ (FullLattice.act g₁ (stdFullLattice Kβ‚€)) (stdFullLattice Kβ‚€)) β†’
      (d'.line (stdFullLattice Kβ‚€) =
            Submodule.span B {((xq'.comp (Ideal.Quotient.mkₐ π’ͺ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) (chartERing.ΞΎ π’ͺ Ο€ r)) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + (1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1} ∧
          d'.line (FullLattice.act g₁ (stdFullLattice Kβ‚€)) =
            (Submodule.span B {(1 : B) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 0 + ((xq'.comp (Ideal.Quotient.mkₐ π’ͺ (Ideal.span {(algebraMap π’ͺ (chartERing π’ͺ Ο€ r) Ο€) ^ (n + 1)}))) (chartERing.Ξ· π’ͺ Ο€ r)) βŠ—β‚œ[π’ͺ] stdBasisVec Kβ‚€ 1}).map
              (actBaseChange B g₁ (stdFullLattice Kβ‚€)).toLinearMap ∧
          d'.InEdgeChart Ο€ (FullLattice.act g₁ (stdFullLattice Kβ‚€)) (stdFullLattice Kβ‚€)) β†’
      DeligneDatum.IsPullback (K := Kβ‚€) (Ο€ := Ο€) B h⁻¹ d P β†’ DeligneDatum.IsPullback (K := Kβ‚€) (Ο€ := Ο€) B h'⁻¹ d' P' β†’
      (βˆƒ g : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€, Matrix.ProjGenLinGroup.mk g ∈ N ∧ DeligneDatum.IsPullback (K := Kβ‚€) (Ο€ := Ο€) B g⁻¹ P P') β†’
      Spec.map (CommRingCat.ofHom xq.toRingHom) ≫ t h = Spec.map (CommRingCat.ofHom xq'.toRingHom) ≫ t h') β†’
    βˆƒ! u : Z n ⟢ T, βˆ€ h : Matrix.GeneralLinearGroup (Fin 2) Kβ‚€, ΞΆ h n ≫ u = t h

end FormalOmega
end CerednikDrinfeld

Statements phrased using this module (11)