OAI/RepresentationTheory/RestrictedTilting/TensorLimits.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact tensor functors and rational tensor representations.

  1. theorem OAI.FiberFunctorProof.tensorLeft_preservesFiniteLimits line 18

    Also declared: OAI/RepresentationTheory/RestrictedTilting/TensorExactness.lean:14 (same declaration text).

  2. theorem OAI.FiberFunctorProof.tensorLeft_preservesFiniteColimits line 23

    Also declared: OAI/RepresentationTheory/RestrictedTilting/TensorExactness.lean:19 (same declaration text).

  3. theorem OAI.FiberFunctorProof.tensorRight_preservesFiniteLimits line 28

    Also declared: OAI/RepresentationTheory/RestrictedTilting/TensorExactness.lean:24 (same declaration text).

  4. theorem OAI.FiberFunctorProof.tensorRight_preservesFiniteColimits line 33

    Distinct definitions of this name: OAI/RepresentationTheory/RestrictedTilting/TensorExactness.lean:29 (same statement text; different proof or body). Qualify references as OAI.FiberFunctorProof.tensorRight_preservesFiniteColimits@path.

  5. instance OAI.FiberFunctorProof.fdrepRigid line 44
  6. lemma OAI.FiberFunctorProof.HasGoodFiltration.extension line 48
  7. lemma OAI.FiberFunctorProof.IsRational.tensor line 81
  8. abbrev OAI.FiberFunctorProof.Binary line 115