BarBimoduleCongruence.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.BimoduleTensor.leftMap_relations line 21
def OAI.DerivedBar.BimoduleTensor.leftMap line 31
Source documentation
The actual left-factor map on the bar's balanced quotient.
```
def leftMap : tensor k D X V →ₗ[D] tensor k D Y V :=
…
```
Mentions: OAI.DerivedBar.BimoduleTensor.tensor
theorem OAI.DerivedBar.BimoduleTensor.leftMap_quotient line 38
theorem OAI.DerivedBar.BimoduleTensor.symm_right line 44
def OAI.DerivedBar.BimoduleTensor.congrLeft line 49
Source documentation
A genuine bimodule equivalence induces an equivalence of the actual balanced tensors.
```
def congrLeft : tensor k D X V ≃ₗ[D] tensor k D Y V :=
…
```
Mentions: OAI.DerivedBar.BimoduleTensor.tensor
def OAI.DerivedBar.BimoduleTensor.tensorFunctorCongr line 70
Source documentation
Naturality in every input module retains the exterior D-action.
```
def tensorFunctorCongr : tensorFunctor k D X ≅ tensorFunctor k D Y :=
…
```
Mentions: OAI.DerivedBar.BimoduleTensor.tensorFunctor
def OAI.DerivedBar.BimoduleTensor.derivedTensorCongr line 80
Source documentation
The same actual tensor equivalence descends to the genuine bar-derived functor.
```
def derivedTensorCongr : derivedTensor k D X ≅ derivedTensor k D Y :=
…
```
Mentions: OAI.DerivedBar.derivedTensor

def OAI.DerivedBar.BimoduleTensor.derivedIterateCongr line 88

Source documentation

All finite genuine iterations are compatible with the original bimodule equivalence.

def derivedIterateCongr : (r : ℕ) → derivedTensorIterate k D X r ≅ derivedTensorIterate k D Y r
  | 0 => Iso.refl _
  | r+1 => isoWhiskerRight (derivedIterateCongr r) (derivedTensor k D X) ≪≫
      isoWhiskerLeft (derivedTensorIterate k D Y r) (derivedTensorCongr k D e he)
end DerivedBar.BimoduleTensor

end

end OAI

Mentions: OAI.DerivedBar.derivedTensorIterate, OAI.DerivedBar.derivedTensor, OAI.DerivedBar.BimoduleTensor.derivedTensorCongr