heyting implication on Subobject X

Stream: maths

[Mario Carneiro]

Does anyone know what kind of assumptions are needed to define the heyting implication on the lattice of subobjects? (@Sina H 𓃵?) It is used on page 9 here (cc: @Valeria de Paiva) which asserts that it suffices to assume that C is locally cartesian closed (but also mentions that this assumption is not minimal). Mathlib has a construction docs#CategoryTheory.Subobject.sSup which depends on [WellPowered C] [HasImages C] [HasCoproducts C] but I don't know what relation these assumptions have to being an LCCC

[Mario Carneiro]

Oh, apparently having a sSup is not sufficient for sSup {Z | Z ⊓ X ≤ Y} to define heyting implication, you also need the complete distributive law docs#Order.Frame.inf_sSup_le_iSup_inf

[Kim Morrison]

From memory [WellPowered C] [HasImages C] [HasCoproducts C] came as a result of applied reverse mathematics while developing the file, rather than the literature.

[Mario Carneiro]

I'm currently making use of the following dubious typeclass:

protected class Subobject.HasHImp (C) [Category C] [HasPullbacks C]  where
  himp {A : C} (X Y : Subobject A) : Subobject A
  le_himp_iff {A : C} {a b c : Subobject A} : a ≤ himp b c ↔ a ⊓ b ≤ c
  himp_pullback_le {A B : C} (f : A ⟶ B) {a b : Subobject B} :
    himp ((pullback f).obj a) ((pullback f).obj b) ≤ (pullback f).obj (himp a b)

I have tried and failed to prove both of these lemmas, and I have reason to believe that le_himp_iff is false using the supremum definition because in preorder categories the question reduces to the aforementioned lattice rule inf_sSup_le_iSup_inf, which is not derivable from just complete lattice axioms

[Valeria de Paiva]

@Mario Carneiro you have seen https://ncatlab.org/nlab/show/Heyting+category right? this seems to indicate that we need that coproducts are stable under pullbacks in C as well, which is something I already knew I needed to have later on for additives.
But distributivity of the lattice of subobjects I thought was automatic. maybe not?

[Yaël Dillies]

General subobjects are not distributive, right? Consider vector subspaces

[Bhavik Mehta]

iirc this file came out of stuff I had in the topos project, in which I deduced these facts from the existence of a subobject classifier, which is a stronger assumption than images and coproducts and LCCC but doesn't assume well powered-ness...