OAI/GroupTheory/PolycyclicRecognition/Algebra/SmallCoefficientTensorAlgebra.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PolycyclicRecognition.smallCoefficientTensor line 15
2. def OAI.PolycyclicRecognition.smallCoefficientTensorUnit line 18
3. theorem OAI.PolycyclicRecognition.smallCoefficientTensorUnit_apply line 27
4. theorem OAI.PolycyclicRecognition.smallCoefficientTensorUnit_natural line 30
5. def OAI.PolycyclicRecognition.smallCoefficientMultiplication line 39
6. def OAI.PolycyclicRecognition.smallCoefficientTensorMultiply line 48
7. theorem OAI.PolycyclicRecognition.smallCoefficientTensorMultiply_apply line 54
8. theorem OAI.PolycyclicRecognition.smallCoefficientTensorMultiply_unit line 59
9. theorem OAI.PolycyclicRecognition.smallCoefficientTensorMultiply_map_unit line 69
10. theorem OAI.PolycyclicRecognition.smallCoefficientTensorMultiply_natural line 79
11. theorem OAI.PolycyclicRecognition.smallCoefficientTensor_split_of_unit_homotopy line 95

    Source documentation

    Extend a primitive using ring multiplication and cancel its epimorphic cover.

    theorem smallCoefficientTensor_split_of_unit_homotopy {P Q K : Rep.{0} ℤ G}
        (π : Q ⟶ K) [Epi π] (ι : K ⟶ P) (r : P ⟶ smallCoefficientTensor K)
        (hr : (π ≫ ι) ≫ r = π ≫ smallCoefficientTensorUnit K) :
        (tensorLeft (smallCoefficientRepresentation G)).map ι ≫
          ((tensorLeft (smallCoefficientRepresentation G)).map r ≫
            smallCoefficientTensorMultiply K) = 𝟙 _ := by
    …

    Mentions: OAI.PolycyclicRecognition.smallCoefficientTensor, OAI.PolycyclicRecognition.smallCoefficientTensorUnit, OAI.PolycyclicRecognition.smallCoefficientRepresentation, OAI.PolycyclicRecognition.smallCoefficientTensorMultiply