Commit 2023-05-06 21:28 75810309

View on Github →

feat(order/category): Free functor Lat ⥤ BddLat (#18949) Construct the free functor from the category of lattices to the category of bounded lattices. Concretely, it adds a bottom and a top element.

Estimated changes

Modified src/order/category/BddLat.lean

added def Lat_to_BddLat

added def Lat_to_BddLat_comp_dual_iso_dual_comp_Lat_to_BddLat

added def Lat_to_BddLat_forget_adjunction

Modified src/order/hom/lattice.lean

added def inf_hom.with_bot'

added theorem inf_hom.with_bot_comp

added theorem inf_hom.with_bot_id

added def inf_hom.with_top'

added theorem inf_hom.with_top_comp

added theorem inf_hom.with_top_id

added def lattice_hom.with_bot'

added theorem lattice_hom.with_bot_comp

added theorem lattice_hom.with_bot_id

added def lattice_hom.with_top'

added theorem lattice_hom.with_top_comp

added theorem lattice_hom.with_top_id

added def lattice_hom.with_top_with_bot'

added def lattice_hom.with_top_with_bot

added theorem lattice_hom.with_top_with_bot_comp

added theorem lattice_hom.with_top_with_bot_id

added def sup_hom.with_bot'

added theorem sup_hom.with_bot_comp

added theorem sup_hom.with_bot_id

added def sup_hom.with_top'

added theorem sup_hom.with_top_comp

added theorem sup_hom.with_top_id