OAI/AlgebraicGeometry/CharacterVarieties/Seams/BoundaryWords.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.fiberCoefficient line 18
2. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.fiberCoefficient_one line 20
3. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.fiberCoefficient_rebase line 25
4. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandCoefficient line 40
5. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandCoefficient_old line 43
6. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandCoefficient_strip line 57
7. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandCoefficient_shortCycle line 65
8. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.actual_secondary_matrix_word line 73

   Source documentation

   A nonprincipal old boundary retains its based matrix product over the coefficient ring.

   theorem actual_secondary_matrix_word (hshort : ∀ b i,short b (some i)=1)
       (hinj : Function.Injective B.shortRoot) (f : F)
       (s : Finset (Side S arity))
       (hs : A.vertexAssembly.corners.boundaryNext.IsCycleOn (s : Set (Side S arity)))
       (hq : (⟨q,none⟩ : Side S arity)∉s) (a : Side S arity) (ha : a∈s) :
       cycleWord (next A q B) (bandCoefficient A q B rank old short f)
         (oldEmbedding A q B a) (secondaryCircle A q B s).card=
       cycleWord A.vertexAssembly.corners.boundaryNext
         (fun a => fiberCoefficient rank f (old a)) a s.card := by
   …

   Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.next, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandCoefficient, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldEmbedding, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.secondaryCircle, OAI.IntegralCharacterVarieties.OccurrenceIncidence.fiberCoefficient

9. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.chain_word_prefix line 105
10. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.chain_word_allBases line 114
11. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.originalSide_injective line 128
12. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.principalCircle_card line 133
13. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorCircle_card line 145
14. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.actual_principal_word_allBases line 153
15. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandCoefficient_original line 193
16. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.actual_principal_matrix_word line 198
17. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.oldGraftCircle_word line 225
18. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedWordPreDiagram line 256

    Source documentation

    The old diagram with its ranks extended to the grafted facets.

    noncomputable def refinedWordPreDiagram : Diagram (D.ports.RefinedBandFacet q d) S V arity :=
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram

19. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedOldBoundary line 260
20. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMirrorBoundary line 263
21. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedLabel_old line 267
22. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedLabel_mirror line 271
23. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedLabel_fresh line 275
24. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedWordPreCoefficient line 278
25. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.cycleWord_of_cycleEntry line 295
26. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandCoefficient_mirror line 314
27. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorCircle_word line 324
28. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.freshCircle_word line 334
29. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarked_boundaryWord line 362
30. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarked_boundaryWord_old line 372
31. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarked_boundaryWord_mirror line 396
32. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarked_boundaryWord_fresh line 409