inf — Mathlib

Lean4
/-- When `[HasPullbacks C]`, `MonoOver A` has "intersections", functorial in both arguments.

As `MonoOver A` is only a preorder, this doesn't satisfy the axioms of `SemilatticeInf`,
but we reuse all the names from `SemilatticeInf` because they will be used to construct
`SemilatticeInf (subobject A)` shortly.
-/
@[simps]
def inf {A : C} : MonoOver A ⥤ MonoOver A ⥤ MonoOver A
    where
  obj f := pullback f.arrow ⋙ map f.arrow
  map
    k :=
    {
      app := fun g => by
        apply homMk _ _
        · apply pullback.lift (pullback.fst _ _) (pullback.snd _ _ ≫ k.left) _
          rw [pullback.condition, assoc, w k]
        dsimp
        rw [pullback.lift_snd_assoc, assoc, w k] }
Похожие утверждения