OAI/Algebra/Finitistic/Selected/SelectedOrdinaryModules.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.SelectedOrdinaryModules.Inflated line 12

    Source documentation

    The source module M(Y), supported on the first D-block and inflated to A.

    def Inflated (Y : S.{0}) := (representation Y).Evaluation
  2. instance OAI.LittleFinitistic.SelectedOrdinaryModules.(instance at line 13) line 13
  3. instance OAI.LittleFinitistic.SelectedOrdinaryModules.(instance at line 15) line 15
  4. instance OAI.LittleFinitistic.SelectedOrdinaryModules.(instance at line 17) line 17
  5. instance OAI.LittleFinitistic.SelectedOrdinaryModules.(instance at line 19) line 19
  6. abbrev OAI.LittleFinitistic.SelectedOrdinaryModules.firstProjection line 22
  7. abbrev OAI.LittleFinitistic.SelectedOrdinaryModules.augmentationRing line 23
  8. instance OAI.LittleFinitistic.SelectedOrdinaryModules.(instance at line 24) line 24
  9. instance OAI.LittleFinitistic.SelectedOrdinaryModules.(instance at line 25) line 25
  10. instance OAI.LittleFinitistic.SelectedOrdinaryModules.(instance at line 27) line 27
  11. instance OAI.LittleFinitistic.SelectedOrdinaryModules.(instance at line 31) line 31
  12. instance OAI.LittleFinitistic.SelectedOrdinaryModules.(instance at line 35) line 35
  13. instance OAI.LittleFinitistic.SelectedOrdinaryModules.(instance at line 38) line 38
  14. abbrev OAI.LittleFinitistic.SelectedOrdinaryModules.module line 41
  15. theorem OAI.LittleFinitistic.SelectedOrdinaryModules.first_action line 44

    Source documentation

    The actual D-action is exactly the original first B-block action.

    theorem first_action (Y : S.{0}) (d : D) (n : Inflated Y) : d • n = d.1 • n := rfl

    Mentions: OAI.LittleFinitistic.SelectedOrdinaryModules.Inflated

  16. theorem OAI.LittleFinitistic.SelectedOrdinaryModules.ideal_annihilates line 46

    Source documentation

    The square-zero ideal acts by zero, as required by the bar calculation.

    theorem ideal_annihilates (Y : S.{0}) (x : X) (n : Inflated Y) :
    (TrivSqZeroExt.inr x : A) • n = 0 := by
…

    Mentions: OAI.LittleFinitistic.SelectedOrdinaryModules.Inflated

  17. theorem OAI.LittleFinitistic.SelectedOrdinaryModules.base_action line 50
  18. theorem OAI.LittleFinitistic.SelectedOrdinaryModules.isZero_iff line 54

    Source documentation

    Inflation preserves exactly the original module's zero criterion.

    theorem isZero_iff (Y : S.{0}) : IsZero (module Y) ↔ Subsingleton Y.val := by
…

    Mentions: OAI.LittleFinitistic.SelectedOrdinaryModules.module

  19. abbrev OAI.LittleFinitistic.SelectedOrdinaryModules.testModule line 62

    Source documentation

    Actual finite-dimensional modules over the one fixed A; their projective dimensions are the remaining homological conclusion.

    abbrev testModule (m : ℕ) [NeZero m] := module (test m)

    Mentions: OAI.LittleFinitistic.SelectedOrdinaryModules.module

  20. theorem OAI.LittleFinitistic.SelectedOrdinaryModules.test_nonzero line 64