feat(CategoryTheory/Subobject): Heyting algebra structure on Subobject in elementary topoi

[node0000]

This PR provides the canonical HeytingAlgebra (Subobject X) instance
for any category C satisfying the elementary-topos hypothesis bundle.
Closes a gap in Mathlib.CategoryTheory.Subobject.Lattice:
the SemilatticeInf, SemilatticeSup, OrderTop, OrderBot, and
Lattice instances on Subobject X were already in place, but the
Heyting-algebra structure that elementary topoi induce on the subobject
lattice was missing.

The construction follows Mac Lane and Moerdijk, Sheaves in Geometry
and Logic, IV.6 Proposition 2: implication is the residual defined
by an equalizer of characteristic morphisms, and the Galois connection
R ≤ residual P Q ↔ R ⊓ P ≤ Q is the load-bearing identity that drives
the HeytingAlgebra typeclass.

What this PR adds

A single new file Mathlib/CategoryTheory/Subobject/Heyting.lean
containing:

• CategoryTheory.Subobject.residual : Subobject X → Subobject X → Subobject X
  — the Heyting implication, defined as
  Subobject.mk (equalizer.ι (χ (P ⊓ Q).arrow) (χ P.arrow)).

• CategoryTheory.Subobject.le_residual_iff_inf_le —
  the Galois connection R ≤ residual P Q ↔ R ⊓ P ≤ Q.

• CategoryTheory.Subobject.heytingAlgebra —
  the HeytingAlgebra (Subobject X) instance, with
  himp := residual, compl P := residual P ⊥,
  le_himp_iff := le_residual_iff_inf_le, and himp_bot := rfl.

Six private lemmas (residual_E1, residual_E2, residual_E3 for the
elimination half of the Galois connection; residual_I1, residual_I2,
residual_I3 for the introduction half) carry the proof; they are
file-local and do not enter the public API.

Hypothesis bundle

[HasSubobjectClassifier C] [HasPullbacks C] [HasEqualizers C]
[HasInitial C] [HasImages C] [HasBinaryCoproducts C] [InitialMonoClass C]

These together are entailed by C being an elementary topos. Of these,
HasSubobjectClassifier and HasEqualizers are the genuinely new
requirements for the residual construction itself; the remainder enter
via the existing SemilatticeInf, SemilatticeSup, OrderTop, and
OrderBot instances on Subobject X that HeytingAlgebra extends.
The per-lemma breakdown is given in the file's module docstring.

Connection to existing API

Mathlib/CategoryTheory/Subobject/Lattice.lean (Bhavik Mehta, Kim
Morrison) already exhibits the SemilatticeInf, SemilatticeSup, OrderTop, OrderBot, Lattice instances on Subobject X under the
corresponding limit/colimit hypotheses. This PR extends that chain
to HeytingAlgebra using the new HasSubobjectClassifier typeclass
introduced in Mathlib/CategoryTheory/Subobject/Classifier/Defs.lean
(Charlie Conneen, Pablo Donato, Klaus Gy, 2024) and the equalizer
infrastructure in Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean.

Combined with the presheaf-topos classifier instance in
Mathlib.CategoryTheory.Topos.Sheaf (HasSubobjectClassifier (Cᵒᵖ ⥤ Type w)
for EssentiallySmall.{w} C), this gives the Heyting structure on any
presheaf-topos subobject lattice automatically.

Use of AI

Per Mathlib's AI-use policy,
disclosing: the initial proof skeleton and the six bridging lemmas
were drafted with the assistance of Cursor
running Anthropic Claude as the
underlying model, during a multi-session co-working pass on a private
formalization project.

The author is the maintainer of the
FalseWork Papers project,
where this instance has been consumed by application-level theorems
(four_position_partition and three other position-theory results)
since Phase 3 of that project — providing a real downstream test of
the construction.

Testing

• The instance resolves at the abstract level (an inferInstance smoke
  test under the topos hypothesis bundle exhibits this).
• himp_bot discharges via rfl (the pseudo-complement is definitionally
  residual P ⊥); le_himp_iff is the Galois connection theorem assembled
  from the six bridging lemmas.
• Downstream: in the FalseWork Papers project, the instance carries four
  position-theory theorems whose proofs are
  LE.le.disjoint_compl_right-style consequences of the Heyting
  structure, kernel-checked with #print axioms reporting only
  [propext, Classical.choice, Quot.sound].
• Users should depend on this instance via typeclass search rather than
  parameterizing over [HeytingAlgebra (Subobject Y)], which can produce
  instance diamonds against the native Subobject order structure.

Acknowledgments

Thanks to Edward van de Meent and Fernando Chu for confirming
the gap and discussing the construction's shape in
a #maths Zulip thread
(2026-05).

References

• [MM92] S. Mac Lane and I. Moerdijk, Sheaves in Geometry and Logic,
  Springer, 1992. Chapter IV § 6, Proposition 2 (the residual
  construction) and Theorem 8 (subobject lattice is a Heyting
  algebra).

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary 082cf14f30

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Subobject.Heyting (new file)	750

---

Declarations diff

+ heytingAlgebra
+ le_residual_iff_inf_le
+ residual
+ residual_E1
+ residual_E2
+ residual_E3
+ residual_I1
+ residual_I2
+ residual_I3

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[dagurtomas]

I'm closing this under our new-contributor-AI-policy. Here is an AI generated overall review if it helps:

Recommendation

I would close it under the AI policy. The author explicitly discloses that
“the initial proof skeleton and the six bridging lemmas were drafted with
Cursor/Claude”, and the commit includes:

  Co-authored-by: Cursor <cursoragent@cursor.com>                              

This is a substantial new theorem/instance file, not a small edit, so the
AI-generated skeleton is core to the contribution.

Additional code-quality concerns

Even ignoring policy, I would not treat this as close to merge-ready:

• The proof structure is very “AI scaffold” shaped: residual_E1, residual_E2,
  residual_E3, residual_I1, etc. These are proof-step names, not
  reusable/mathlib-style API.
• Several private lemmas are thin wrappers around existing facts, e.g.
  residual_I1 := Subobject.inf_pullback _ _ _.
• The proof is brittle and low-level:
  • uses change to unfold implementation details of residual;
  • manually sets 𝒞 := HasSubobjectClassifier.exists_classifier.some;
  • repeats the same classifier/pullback key argument twice;
  • comments mention “unsolvable metavar” and instance-diamond workarounds.
• Documentation contains non-mathlib phrasing like “load-bearing”, “hypothesis
  bundle”, and over-explains implementation details instead of presenting
  clean API.
• The PR body itself warns about possible instance diamonds if users
  parameterize over [HeytingAlgebra (Subobject Y)], which suggests the
  instance/design has not been fully integrated with the existing Subobject
  order API.

Salvageability

The mathematical idea is plausible and the file compiles, but getting it into
mathlib quality would require a real refactor by someone comfortable with the
Subobject/classifier API. It is not a quick doc/proof-golf pass.