OrdinaryRightProjective.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.OrdinarySimulation.finitePi_projective line 11

Source documentation

The finite direct sum of actual projective terms is projective.

theorem finitePi_projective {R : Type u} [Ring R] {ι : Type v} [Fintype ι]
    (V : ι → Type w) [∀ i, AddCommGroup (V i)] [∀ i, Module R (V i)]
    [∀ i, Module.Projective R (V i)] : Module.Projective R (∀ i, V i) :=
…

abbrev OAI.LittleFinitistic.OrdinarySimulation.underlyingRightComplex line 20
Source documentation
The actual underlying right-B complex of the genuine dg bimodule.
```
abbrev underlyingRightComplex (P : CochainComplex (ModuleCat.{u} (Enveloping k B)) ℤ) :
    CochainComplex (ModuleCat.{u} Bᵐᵒᵖ) ℤ :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.Enveloping
theorem OAI.LittleFinitistic.OrdinarySimulation.ordinaryO_right_projective line 25