OAI/RepresentationTheory/RestrictedTilting/TensorExactness.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiberFunctorProof.tensorLeft_preservesFiniteLimits line 14

    Also declared: OAI/RepresentationTheory/RestrictedTilting/TensorLimits.lean:18 (same declaration text).

  2. theorem OAI.FiberFunctorProof.tensorLeft_preservesFiniteColimits line 19

    Also declared: OAI/RepresentationTheory/RestrictedTilting/TensorLimits.lean:23 (same declaration text).

  3. theorem OAI.FiberFunctorProof.tensorRight_preservesFiniteLimits line 24

    Also declared: OAI/RepresentationTheory/RestrictedTilting/TensorLimits.lean:28 (same declaration text).

  4. theorem OAI.FiberFunctorProof.tensorRight_preservesFiniteColimits line 29

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

  5. lemma OAI.FiberFunctorProof.coevaluation_ne_zero line 36
  6. lemma OAI.FiberFunctorProof.tensorRight_faithful line 46
  7. lemma OAI.FiberFunctorProof.coevaluation_ne_zero_right line 59
  8. lemma OAI.FiberFunctorProof.tensorLeft_faithful line 69
  9. lemma OAI.FiberFunctorProof.projective_tensor line 83
  10. theorem OAI.FiberFunctorProof.exact_of_nonzero_projective line 90