instMonoFunctorOppositeTypeHomOfLe

English

For subpresheaves S and T, the object of their maximum at i is the union S.obj i ∪ T.obj i.

Русский

Для подпрешафов S и T, объект их максимума в i равен объединению S.obj i и T.obj i.

LaTeX

$$$(S \\uplus T).obj i = S.obj i \\cup T.obj i$$$

Lean4

instance {G G' : Subpresheaf F} (h : G ≤ G') : Mono (Subpresheaf.homOfLe h) :=
  ⟨fun _ _ e =>
    NatTrans.ext <|
      funext fun U => funext fun x => Subtype.ext <| (congr_arg Subtype.val <| (congr_fun (congr_app e U) x :) :)⟩

Похожие утверждения