Matching classified objects across an equivalence #
The refined Torelli arguments first recover the exceptional-block indices from their residual projection objects. Completeness says that the image of each classified object is a shift of a target candidate; separation makes the target index unique. Applying the same argument to the inverse equivalence proves that the resulting map is a bijection.
This file carries out that formal argument for both classification shapes used by the Enriques papers. For a mixed classification, positivity of the block lengths is the only extra hypothesis needed to know that every candidate is either spherical or pseudoprojective. The result preserves the coarse block kind (singleton versus longer); equality of the lengths of two longer blocks requires the subsequent extension induction and is deliberately not asserted here.
noncomputable def
CategoryTheory.SerreFunctor.SphericalClassificationData.matchIndex
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[HasShift C ℤ]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Linear k D]
[HasShift D ℤ]
{S_C : SerreFunctorData k C}
{S_D : SerreFunctorData k D}
{n : ℕ}
{I : Type t}
{J : Type t'}
(A : SphericalClassificationData S_C n I)
(B : SphericalClassificationData S_D n J)
(F : SerreCompatibleEquivalence S_C S_D)
(i : I)
:
J
The target index represented by the image of a source candidate.
Equations
- A.matchIndex B F i = Classical.choose ⋯
Instances For
theorem
CategoryTheory.SerreFunctor.SphericalClassificationData.matchIndex_spec
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[HasShift C ℤ]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Linear k D]
[HasShift D ℤ]
{S_C : SerreFunctorData k C}
{S_D : SerreFunctorData k D}
{n : ℕ}
{I : Type t}
{J : Type t'}
(A : SphericalClassificationData S_C n I)
(B : SphericalClassificationData S_D n J)
(F : SerreCompatibleEquivalence S_C S_D)
(i : I)
:
The image of a source candidate is a shift of its matched target candidate.
theorem
CategoryTheory.SerreFunctor.SphericalClassificationData.matchIndex_injective
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[HasShift C ℤ]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Linear k D]
[HasShift D ℤ]
{S_C : SerreFunctorData k C}
{S_D : SerreFunctorData k D}
{n : ℕ}
{I : Type t}
{J : Type t'}
(A : SphericalClassificationData S_C n I)
(B : SphericalClassificationData S_D n J)
(F : SerreCompatibleEquivalence S_C S_D)
:
Function.Injective (A.matchIndex B F)
Separation of the classified candidates makes the matching map injective.
theorem
CategoryTheory.SerreFunctor.SphericalClassificationData.reverse_matchIndex_injective
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[HasShift C ℤ]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Linear k D]
[HasShift D ℤ]
{S_C : SerreFunctorData k C}
{S_D : SerreFunctorData k D}
{n : ℕ}
{I : Type t}
{J : Type t'}
(A : SphericalClassificationData S_C n I)
(B : SphericalClassificationData S_D n J)
(F : SerreCompatibleEquivalence S_C S_D)
:
Function.Injective (B.matchIndex A F.symm)
The inverse classification gives an injection in the opposite direction.
noncomputable def
CategoryTheory.SerreFunctor.SphericalClassificationData.matchingEquiv
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[HasShift C ℤ]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Linear k D]
[HasShift D ℤ]
{S_C : SerreFunctorData k C}
{S_D : SerreFunctorData k D}
{n : ℕ}
{I : Type t}
{J : Type t'}
(A : SphericalClassificationData S_C n I)
(B : SphericalClassificationData S_D n J)
(F : SerreCompatibleEquivalence S_C S_D)
[Fintype I]
[Fintype J]
:
Classified spherical candidates are canonically reindexed by a Serre-compatible equivalence.
Equations
- A.matchingEquiv B F = Equiv.ofBijective (A.matchIndex B F) ⋯
Instances For
@[simp]
theorem
CategoryTheory.SerreFunctor.SphericalClassificationData.matchingEquiv_apply
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[HasShift C ℤ]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Linear k D]
[HasShift D ℤ]
{S_C : SerreFunctorData k C}
{S_D : SerreFunctorData k D}
{n : ℕ}
{I : Type t}
{J : Type t'}
(A : SphericalClassificationData S_C n I)
(B : SphericalClassificationData S_D n J)
(F : SerreCompatibleEquivalence S_C S_D)
[Fintype I]
[Fintype J]
(i : I)
:
theorem
CategoryTheory.SerreFunctor.SphericalClassificationData.matchingEquiv_spec
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[HasShift C ℤ]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Linear k D]
[HasShift D ℤ]
{S_C : SerreFunctorData k C}
{S_D : SerreFunctorData k D}
{n : ℕ}
{I : Type t}
{J : Type t'}
(A : SphericalClassificationData S_C n I)
(B : SphericalClassificationData S_D n J)
(F : SerreCompatibleEquivalence S_C S_D)
[Fintype I]
[Fintype J]
(i : I)
:
The matching equivalence carries the candidate-shift comparison proved by completeness.
noncomputable def
CategoryTheory.SerreFunctor.MixedClassificationData.matchIndex
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[HasShift C ℤ]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Linear k D]
[HasShift D ℤ]
{S_C : SerreFunctorData k C}
{S_D : SerreFunctorData k D}
{n : ℕ}
{I : Type t}
{J : Type t'}
(A : MixedClassificationData S_C n I)
(B : MixedClassificationData S_D n J)
(F : SerreCompatibleEquivalence S_C S_D)
(hA : ∀ (i : I), 0 < A.blockLength i)
(i : I)
:
J
The target index represented by the image of a source candidate. The definition branches only on whether the source block is a singleton or a longer block.
Equations
- A.matchIndex B F hA i = if hi : A.blockLength i = 1 then Classical.choose ⋯ else Classical.choose ⋯
Instances For
theorem
CategoryTheory.SerreFunctor.MixedClassificationData.matchIndex_length_eq_one
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[HasShift C ℤ]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Linear k D]
[HasShift D ℤ]
{S_C : SerreFunctorData k C}
{S_D : SerreFunctorData k D}
{n : ℕ}
{I : Type t}
{J : Type t'}
(A : MixedClassificationData S_C n I)
(B : MixedClassificationData S_D n J)
(F : SerreCompatibleEquivalence S_C S_D)
(hA : ∀ (i : I), 0 < A.blockLength i)
{i : I}
(hi : A.blockLength i = 1)
:
Singleton source blocks match singleton target blocks.
theorem
CategoryTheory.SerreFunctor.MixedClassificationData.matchIndex_length_two_le
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[HasShift C ℤ]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Linear k D]
[HasShift D ℤ]
{S_C : SerreFunctorData k C}
{S_D : SerreFunctorData k D}
{n : ℕ}
{I : Type t}
{J : Type t'}
(A : MixedClassificationData S_C n I)
(B : MixedClassificationData S_D n J)
(F : SerreCompatibleEquivalence S_C S_D)
(hA : ∀ (i : I), 0 < A.blockLength i)
{i : I}
(hi : 2 ≤ A.blockLength i)
:
Longer source blocks match longer target blocks.
theorem
CategoryTheory.SerreFunctor.MixedClassificationData.matchIndex_spec
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[HasShift C ℤ]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Linear k D]
[HasShift D ℤ]
{S_C : SerreFunctorData k C}
{S_D : SerreFunctorData k D}
{n : ℕ}
{I : Type t}
{J : Type t'}
(A : MixedClassificationData S_C n I)
(B : MixedClassificationData S_D n J)
(F : SerreCompatibleEquivalence S_C S_D)
(hA : ∀ (i : I), 0 < A.blockLength i)
(i : I)
:
The image of every source candidate is a shift of its matched target candidate.
theorem
CategoryTheory.SerreFunctor.MixedClassificationData.matchIndex_injective
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[HasShift C ℤ]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Linear k D]
[HasShift D ℤ]
{S_C : SerreFunctorData k C}
{S_D : SerreFunctorData k D}
{n : ℕ}
{I : Type t}
{J : Type t'}
(A : MixedClassificationData S_C n I)
(B : MixedClassificationData S_D n J)
(F : SerreCompatibleEquivalence S_C S_D)
(hA : ∀ (i : I), 0 < A.blockLength i)
:
Function.Injective (A.matchIndex B F hA)
Separation of spherical and pseudoprojective candidates makes the mixed matching injective.
noncomputable def
CategoryTheory.SerreFunctor.MixedClassificationData.matchingEquiv
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[HasShift C ℤ]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Linear k D]
[HasShift D ℤ]
{S_C : SerreFunctorData k C}
{S_D : SerreFunctorData k D}
{n : ℕ}
{I : Type t}
{J : Type t'}
(A : MixedClassificationData S_C n I)
(B : MixedClassificationData S_D n J)
(F : SerreCompatibleEquivalence S_C S_D)
(hA : ∀ (i : I), 0 < A.blockLength i)
(hB : ∀ (j : J), 0 < B.blockLength j)
[Fintype I]
[Fintype J]
:
Mixed classified candidates are reindexed by a Serre-compatible equivalence.
Equations
- A.matchingEquiv B F hA hB = Equiv.ofBijective (A.matchIndex B F hA) ⋯
Instances For
@[simp]
theorem
CategoryTheory.SerreFunctor.MixedClassificationData.matchingEquiv_apply
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[HasShift C ℤ]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Linear k D]
[HasShift D ℤ]
{S_C : SerreFunctorData k C}
{S_D : SerreFunctorData k D}
{n : ℕ}
{I : Type t}
{J : Type t'}
(A : MixedClassificationData S_C n I)
(B : MixedClassificationData S_D n J)
(F : SerreCompatibleEquivalence S_C S_D)
(hA : ∀ (i : I), 0 < A.blockLength i)
(hB : ∀ (j : J), 0 < B.blockLength j)
[Fintype I]
[Fintype J]
(i : I)
:
theorem
CategoryTheory.SerreFunctor.MixedClassificationData.matchingEquiv_length_eq_one_iff
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[HasShift C ℤ]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Linear k D]
[HasShift D ℤ]
{S_C : SerreFunctorData k C}
{S_D : SerreFunctorData k D}
{n : ℕ}
{I : Type t}
{J : Type t'}
(A : MixedClassificationData S_C n I)
(B : MixedClassificationData S_D n J)
(F : SerreCompatibleEquivalence S_C S_D)
(hA : ∀ (i : I), 0 < A.blockLength i)
(hB : ∀ (j : J), 0 < B.blockLength j)
[Fintype I]
[Fintype J]
(i : I)
:
The matching equivalence preserves singleton blocks.
theorem
CategoryTheory.SerreFunctor.MixedClassificationData.matchingEquiv_length_two_le_iff
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[HasShift C ℤ]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Linear k D]
[HasShift D ℤ]
{S_C : SerreFunctorData k C}
{S_D : SerreFunctorData k D}
{n : ℕ}
{I : Type t}
{J : Type t'}
(A : MixedClassificationData S_C n I)
(B : MixedClassificationData S_D n J)
(F : SerreCompatibleEquivalence S_C S_D)
(hA : ∀ (i : I), 0 < A.blockLength i)
(hB : ∀ (j : J), 0 < B.blockLength j)
[Fintype I]
[Fintype J]
(i : I)
:
The matching equivalence preserves longer blocks.
theorem
CategoryTheory.SerreFunctor.MixedClassificationData.matchingEquiv_spec
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[HasShift C ℤ]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Linear k D]
[HasShift D ℤ]
{S_C : SerreFunctorData k C}
{S_D : SerreFunctorData k D}
{n : ℕ}
{I : Type t}
{J : Type t'}
(A : MixedClassificationData S_C n I)
(B : MixedClassificationData S_D n J)
(F : SerreCompatibleEquivalence S_C S_D)
(hA : ∀ (i : I), 0 < A.blockLength i)
(hB : ∀ (j : J), 0 < B.blockLength j)
[Fintype I]
[Fintype J]
(i : I)
:
The image of every mixed candidate is a shift of the target candidate selected by the matching equivalence.