mathlib3 documentation

category_theory.closed.ideal

Exponential ideals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

@[class]

structure category_theory.exponential_ideal {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (i : D ⥤ C) [category_theory.limits.has_finite_products C] [category_theory.cartesian_closed C] :

Prop

exp_closed : ∀ {B : C}, B ∈ i.ess_image → ∀ (A : C), (category_theory.exp A).obj B ∈ i.ess_image

The subcategory D of C expressed as an inclusion functor is an exponential ideal if B ∈ D implies A ⟹ B ∈ D for all A.

Instances of this typeclass

theorem category_theory.exponential_ideal.mk' {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (i : D ⥤ C) [category_theory.limits.has_finite_products C] [category_theory.cartesian_closed C] (h : ∀ (B : D) (A : C), (category_theory.exp A).obj (i.obj B) ∈ i.ess_image) :

category_theory.exponential_ideal i

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.

@[protected, instance]

def category_theory.functor.id.exponential_ideal {C : Type u₁} [category_theory.category C] [category_theory.limits.has_finite_products C] [category_theory.cartesian_closed C] :

category_theory.exponential_ideal (𝟭 C)

The entire category viewed as a subcategory is an exponential ideal.

@[protected, instance]

def category_theory.subterminal_inclusion.exponential_ideal {C : Type u₁} [category_theory.category C] [category_theory.limits.has_finite_products C] [category_theory.cartesian_closed C] :

category_theory.exponential_ideal (category_theory.subterminal_inclusion C)

The subcategory of subterminal objects is an exponential ideal.

noncomputable def category_theory.exponential_ideal_reflective {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (i : D ⥤ C) [category_theory.limits.has_finite_products C] [category_theory.cartesian_closed C] (A : C) [category_theory.reflective i] [category_theory.exponential_ideal i] :

i ⋙ category_theory.exp A ⋙ category_theory.left_adjoint i ⋙ i ≅ i ⋙ category_theory.exp A

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 ⋙ left_adjoint i ⋙ i ≅ i ⋙ exp A, that is: (A ⟹ iB) ≅ i L (A ⟹ iB), naturally in B. The converse is given in exponential_ideal.mk_of_iso.

Equations

category_theory.exponential_ideal_reflective i A = (category_theory.nat_iso.of_components (λ (X : D), category_theory.as_iso ((category_theory.adjunction.of_right_adjoint i).unit.app ((category_theory.exp A).obj (i.obj X)))) _).symm

theorem category_theory.exponential_ideal.mk_of_iso {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (i : D ⥤ C) [category_theory.limits.has_finite_products C] [category_theory.cartesian_closed C] [category_theory.reflective i] (h : Π (A : C), i ⋙ category_theory.exp A ⋙ category_theory.left_adjoint i ⋙ i ≅ i ⋙ category_theory.exp A) :

category_theory.exponential_ideal i

Given a natural isomorphism i ⋙ exp A ⋙ left_adjoint i ⋙ i ≅ i ⋙ exp A, we can show i is an exponential ideal.

theorem category_theory.reflective_products {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (i : D ⥤ C) [category_theory.limits.has_finite_products C] [category_theory.reflective i] :

category_theory.limits.has_finite_products D

@[protected, instance]

def category_theory.exponential_ideal_of_preserves_binary_products {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (i : D ⥤ C) [category_theory.limits.has_finite_products C] [category_theory.reflective i] [category_theory.cartesian_closed C] [category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) (category_theory.left_adjoint i)] :

category_theory.exponential_ideal i

If the reflector preserves binary products, the subcategory is an exponential ideal. This is the converse of preserves_binary_products_of_exponential_ideal.

noncomputable def category_theory.cartesian_closed_of_reflective {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (i : D ⥤ C) [category_theory.limits.has_finite_products C] [category_theory.reflective i] [category_theory.cartesian_closed C] [category_theory.exponential_ideal i] :

category_theory.cartesian_closed D

If i witnesses that D is a reflective subcategory and an exponential ideal, then D is itself cartesian closed.

Equations

category_theory.cartesian_closed_of_reflective i = {closed' := λ (B : D), {is_adj := {right := i ⋙ category_theory.exp (i.obj B) ⋙ category_theory.left_adjoint i, adj := category_theory.adjunction.restrict_fully_faithful i i (category_theory.exp.adjunction (i.obj B)) (category_theory.nat_iso.of_components (λ (X : D), category_theory.as_iso (category_theory.limits.prod_comparison i B X)) _).symm (category_theory.exponential_ideal_reflective i (i.obj B)).symm category_theory.reflective.to_faithful}}}

noncomputable def category_theory.bijection {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (i : D ⥤ C) [category_theory.limits.has_finite_products C] [category_theory.reflective i] [category_theory.cartesian_closed C] [category_theory.exponential_ideal i] (A B : C) (X : D) :

((category_theory.left_adjoint i).obj (A ⨯ B) ⟶ X) ≃ ((category_theory.left_adjoint i).obj A ⨯ (category_theory.left_adjoint i).obj B ⟶ X)

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 preserves_binary_products_of_exponential_ideal.

Equations

category_theory.bijection i A B X = (((((((((((category_theory.adjunction.of_right_adjoint i).hom_equiv (A ⨯ B) X).trans ((category_theory.limits.prod.braiding A B).hom_congr (category_theory.iso.refl (i.obj X)))).trans ((category_theory.exp.adjunction B).hom_equiv A (i.obj X))).trans (category_theory.unit_comp_partial_bijective A _)).trans ((category_theory.exp.adjunction B).hom_equiv (i.obj ((category_theory.left_adjoint i).obj A)) (i.obj X)).symm).trans ((category_theory.limits.prod.braiding B (i.obj ((category_theory.left_adjoint i).obj A))).hom_congr (category_theory.iso.refl (i.obj X)))).trans ((category_theory.exp.adjunction (i.obj ((category_theory.left_adjoint i).obj A))).hom_equiv B (i.obj X))).trans (category_theory.unit_comp_partial_bijective B _)).trans ((category_theory.exp.adjunction (i.obj ((category_theory.left_adjoint i).obj A))).hom_equiv (i.obj ((category_theory.left_adjoint i).obj B)) (i.obj X)).symm).trans ((category_theory.limits.preserves_limit_pair.iso i ((category_theory.left_adjoint i).obj A) ((category_theory.left_adjoint i).obj B)).symm.hom_congr (category_theory.iso.refl (i.obj X)))).trans (category_theory.equiv_of_fully_faithful i).symm

theorem category_theory.bijection_symm_apply_id {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (i : D ⥤ C) [category_theory.limits.has_finite_products C] [category_theory.reflective i] [category_theory.cartesian_closed C] [category_theory.exponential_ideal i] (A B : C) :

⇑((category_theory.bijection i A B ((category_theory.left_adjoint i).obj A ⨯ (category_theory.left_adjoint i).obj B)).symm) (𝟙 ((category_theory.left_adjoint i).obj A ⨯ (category_theory.left_adjoint i).obj B)) = category_theory.limits.prod_comparison (category_theory.left_adjoint i) A B

theorem category_theory.bijection_natural {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (i : D ⥤ C) [category_theory.limits.has_finite_products C] [category_theory.reflective i] [category_theory.cartesian_closed C] [category_theory.exponential_ideal i] (A B : C) (X X' : D) (f : (category_theory.left_adjoint i).obj (A ⨯ B) ⟶ X) (g : X ⟶ X') :

⇑(category_theory.bijection i A B X') (f ≫ g) = ⇑(category_theory.bijection i A B X) f ≫ g

theorem category_theory.prod_comparison_iso {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (i : D ⥤ C) [category_theory.limits.has_finite_products C] [category_theory.reflective i] [category_theory.cartesian_closed C] [category_theory.exponential_ideal i] (A B : C) :

category_theory.is_iso (category_theory.limits.prod_comparison (category_theory.left_adjoint i) A B)

The bijection allows us to show that prod_comparison L A B is an isomorphism, where the inverse is the forward map of the identity morphism.

noncomputable def category_theory.preserves_binary_products_of_exponential_ideal {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (i : D ⥤ C) [category_theory.limits.has_finite_products C] [category_theory.reflective i] [category_theory.cartesian_closed C] [category_theory.exponential_ideal i] :

category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) (category_theory.left_adjoint i)

If a reflective subcategory is an exponential ideal, then the reflector preserves binary products. This is the converse of exponential_ideal_of_preserves_binary_products.

Equations

category_theory.preserves_binary_products_of_exponential_ideal i = {preserves_limit := λ (K : category_theory.discrete category_theory.limits.walking_pair ⥤ C), category_theory.limits.preserves_limit_of_iso_diagram (category_theory.left_adjoint i) (category_theory.limits.diagram_iso_pair K).symm}

noncomputable def category_theory.preserves_finite_products_of_exponential_ideal {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (i : D ⥤ C) [category_theory.limits.has_finite_products C] [category_theory.reflective i] [category_theory.cartesian_closed C] [category_theory.exponential_ideal i] (J : Type) [fintype J] :

category_theory.limits.preserves_limits_of_shape (category_theory.discrete J) (category_theory.left_adjoint i)

If a reflective subcategory is an exponential ideal, then the reflector preserves finite products.

Equations

category_theory.preserves_finite_products_of_exponential_ideal i J = let _inst : category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) (category_theory.left_adjoint i) := category_theory.preserves_binary_products_of_exponential_ideal i, _inst_8 : category_theory.limits.preserves_limits_of_shape (category_theory.discrete pempty) (category_theory.left_adjoint i) := category_theory.left_adjoint_preserves_terminal_of_reflective i in category_theory.preserves_finite_products_of_preserves_binary_and_terminal (category_theory.left_adjoint i) J