OAI/Algebra/Finitistic/Selected/SelectedBarBimodule.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.SelectedBarBimodule.comparisonX line 11

    Source documentation

    The action presentation of X used by the generic native/bar comparison.

    abbrev comparisonX := BimoduleBarComparison.Actions ℂ D SelectedOrdinaryResolution.target

    Mentions: OAI.LittleFinitistic.BimoduleBarComparison.Actions, OAI.LittleFinitistic.SelectedOrdinaryResolution.target

  2. def OAI.LittleFinitistic.SelectedBarBimodule.rightEquiv line 14

    Source documentation

    Recover exactly the original right action of the constructed ordinary X.

    def rightEquiv : comparisonX ≃ₗ[Dᵐᵒᵖ] X :=
…

    Mentions: OAI.LittleFinitistic.SelectedBarBimodule.comparisonX

  3. theorem OAI.LittleFinitistic.SelectedBarBimodule.left_action line 18

    Source documentation

    The same identification preserves the original outside left D-action.

    theorem left_action (d : D) (x : comparisonX) : rightEquiv (d • x) = d • rightEquiv x :=
…

    Mentions: OAI.LittleFinitistic.SelectedBarBimodule.comparisonX, OAI.LittleFinitistic.SelectedBarBimodule.rightEquiv

  4. def OAI.LittleFinitistic.SelectedBarBimodule.leftEquiv line 21
  5. theorem OAI.LittleFinitistic.SelectedBarBimodule.right_action line 29