OAI/Algebra/Finitistic/Ordinary/OrdinarySupportedExtension.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.OrdinarySimulation.SupportedExtension.component line 14

    Source documentation

    The supported complex's restriction and extension have its actual components.

    def component (j : J) : (K.stupidTrunc e).X j ≅ K.X j :=
…
  2. theorem OAI.LittleFinitistic.OrdinarySimulation.SupportedExtension.component_iso_unique line 20
  3. theorem OAI.LittleFinitistic.OrdinarySimulation.SupportedExtension.component_at line 26
  4. def OAI.LittleFinitistic.OrdinarySimulation.SupportedExtension.iso line 32

    Source documentation

    An actual chain isomorphism, with support supplied by proved zero objects.

    def iso : K.stupidTrunc e ≅ K :=
…