OAI/Algebra/Finitistic/Selected/SelectedChainAction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LittleFinitistic.SelectedChainAction.HAction_one line 13
2. lemma OAI.LittleFinitistic.SelectedChainAction.HAction_val line 22

   Source documentation

   In the underlying Y, the selected action is exactly restriction of alpha(r).

   lemma HAction_val (r : SelectionRing) (x : H (Y := Y)) :
   …

   Mentions: OAI.LittleFinitistic.SelectionRing

3. lemma OAI.LittleFinitistic.SelectedChainAction.distinguished01 line 29
4. lemma OAI.LittleFinitistic.SelectedChainAction.distinguished12 line 35
5. lemma OAI.LittleFinitistic.SelectedChainAction.arrow01_val line 43

   Source documentation

   Every actual first arrow, on every homology class in either selected degree.

   lemma arrow01_val (a : Fin (encoding.generators+1))
       (f : UnderlyingRepresentatives.complex P fixed.D0 ⟶ UnderlyingRepresentatives.complex P fixed.D1)
       (hf : (HomotopyCategory.quotient _ _).map f = (SourceModelBridge.ambient P).map (fixed.f a))
       (n : ℤ) (hn : n = 0 ∨ n = -3) (x : (complex (Y := Y) fixed.D0).homology n) :
   …

   Mentions: OAI.LittleFinitistic.UnderlyingRepresentatives.complex, OAI.LittleFinitistic.SourceModelBridge.ambient

6. lemma OAI.LittleFinitistic.SelectedChainAction.arrow12_val line 58