OAI/Geometry/HyperbolicGroups/StarFiber.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PinnedAssignments.extend_restrict line 18
2. def OAI.HyperbolicObstruction.PinnedAssignments.fiberEquiv line 27

   Source documentation

   No incidence or probabilistic assumption is hidden in the pinned-fiber bijection: free assignments extend uniquely, with the original fieldwise rule.

   def fiberEquiv (tag : W → F) (P : Finset W) (ξ : W → A) (H : (W → A) → Prop) :
       {σ : W → A // Fieldwise tag σ ∧ (∀ v ∈ P, σ v = ξ v) ∧ H σ} ≃
         {τ : Free P → A // τ ∈ candidates tag P ξ ∧ H (extend P ξ τ)} where
   …

   Mentions: OAI.HyperbolicObstruction.PinnedAssignments.Fieldwise, OAI.HyperbolicObstruction.PinnedAssignments.Free, OAI.HyperbolicObstruction.PinnedAssignments.candidates, OAI.HyperbolicObstruction.PinnedAssignments.extend

3. lemma OAI.HyperbolicObstruction.StarModel.branch_eq_iff line 51
4. lemma OAI.HyperbolicObstruction.StarModel.fixed_branch_present line 62
5. abbrev OAI.HyperbolicObstruction.StarModel.Stars line 101
6. abbrev OAI.HyperbolicObstruction.StarModel.Matches line 105
7. instance OAI.HyperbolicObstruction.StarModel.(instance at line 108) line 108
8. instance OAI.HyperbolicObstruction.StarModel.(instance at line 114) line 114
9. def OAI.HyperbolicObstruction.StarModel.starBranch line 118
10. def OAI.HyperbolicObstruction.StarModel.branchValues line 122
11. lemma OAI.HyperbolicObstruction.StarModel.branchValues_coord line 125
12. theorem OAI.HyperbolicObstruction.StarModel.card_branch_fiber line 131

    Source documentation

    The fixed-match extension statistic is exactly the size of the branch fiber of actual, present, fieldwise-injective stars.

    theorem card_branch_fiber (support : R → Finset F) (U : Finset F)
        (w : TableModel.Entry (A := A) support → Bool) (j₀ : B) (σ : Matches support w) :
    …

    Mentions: OAI.HyperbolicObstruction.TableModel.Entry, OAI.HyperbolicObstruction.StarModel.Matches