Commit 2022-04-29 04:24 ccb9d64b

View on Github →

feat(category_theory/braiding): pull back a braiding along a faithful functor (#13684) I intend to use this to define the braiding/symmetry on Rep k G using the existing braiding/symmetry on Module k.

Estimated changes

Modified src/algebraic_geometry/open_immersion.lean

Modified src/algebraic_geometry/sheafed_space.lean

Modified src/category_theory/equivalence.lean

Modified src/category_theory/functor/fully_faithful.lean

modified theorem category_theory.functor.map_injective

modified theorem category_theory.functor.map_iso_injective

modified def category_theory.functor.preimage

added def category_theory.functor.preimage_iso

added theorem category_theory.functor.preimage_iso_map_iso

deleted def category_theory.preimage_iso

deleted theorem category_theory.preimage_iso_hom

deleted theorem category_theory.preimage_iso_inv

deleted theorem category_theory.preimage_iso_map_iso

Modified src/category_theory/monoidal/braided.lean

added def category_theory.braided_category_of_faithful

added def category_theory.braided_category_of_fully_faithful

added def category_theory.symmetric_category_of_faithful

Modified src/category_theory/subobject/mono_over.lean

Modified src/category_theory/yoneda.lean