Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-24 09:17 c49e89df

View on Github →

feat(category_theory/adjunction): definitions, basic proofs, and examples (#619)

Estimated changes

Created src/category_theory/adjunction.lean

added def category_theory.adjunction.adjunction_of_equiv_left

added def category_theory.adjunction.adjunction_of_equiv_right

added def category_theory.adjunction.cocones_iso

added def category_theory.adjunction.comp

added def category_theory.adjunction.cones_iso

added theorem category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_left

added theorem category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_right_symm

added structure category_theory.adjunction.core_hom_equiv

added structure category_theory.adjunction.core_unit_counit

added def category_theory.adjunction.functoriality_is_left_adjoint

added def category_theory.adjunction.functoriality_is_right_adjoint

added theorem category_theory.adjunction.hom_equiv_naturality_left

added theorem category_theory.adjunction.hom_equiv_naturality_left_symm

added theorem category_theory.adjunction.hom_equiv_naturality_right

added theorem category_theory.adjunction.hom_equiv_naturality_right_symm

added def category_theory.adjunction.id

added structure category_theory.adjunction.is_left_adjoint

added structure category_theory.adjunction.is_right_adjoint

added def category_theory.adjunction.left_adjoint_of_equiv

added def category_theory.adjunction.left_adjoint_preserves_colimits

added theorem category_theory.adjunction.left_triangle

added theorem category_theory.adjunction.left_triangle_components

added def category_theory.adjunction.mk_of_hom_equiv

added def category_theory.adjunction.mk_of_unit_counit

added def category_theory.adjunction.right_adjoint_of_equiv

added def category_theory.adjunction.right_adjoint_preserves_limits

added theorem category_theory.adjunction.right_triangle

added theorem category_theory.adjunction.right_triangle_components

added structure category_theory.adjunction

Modified src/category_theory/category.lean

modified theorem category_theory.bundled_hom_coe

modified theorem category_theory.concrete_category_comp

modified theorem category_theory.concrete_category_id

Modified src/category_theory/examples/monoids.lean

Modified src/category_theory/examples/rings.lean

added def category_theory.examples.CommRing.Int.cast

added def category_theory.examples.CommRing.Int.hom_unique

added def category_theory.examples.CommRing.Int

added theorem category_theory.examples.CommRing.comp_val

added def category_theory.examples.CommRing.forget

modified def category_theory.examples.CommRing.forget_to_CommMon

added theorem category_theory.examples.CommRing.hom_coe_app

added theorem category_theory.examples.CommRing.id_val

added def category_theory.examples.CommRing.int.eq_cast'

added theorem category_theory.examples.CommRing.polynomial_map_val

added theorem category_theory.examples.CommRing.polynomial_obj_α

added def category_theory.examples.CommRing.to_Ring

deleted theorem category_theory.examples.CommRing_hom_coe_app

Modified src/category_theory/examples/topological_spaces.lean

added def category_theory.examples.Top.adj₁

added def category_theory.examples.Top.adj₂

added def category_theory.examples.Top.discrete

added def category_theory.examples.Top.trivial

Modified src/category_theory/fully_faithful.lean

Modified src/category_theory/limits/cones.lean

added theorem category_theory.functor.cocones_map_app

added theorem category_theory.functor.cones_map_app

deleted def category_theory.limits.cocone.precompose

added def category_theory.limits.cocones.precompose

added theorem category_theory.limits.cocones.precompose_map_hom

added theorem category_theory.limits.cocones.precompose_obj_X

added theorem category_theory.limits.cocones.precompose_obj_ι

deleted def category_theory.limits.cone.postcompose

added def category_theory.limits.cones.postcompose

added theorem category_theory.limits.cones.postcompose_map_hom

added theorem category_theory.limits.cones.postcompose_obj_X

added theorem category_theory.limits.cones.postcompose_obj_π

Modified src/category_theory/limits/limits.lean

added def category_theory.limits.is_colimit_iso_unique_cocone_morphism

added def category_theory.limits.is_limit_iso_unique_cone_morphism

Modified src/data/equiv/basic.lean

modified def equiv.unique_of_equiv