English
If the reflector preserves binary products, then the corresponding exponential ideal i is closed under binary products, i.e., it is an exponential ideal.
Русский
Если рефлектор сохраняет двоичные произведения, то соответствующий экспоненциальный идеал i замкнут по двоичным произведениям.
LaTeX
$$$ \\text{ExponentialIdeal } i $$$
Lean4
/-- If the reflector preserves binary products, the subcategory is an exponential ideal.
This is the converse of `preservesBinaryProductsOfExponentialIdeal`.
-/
instance (priority := 10) exponentialIdeal_of_preservesBinaryProducts
[Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)] : ExponentialIdeal i :=
by
let ir := reflectorAdjunction i
let L : C ⥤ D := reflector i
let η : 𝟭 C ⟶ L ⋙ i := ir.unit
let ε : i ⋙ L ⟶ 𝟭 D := ir.counit
apply ExponentialIdeal.mk'
intro B A
let q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
by
apply CartesianClosed.curry (ir.homEquiv _ _ _)
apply _ ≫ (ir.homEquiv _ _).symm ((exp.ev A).app (i.obj B))
exact prodComparison L A _ ≫ (_ ◁ (ε.app _)) ≫ inv (prodComparison _ _ _)
have : η.app (A ⟹ i.obj B) ≫ q = 𝟙 (A ⟹ i.obj B) := by
dsimp
rw [← curry_natural_left, curry_eq_iff, uncurry_id_eq_ev, ← ir.homEquiv_naturality_left, ir.homEquiv_apply_eq,
assoc, assoc, prodComparison_natural_whiskerLeft_assoc, ← whiskerLeft_comp_assoc, ir.left_triangle_components,
whiskerLeft_id, id_comp]
apply IsIso.hom_inv_id_assoc
haveI : IsSplitMono (η.app (A ⟹ i.obj B)) := IsSplitMono.mk' ⟨_, this⟩
apply mem_essImage_of_unit_isSplitMono
