Hurwitz.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.reorderBoundary line 16
Source documentation
Only the ordered boundary enumeration is changed. Every side, corner, seam, genus and facet remains the old one.
```
def reorderBoundary (σ : ∀ f,Equiv.Perm (Fin (D.boundaryCount f))) : Diagram F S V arity where
…
```
Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram

def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.reorderGenerators line 33

Source documentation

This producer merely transfers the identical named matrix coordinates; the noncommutative re- framing is performed before this transfer.

def reorderGenerators (σ : ∀ f,Equiv.Perm (Fin (D.boundaryCount f)))
    (g : (e : D.Generator) → (Matrix (Fin (D.generatorRank e)) (Fin (D.generatorRank e)) R)ˣ) :
    (e : (D.reorderBoundary σ).Generator) →
      (Matrix (Fin ((D.reorderBoundary σ).generatorRank e))
        (Fin ((D.reorderBoundary σ).generatorRank e)) R)ˣ
  | .side a => g (.side a)
  | .frame s b => g (.frame s b)
  | .handle f k b => g (.handle f k b)

Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.Generator, OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.generatorRank

lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.reorder_vertexComparison line 42
def OAI.IntegralCharacterVarieties.SurfaceSurgery.Hurwitz.negative line 53
def OAI.IntegralCharacterVarieties.SurfaceSurgery.Hurwitz.positive line 56
lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.Hurwitz.positive_negative line 60
lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.Hurwitz.negative_positive line 70
def OAI.IntegralCharacterVarieties.SurfaceSurgery.Hurwitz.swapAutomorphism line 81
Source documentation
The elementary Hurwitz automorphism fixes every other free generator.
```
def swapAutomorphism (a b : I) (hab : a≠b) : FreeGroup I ≃* FreeGroup I where
…
```
lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.Hurwitz.swapAutomorphism_of line 88
structure OAI.IntegralCharacterVarieties.SurfaceSurgery.Hurwitz.BasedPermutation line 95
Source documentation
A finite boundary enumeration change together with an invertible word substitution. Product preservation is NOT the only stored certificate.
```
structure BasedPermutation (l m : List I) where
…
```
theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.Hurwitz.basedPermutation_exists line 103
Source documentation
Obtained solely from the permutation of distinct circle labels.
```
theorem basedPermutation_exists {l m : List I} (hp : l.Perm m) (hn : l.Nodup) :
    Nonempty (BasedPermutation l m) := by
…
```
Mentions: OAI.IntegralCharacterVarieties.SurfaceSurgery.Hurwitz.BasedPermutation
def OAI.IntegralCharacterVarieties.SurfaceSurgery.Hurwitz.change line 161
Source documentation
Precomposition by the free-group automorphism, with its inverse. This works for full-ring matrix groups, not only for complex points.
```
def change (e : FreeGroup I ≃* FreeGroup I) (f : I → H) : I → H :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.Hurwitz.lift_change line 164
def OAI.IntegralCharacterVarieties.SurfaceSurgery.Hurwitz.evaluationEquiv line 171
lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.Hurwitz.BasedPermutation.generator_eval line 185
lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.Hurwitz.BasedPermutation.product_eval line 191
lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.Hurwitz.BasedPermutation.inverse_generator line 198
lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.Hurwitz.inverse_evaluation_path line 205
def OAI.IntegralCharacterVarieties.SurfaceSurgery.Hurwitz.finPresentation line 212
Source documentation
A fixed presentation automorphism for each finite boundary permutation.
```
def finPresentation {n : ℕ} (σ : Equiv.Perm (Fin n)) :
    BasedPermutation (List.ofFn (fun i : Fin n => i)) (List.ofFn σ) := by
…
```
Mentions: OAI.IntegralCharacterVarieties.SurfaceSurgery.Hurwitz.BasedPermutation
lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.Hurwitz.finPresentation_spec line 223