OAI/RepresentationTheory/RestrictedTilting/SmallGroupTrace.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiberFunctorProof.SmallGroupTrace.freeNormRepresentative line 15
2. lemma OAI.FiberFunctorProof.SmallGroupTrace.freeNormRepresentative_apply line 22
3. lemma OAI.FiberFunctorProof.SmallGroupTrace.free_action_apply line 26
4. lemma OAI.FiberFunctorProof.SmallGroupTrace.free_relativeTrace line 44
5. def OAI.FiberFunctorProof.SmallGroupTrace.finiteIntertwiner line 60
6. lemma OAI.FiberFunctorProof.SmallGroupTrace.finiteIntertwiner_hom line 64
7. lemma OAI.FiberFunctorProof.SmallGroupTrace.finiteIntertwiner_epi line 68
8. lemma OAI.FiberFunctorProof.SmallGroupTrace.fdrep_free_projective line 76
9. def OAI.FiberFunctorProof.SmallGroupTrace.finiteFreeCover line 84
10. lemma OAI.FiberFunctorProof.SmallGroupTrace.finiteFreeCover_epi line 89
11. def OAI.FiberFunctorProof.SmallGroupTrace.coordinateTraceLift line 110
12. lemma OAI.FiberFunctorProof.SmallGroupTrace.coordinateTraceLift_apply line 116
13. def OAI.FiberFunctorProof.SmallGroupTrace.coordinateTraceHom line 122
14. lemma OAI.FiberFunctorProof.SmallGroupTrace.freeCover_traceLift line 135
15. def OAI.FiberFunctorProof.SmallGroupTrace.finiteTraceBasis line 149
16. theorem OAI.FiberFunctorProof.SmallGroupTrace.relativeTrace_factors line 154
17. def OAI.FiberFunctorProof.SmallGroupTrace.underlyingIntertwiner line 166
18. theorem OAI.FiberFunctorProof.SmallGroupTrace.relativeTrace_of_factors line 172
19. theorem OAI.FiberFunctorProof.SmallGroupTrace.projective_factor_iff_relativeTrace line 187