OAI/RepresentationTheory/RestrictedTilting/TraceFactor.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiberFunctorProof.coordinateTraceLift line 13
2. lemma OAI.FiberFunctorProof.coordinateTraceLift_apply line 19
3. def OAI.FiberFunctorProof.coordinateTraceHom line 25
4. lemma OAI.FiberFunctorProof.freeCover_traceLift line 38
5. def OAI.FiberFunctorProof.finiteTraceBasis line 52
6. theorem OAI.FiberFunctorProof.relativeTrace_factors line 57
7. def OAI.FiberFunctorProof.underlyingIntertwiner line 69
8. theorem OAI.FiberFunctorProof.relativeTrace_of_factors line 75
9. theorem OAI.FiberFunctorProof.projective_factor_iff_relativeTrace line 90