AlgebraicPictures.lean`

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TorsionFreeZeroDivisors.WordBlocks.Matching.removeConjugator line 14
Source documentation
Remove exactly the actual conjugating word, not a replacement reduced representative. Each removal is the proved cap splice on the same boundary.
```
def Matching.removeConjugator (c w : List (A×Bool)) (ws : List (List (A×Bool)))
    (d : Matching WordPairing.inverseLetter ((c++w++invRev c)::ws)) :
    Matching WordPairing.inverseLetter (w::ws) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WordBlocks.Matching, OAI.TorsionFreeZeroDivisors.WordPairing.inverseLetter
def OAI.TorsionFreeZeroDivisors.WordBlocks.Matching.removeConjugatorAt line 26
def OAI.TorsionFreeZeroDivisors.AlgebraicPictures.coreWords line 35
def OAI.TorsionFreeZeroDivisors.AlgebraicPictures.stripConjugators line 36
theorem OAI.TorsionFreeZeroDivisors.AlgebraicPictures.quotient_core_matching line 52
Source documentation
A literal quotient-null word supplies actual planar inverse-letter matching on the outer inverse word and signed relator cores, with all conjugating paths removed by genuine genus-zero preserving surgery. This is still finite permutation data, not an assumed topological surface or graph lift.
```
theorem quotient_core_matching (outer : List (A×Bool))
    (h : PresentedGroup.mk (relations rel) (mk outer)=1) :
    ∃ts : List (Term (A:=A) (I:=I)),
…
```
Mentions: OAI.TorsionFreeZeroDivisors.AlgebraicPictures.relations, OAI.TorsionFreeZeroDivisors.AlgebraicPictures.Term
inductive OAI.TorsionFreeZeroDivisors.GraphPresentation.Path line 68
Source documentation
An ordinary port path; no reduction assumption, and loops and parallel edges remain distinct. This is used for the exact graph relators.
```
inductive Path : V→V→Type
  | nil (v : V) : Path v v
  | cons (d : D) {b : V} (p : Path (Γ.origin (Γ.reverse d)) b) : Path (Γ.origin d) b
namespace Path
variable {Γ} {a b c : V}
```
def OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.append line 73
def OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.single line 76
def OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.cast line 77
def OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.reverse line 79
def OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.eval line 87
lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.eval_nil line 90
lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.eval_cons line 92
lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.eval_append line 95
lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.eval_single line 101
lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.eval_cast line 103
lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.eval_reverse line 107
lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.eval_map line 116
def OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.darts line 128
lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.darts_nil line 131
lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.darts_cons line 132
lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.darts_cast line 134
lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.darts_append line 136
lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.darts_reverse line 141
lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.empty_ends line 149
lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.first_origin line 153
lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.last_origin line 157
lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.chain line 165
def OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.letters line 178
lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.letters_mk line 179
lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.letters_reverse line 187
def OAI.TorsionFreeZeroDivisors.WordBlocks.mapCoordinates line 199
lemma OAI.TorsionFreeZeroDivisors.WordBlocks.mapCoordinates_letter line 202
lemma OAI.TorsionFreeZeroDivisors.WordBlocks.rotate_cast line 210
lemma OAI.TorsionFreeZeroDivisors.WordBlocks.mapCoordinates_rotation line 212
structure OAI.TorsionFreeZeroDivisors.WordBlocks.LiftedMatching line 223
Source documentation
Actual boundary occurrences are graph darts; only their labels are inverse matched. In particular, this does not silently require equal graph lifts.
```
structure LiftedMatching (inv : A→A) (ws : List (List D)) where
…
```
def OAI.TorsionFreeZeroDivisors.WordBlocks.Matching.lift line 229
lemma OAI.TorsionFreeZeroDivisors.MapDeletion.genusZero_iff_delete line 254
def OAI.TorsionFreeZeroDivisors.MarkerInsertion.rotation line 284
Source documentation
Insert an unpaired marker immediately before p.
```
def rotation : Equiv.Perm (Option O) := Equiv.swap none (some p)*Equiv.optionCongr σ
```
def OAI.TorsionFreeZeroDivisors.MarkerInsertion.partner line 285
lemma OAI.TorsionFreeZeroDivisors.MarkerInsertion.rotation_none line 286
lemma OAI.TorsionFreeZeroDivisors.MarkerInsertion.partner_none line 287
lemma OAI.TorsionFreeZeroDivisors.MarkerInsertion.rotation_some line 288
lemma OAI.TorsionFreeZeroDivisors.MarkerInsertion.rotation_predecessor line 291
lemma OAI.TorsionFreeZeroDivisors.MarkerInsertion.rotation_nonfixed line 293
lemma OAI.TorsionFreeZeroDivisors.MarkerInsertion.partner_involutive line 294
lemma OAI.TorsionFreeZeroDivisors.MarkerInsertion.fixed_only line 299
def OAI.TorsionFreeZeroDivisors.MarkerInsertion.coordinates line 303
lemma OAI.TorsionFreeZeroDivisors.MarkerInsertion.boundary_commutes line 309
lemma OAI.TorsionFreeZeroDivisors.MarkerInsertion.partner_commutes line 315
lemma OAI.TorsionFreeZeroDivisors.MarkerInsertion.boundary_conjugate line 316
lemma OAI.TorsionFreeZeroDivisors.MarkerInsertion.partner_conjugate line 323
theorem OAI.TorsionFreeZeroDivisors.MarkerInsertion.genusZero line 331
Source documentation
The literal marked rotation retains the exact genus-zero certificate. This is only finite permutation insertion, not a surface realization.
```
theorem genusZero (hz : MapEuler.GenusZero σ α) : MapEuler.GenusZero (rotation σ p) (partner α) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero, OAI.TorsionFreeZeroDivisors.MarkerInsertion.rotation, OAI.TorsionFreeZeroDivisors.MarkerInsertion.partner
def OAI.TorsionFreeZeroDivisors.FinitePicture.ofBoundary line 353
Source documentation
Insert the literal root break in a lifted genus-zero full matching. This retains every graph dart and all endpoints; no graph path is replaced by its rose label. The initial existence of this full matching must still be proved.
```
def ofBoundary : Data (O:=Option O) Γ label inv x y where
…
```
Mentions: OAI.TorsionFreeZeroDivisors.FinitePicture.Data