OAI/RingTheory/DirectFiniteness/RibbonRestriction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.Planar.restrictQuotient line 15
2. lemma OAI.KaplanskyCounterexample.Planar.restrictQuotient_injective line 19
3. def OAI.KaplanskyCounterexample.Planar.quotientRestrictSumEquiv line 32

   Source documentation

   Components of an invariant subset and of its complement partition the components of the original finite set.

   def quotientRestrictSumEquiv (s : Setoid α) (P : α → Prop)
       (hP : ∀ {x y}, s.r x y → (P x ↔ P y)) :
       (Quotient (s.comap (Subtype.val : {x // P x} → α)) ⊕
         Quotient (s.comap (Subtype.val : {x // ¬ P x} → α))) ≃ Quotient s :=
   …

4. lemma OAI.KaplanskyCounterexample.Planar.quotient_restrict_card_split line 59
5. lemma OAI.KaplanskyCounterexample.Planar.perm_invariant_cycle line 68
6. lemma OAI.KaplanskyCounterexample.Planar.subtype_cycles_setoid line 74
7. lemma OAI.KaplanskyCounterexample.Planar.cycles_restrict_card_split line 80
8. def OAI.KaplanskyCounterexample.Planar.Ribbon.restrict line 88

   Source documentation

   Restrict a ribbon to a union of its connected components.

   def Ribbon.restrict (R : Ribbon α) (P : α → Prop)
       (hb : ∀ x, P (R.black x) ↔ P x) (hw : ∀ x, P (R.white x) ↔ P x) :
       Ribbon {x // P x} where
   …

   Mentions: OAI.KaplanskyCounterexample.Planar.Ribbon

9. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.restrict_face line 95
10. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.invariant_components line 98
11. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.restrict_components line 107
12. def OAI.KaplanskyCounterexample.Planar.Ribbon.GenusZero line 143

    Source documentation

    Euler equality componentwise, i.e., genus zero for all components.

    def Ribbon.GenusZero (R : Ribbon α) : Prop :=
    …

    Mentions: OAI.KaplanskyCounterexample.Planar.Ribbon

13. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.planar_restrict line 147