mk_of_iso — Mathlib

English

If there is a natural isomorphism i ⋙ exp A ⋙ leftAdjoint i ⋙ i ≅ i ⋙ exp A, then i is an exponential ideal.

Русский

Если существует естественная изоморфность i ⋙ exp A ⋙ leftAdjoint i ⋙ i ≅ i ⋙ exp A, тогда i является экспоненциальным идеалом.

LaTeX

$$$ \\forall A, i \\circ \\mathrm{exp}(A) \\circ \\mathrm{leftAdjoint} (i) \\circ i \\cong i \\circ \\mathrm{exp}(A) \\Rightarrow \\mathrm{ExponentialIdeal} i $$$

Lean4

/-- Given a natural isomorphism `i ⋙ exp A ⋙ leftAdjoint i ⋙ i ≅ i ⋙ exp A`, we can show `i`
is an exponential ideal.
-/
theorem mk_of_iso [Reflective i] (h : ∀ A : C, i ⋙ exp A ⋙ reflector i ⋙ i ≅ i ⋙ exp A) : ExponentialIdeal i :=
  by
  apply ExponentialIdeal.mk'
  intro B A
  exact ⟨_, ⟨(h A).app B⟩⟩

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