feat: port CategoryTheory.Closed.Ideal (#4951)

Co-authored-by: Alex J Best <alex.j.best@gmail.com>

Mathlib.lean

@@ -825,6 +825,7 @@ import Mathlib.CategoryTheory.Category.ULift
 import Mathlib.CategoryTheory.Closed.Cartesian
 import Mathlib.CategoryTheory.Closed.Functor
 import Mathlib.CategoryTheory.Closed.FunctorCategory
+import Mathlib.CategoryTheory.Closed.Ideal
 import Mathlib.CategoryTheory.Closed.Monoidal
 import Mathlib.CategoryTheory.Closed.Types
 import Mathlib.CategoryTheory.Closed.Zero

Mathlib/CategoryTheory/Closed/Ideal.lean

@@ -0,0 +1,281 @@
+/-
+Copyright (c) 2021 Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta
+
+! This file was ported from Lean 3 source module category_theory.closed.ideal
+! leanprover-community/mathlib commit ac3ae212f394f508df43e37aa093722fa9b65d31
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
+import Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
+import Mathlib.CategoryTheory.Monad.Limits
+import Mathlib.CategoryTheory.Adjunction.FullyFaithful
+import Mathlib.CategoryTheory.Adjunction.Reflective
+import Mathlib.CategoryTheory.Closed.Cartesian
+import Mathlib.CategoryTheory.Subterminal
+
+/-!
+# Exponential ideals
+
+An exponential ideal of a cartesian closed category `C` is a subcategory `D ⊆ C` such that for any
+`B : D` and `A : C`, the exponential `A ⟹ B` is in `D`: resembling ring theoretic ideals. We
+define the notion here for inclusion functors `i : D ⥤ C` rather than explicit subcategories to
+preserve the principle of equivalence.
+
+We additionally show that if `C` is cartesian closed and `i : D ⥤ C` is a reflective functor, the
+following are equivalent.
+* The left adjoint to `i` preserves binary (equivalently, finite) products.
+* `i` is an exponential ideal.
+-/
+
+
+universe v₁ v₂ u₁ u₂
+
+noncomputable section
+
+namespace CategoryTheory
+
+open Limits Category
+
+section Ideal
+
+variable {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₁} D] {i : D ⥤ C}
+
+variable (i) [HasFiniteProducts C] [CartesianClosed C]
+
+/-- The subcategory `D` of `C` expressed as an inclusion functor is an *exponential ideal* if
+`B ∈ D` implies `A ⟹ B ∈ D` for all `A`.
+-/
+class ExponentialIdeal : Prop where
+  exp_closed : ∀ {B}, B ∈ i.essImage → ∀ A, (A ⟹ B) ∈ i.essImage
+#align category_theory.exponential_ideal CategoryTheory.ExponentialIdeal
+attribute [nolint docBlame] ExponentialIdeal.exp_closed
+
+/-- 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 ExponentialIdeal.mk' (h : ∀ (B : D) (A : C), (A ⟹ i.obj B) ∈ i.essImage) :
+    ExponentialIdeal i :=
+  ⟨fun hB A => by
+    rcases hB with ⟨B', ⟨iB'⟩⟩
+    exact Functor.essImage.ofIso ((exp A).mapIso iB') (h B' A)⟩
+#align category_theory.exponential_ideal.mk' CategoryTheory.ExponentialIdeal.mk'
+
+/-- The entire category viewed as a subcategory is an exponential ideal. -/
+instance : ExponentialIdeal (𝟭 C) :=
+  ExponentialIdeal.mk' _ fun _ _ => ⟨_, ⟨Iso.refl _⟩⟩
+
+open CartesianClosed
+
+/-- The subcategory of subterminal objects is an exponential ideal. -/
+instance : ExponentialIdeal (subterminalInclusion C) := by
+  apply ExponentialIdeal.mk'
+  intro B A
+  refine' ⟨⟨A ⟹ B.1, fun Z g h => _⟩, ⟨Iso.refl _⟩⟩
+  exact uncurry_injective (B.2 (CartesianClosed.uncurry g) (CartesianClosed.uncurry h))
+
+/-- If `D` is a reflective subcategory, the property of being an exponential ideal is equivalent to
+the presence of a natural isomorphism `i ⋙ exp A ⋙ leftAdjoint i ⋙ i ≅ i ⋙ exp A`, that is:
+`(A ⟹ iB) ≅ i L (A ⟹ iB)`, naturally in `B`.
+The converse is given in `ExponentialIdeal.mk_of_iso`.
+-/
+def exponentialIdealReflective (A : C) [Reflective i] [ExponentialIdeal i] :
+    i ⋙ exp A ⋙ leftAdjoint i ⋙ i ≅ i ⋙ exp A := by
+  symm
+  apply NatIso.ofComponents _ _
+  · intro X
+    haveI := Functor.essImage.unit_isIso (ExponentialIdeal.exp_closed (i.obj_mem_essImage X) A)
+    apply asIso ((Adjunction.ofRightAdjoint i).unit.app (A ⟹ i.obj X))
+  · simp [asIso]
+#align category_theory.exponential_ideal_reflective CategoryTheory.exponentialIdealReflective
+
+/-- Given a natural isomorphism `i ⋙ exp A ⋙ leftAdjoint i ⋙ i ≅ i ⋙ exp A`, we can show `i`
+is an exponential ideal.
+-/
+theorem ExponentialIdeal.mk_of_iso [Reflective i]
+    (h : ∀ A : C, i ⋙ exp A ⋙ leftAdjoint i ⋙ i ≅ i ⋙ exp A) : ExponentialIdeal i := by
+  apply ExponentialIdeal.mk'
+  intro B A
+  exact ⟨_, ⟨(h A).app B⟩⟩
+#align category_theory.exponential_ideal.mk_of_iso CategoryTheory.ExponentialIdeal.mk_of_iso
+
+end Ideal
+
+section
+
+variable {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₁} D]
+
+variable (i : D ⥤ C)
+
+-- Porting note: this used to be used as a local instance,
+-- now it can instead be used as a have when needed
+-- we assume HasFiniteProducts D as a hypothesis below
+theorem reflective_products [HasFiniteProducts C] [Reflective i] : HasFiniteProducts D :=
+  ⟨fun _ => hasLimitsOfShape_of_reflective i⟩
+#align category_theory.reflective_products CategoryTheory.reflective_products
+
+
+open CartesianClosed
+
+variable [HasFiniteProducts C] [Reflective i] [CartesianClosed C] [HasFiniteProducts D]
+
+/-- If the reflector preserves binary products, the subcategory is an exponential ideal.
+This is the converse of `preservesBinaryProductsOfExponentialIdeal`.
+-/
+instance (priority := 10) exponentialIdeal_of_preservesBinaryProducts
+    [PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i)] : ExponentialIdeal i := by
+  let ir := Adjunction.ofRightAdjoint i
+  let L : C ⥤ D := leftAdjoint 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
+  apply CartesianClosed.curry (ir.homEquiv _ _ _)
+  apply _ ≫ (ir.homEquiv _ _).symm ((exp.ev A).app (i.obj B))
+  refine' prodComparison L A _ ≫ Limits.prod.map (𝟙 _) (ε.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_assoc, L.map_id,
+      ← prod.map_id_comp_assoc, ir.left_triangle_components, prod.map_id_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
+#align category_theory.exponential_ideal_of_preserves_binary_products CategoryTheory.exponentialIdeal_of_preservesBinaryProducts
+
+variable [ExponentialIdeal i]
+
+/-- If `i` witnesses that `D` is a reflective subcategory and an exponential ideal, then `D` is
+itself cartesian closed.
+-/
+def cartesianClosedOfReflective : CartesianClosed D :=
+  { monoidalOfHasFiniteProducts D with -- Porting note: Added this instance
+    closed := fun B =>
+      { isAdj :=
+          { right := i ⋙ exp (i.obj B) ⋙ leftAdjoint i
+            adj := by
+              apply Adjunction.restrictFullyFaithful i i (exp.adjunction (i.obj B))
+              · symm
+                refine' NatIso.ofComponents (fun X => _) (fun f => _)
+                · haveI :=
+                    Adjunction.rightAdjointPreservesLimits.{0, 0} (Adjunction.ofRightAdjoint i)
+                  apply asIso (prodComparison i B X)
+                · dsimp [asIso]
+                  rw [prodComparison_natural, Functor.map_id]
+              · apply (exponentialIdealReflective i _).symm } } }
+#align category_theory.cartesian_closed_of_reflective CategoryTheory.cartesianClosedOfReflective
+
+-- It's annoying that I need to do this.
+attribute [-instance] CategoryTheory.preservesLimitOfCreatesLimitAndHasLimit
+  CategoryTheory.preservesLimitOfShapeOfCreatesLimitsOfShapeAndHasLimitsOfShape
+
+/-- We construct a bijection between morphisms `L(A ⨯ B) ⟶ X` and morphisms `LA ⨯ LB ⟶ X`.
+This bijection has two key properties:
+* It is natural in `X`: See `bijection_natural`.
+* When `X = LA ⨯ LB`, then the backwards direction sends the identity morphism to the product
+  comparison morphism: See `bijection_symm_apply_id`.
+
+Together these help show that `L` preserves binary products. This should be considered
+*internal implementation* towards `preservesBinaryProductsOfExponentialIdeal`.
+-/
+noncomputable def bijection (A B : C) (X : D) :
+    ((leftAdjoint i).obj (A ⨯ B) ⟶ X) ≃ ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B ⟶ X) :=
+  calc
+    _ ≃ (A ⨯ B ⟶ i.obj X) := (Adjunction.ofRightAdjoint i).homEquiv _ _
+    _ ≃ (B ⨯ A ⟶ i.obj X) := ((Limits.prod.braiding _ _).homCongr (Iso.refl _))
+    _ ≃ (A ⟶ B ⟹ i.obj X) := ((exp.adjunction _).homEquiv _ _)
+    _ ≃ (i.obj ((leftAdjoint i).obj A) ⟶ B ⟹ i.obj X) :=
+      (unitCompPartialBijective _ (ExponentialIdeal.exp_closed (i.obj_mem_essImage _) _))
+    _ ≃ (B ⨯ i.obj ((leftAdjoint i).obj A) ⟶ i.obj X) := ((exp.adjunction _).homEquiv _ _).symm
+    _ ≃ (i.obj ((leftAdjoint i).obj A) ⨯ B ⟶ i.obj X) :=
+      ((Limits.prod.braiding _ _).homCongr (Iso.refl _))
+    _ ≃ (B ⟶ i.obj ((leftAdjoint i).obj A) ⟹ i.obj X) := ((exp.adjunction _).homEquiv _ _)
+    _ ≃ (i.obj ((leftAdjoint i).obj B) ⟶ i.obj ((leftAdjoint i).obj A) ⟹ i.obj X) :=
+      (unitCompPartialBijective _ (ExponentialIdeal.exp_closed (i.obj_mem_essImage _) _))
+    _ ≃ (i.obj ((leftAdjoint i).obj A) ⨯ i.obj ((leftAdjoint i).obj B) ⟶ i.obj X) :=
+      ((exp.adjunction _).homEquiv _ _).symm
+    _ ≃ (i.obj ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B) ⟶ i.obj X) :=
+      haveI : PreservesLimits i := (Adjunction.ofRightAdjoint i).rightAdjointPreservesLimits
+      haveI := preservesSmallestLimitsOfPreservesLimits i
+      Iso.homCongr (PreservesLimitPair.iso _ _ _).symm (Iso.refl (i.obj X))
+    _ ≃ ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B ⟶ X) := (equivOfFullyFaithful _).symm
+#align category_theory.bijection CategoryTheory.bijection
+
+theorem bijection_symm_apply_id (A B : C) :
+    (bijection i A B _).symm (𝟙 _) = prodComparison _ _ _ := by
+  -- Porting note: added
+  have : PreservesLimits i := (Adjunction.ofRightAdjoint i).rightAdjointPreservesLimits
+  have := preservesSmallestLimitsOfPreservesLimits i
+  dsimp [bijection]
+  -- Porting note: added
+  erw [homEquiv_symm_apply_eq, homEquiv_symm_apply_eq, homEquiv_apply_eq, homEquiv_apply_eq]
+  rw [comp_id, comp_id, comp_id, i.map_id, comp_id, unitCompPartialBijective_symm_apply,
+    unitCompPartialBijective_symm_apply, uncurry_natural_left, uncurry_curry,
+    uncurry_natural_left, uncurry_curry, prod.lift_map_assoc, comp_id, prod.lift_map_assoc, comp_id]
+  -- Porting note: added
+  dsimp only [Functor.comp_obj]
+  rw [prod.comp_lift_assoc, prod.lift_snd, prod.lift_fst_assoc, prod.lift_fst_comp_snd_comp,
+    ← Adjunction.eq_homEquiv_apply, Adjunction.homEquiv_unit, Iso.comp_inv_eq, assoc]
+  -- Porting note: rw became erw
+  erw [PreservesLimitPair.iso_hom i ((leftAdjoint i).obj A) ((leftAdjoint i).obj B)]
+  apply prod.hom_ext
+  · rw [Limits.prod.map_fst, assoc, assoc, prodComparison_fst, ← i.map_comp, prodComparison_fst]
+    apply (Adjunction.ofRightAdjoint i).unit.naturality
+  · rw [Limits.prod.map_snd, assoc, assoc, prodComparison_snd, ← i.map_comp, prodComparison_snd]
+    apply (Adjunction.ofRightAdjoint i).unit.naturality
+#align category_theory.bijection_symm_apply_id CategoryTheory.bijection_symm_apply_id
+
+theorem bijection_natural (A B : C) (X X' : D) (f : (leftAdjoint i).obj (A ⨯ B) ⟶ X) (g : X ⟶ X') :
+    bijection i _ _ _ (f ≫ g) = bijection i _ _ _ f ≫ g := by
+  dsimp [bijection]
+  -- Porting note: added
+  erw [homEquiv_symm_apply_eq, homEquiv_symm_apply_eq, homEquiv_apply_eq, homEquiv_apply_eq,
+    homEquiv_symm_apply_eq, homEquiv_symm_apply_eq, homEquiv_apply_eq, homEquiv_apply_eq]
+  apply i.map_injective
+  rw [i.image_preimage, i.map_comp, i.image_preimage, comp_id, comp_id, comp_id, comp_id, comp_id,
+    comp_id, Adjunction.homEquiv_naturality_right, ← assoc, curry_natural_right _ (i.map g),
+    unitCompPartialBijective_natural, uncurry_natural_right, ← assoc, curry_natural_right,
+    unitCompPartialBijective_natural, uncurry_natural_right, assoc]
+#align category_theory.bijection_natural CategoryTheory.bijection_natural
+
+/--
+The bijection allows us to show that `prodComparison L A B` is an isomorphism, where the inverse
+is the forward map of the identity morphism.
+-/
+theorem prodComparison_iso (A B : C) : IsIso (prodComparison (leftAdjoint i) A B) :=
+  ⟨⟨bijection i _ _ _ (𝟙 _), by
+      rw [← (bijection i _ _ _).injective.eq_iff, bijection_natural, ← bijection_symm_apply_id,
+        Equiv.apply_symm_apply, id_comp],
+      by rw [← bijection_natural, id_comp, ← bijection_symm_apply_id, Equiv.apply_symm_apply]⟩⟩
+#align category_theory.prod_comparison_iso CategoryTheory.prodComparison_iso
+
+attribute [local instance] prodComparison_iso
+
+/--
+If a reflective subcategory is an exponential ideal, then the reflector preserves binary products.
+This is the converse of `exponentialIdeal_of_preserves_binary_products`.
+-/
+noncomputable def preservesBinaryProductsOfExponentialIdeal :
+    PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i) where
+  preservesLimit {K} :=
+    letI := PreservesLimitPair.ofIsoProdComparison
+      (leftAdjoint i) (K.obj ⟨WalkingPair.left⟩) (K.obj ⟨WalkingPair.right⟩)
+    Limits.preservesLimitOfIsoDiagram _ (diagramIsoPair K).symm
+#align category_theory.preserves_binary_products_of_exponential_ideal CategoryTheory.preservesBinaryProductsOfExponentialIdeal
+
+/--
+If a reflective subcategory is an exponential ideal, then the reflector preserves finite products.
+-/
+noncomputable def preservesFiniteProductsOfExponentialIdeal (J : Type) [Fintype J] :
+    PreservesLimitsOfShape (Discrete J) (leftAdjoint i) := by
+  letI := preservesBinaryProductsOfExponentialIdeal i
+  letI := leftAdjointPreservesTerminalOfReflective.{0} i
+  apply preservesFiniteProductsOfPreservesBinaryAndTerminal (leftAdjoint i) J
+#align category_theory.preserves_finite_products_of_exponential_ideal CategoryTheory.preservesFiniteProductsOfExponentialIdeal
+
+end
+
+end CategoryTheory