mk' — Mathlib

English

To show that i is an exponential ideal it suffices to exhibit that for all B ∈ D and A ∈ C, the object A ⟹ i.obj B lies in the essential image of i.

Русский

Чтобы показать, что i является экспоненциальным идеалом, достаточно показать, что для любых B ∈ D и A ∈ C, объект A ⟹ i.obj B принадлежит к образу i.

LaTeX

$$$ \\forall B \\in D, A \\in C,\\ i.essImage (A \\Rightarrow i.obj B) $$$

Lean4

/-- To show `i` is an exponential ideal it suffices to show that `A ⟹ iB` is "in" `D` for any `A` in
`C` and `B` in `D`.
-/
theorem mk' (h : ∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)) : ExponentialIdeal i :=
  ⟨fun hB A => by
    rcases hB with ⟨B', ⟨iB'⟩⟩
    exact Functor.essImage.ofIso ((exp A).mapIso iB') (h B' A)⟩

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