Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CategoryTheory_Subfunctor_OfIsTerminal.lean

definition moduleadapted from the Imperial College London FLT project: FLT/Deformations/Subfunctor.lean

Subfunctor cut out by a subset at a terminal object

Let \mathcal C be a category and F\colon\mathcal C\to\mathbf{Set} a functor to types. The single declaration CategoryTheory.Subfunctor.ofIsTerminal takes an object X of \mathcal C together with a witness hX that X is terminal, and a subset s\subseteq F(X), and produces a subfunctor of F in the sense of Mathlib's CategoryTheory.Subfunctor: a family of subsets of the values of F stable under the maps of F. Its value at an object U is the preimage \bigl(F(!_U)\bigr)^{-1}(s)\subseteq F(U), where !_U\colon U\to X is the unique morphism to the terminal object, obtained from hX. Thus an element x\in F(U) lies in the subfunctor exactly when its image under the structure map to F(X) belongs to s; the subfunctor is the fibre of F over s along the canonical transformation to the constant value F(X). The stability condition required by Subfunctor is that for every morphism i\colon U\to V the map F(i) carries the subset attached to U into the subset attached to V; this holds because !_U factors as i followed by !_V by terminality of X, so that F(!_V)\circ F(i)=F(!_U) and the two preimages agree. No condition is imposed on s, and no limit or size hypothesis beyond the terminality of X is used; the subfunctor is obtained for an arbitrary subset of F(X), in particular for a singleton s=\{x\}, where it is the subfunctor of elements lying over the chosen point x\in F(X).

Relation to Mathlib

Built directly on Mathlib's CategoryTheory.Subfunctor structure for functors to Type w; it adds this one construction, a subfunctor defined as the fibre of a subset of the value at a terminal object.

Where it is used

The construction is the mechanism by which the functor of lifts of a fixed residual representation is cut out of a functor of representations in deformation theory: on a category of coefficient algebras whose terminal object is the residue field, reduction is the map to the value at the terminal object, and taking s to be the singleton of the residual representation gives the subfunctor of lifts, and similarly the deformation functor inside representations up to strict equivalence.

References

  1. B. Mazur, Deforming Galois representations, in: Galois Groups over \mathbb{Q}, MSRI Publications 16, Springer, 1989, 385–437
  2. S. Mac Lane, Categories for the Working Mathematician, 2nd ed., Graduate Texts in Mathematics 5, Springer, 1998

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_CategoryTheory_Subfunctor_OfIsTerminal.lean

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

set_option autoImplicit false

universe w v u

open CategoryTheory

namespace CategoryTheory
namespace Subfunctor

variable {C : Type u} [Category.{v} C] (F : C ⥤ Type w)

def ofIsTerminal {X : C} (hX : Limits.IsTerminal X) (s : Set (F.obj X)) :
    Subfunctor F where
  obj U := F.map (hX.from U) ⁻¹' s
  map {U V} i := by
    simp only [← Set.preimage_comp, ← hX.comp_from i, F.map_comp]
    rfl

end Subfunctor
end CategoryTheory

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).