feat(Condensed): a sequential limit of epimorphisms in light condensed modules is epimorphic

[dagurtomas]

---

• depends on: chore(CategoryTheory/Sites): make Subcanonical a class #18186
• depends on: feat(CategoryTheory/Sites): some API for the Yoneda embedding into sheaf categories #18185
• depends on: [Merged by Bors] - chore(CategoryTheory/Functor): dualize OfSequence #18325

[github-actions]

PR summary 1dd80a7930

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Condensed.Light.Epi	1695	1699	+4 (+0.24%)

Import changes for all files

Files	Import difference
Mathlib.Condensed.Light.Epi	4
Mathlib.CategoryTheory.Sites.Subcanonical	693
Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit	927

---

Declarations diff

+ Sheaf.Subcanonical
+ Sheaf.Subcanonical.isSheaf_of_isRepresentable
+ Sheaf.Subcanonical.of_isSheaf_yoneda_obj
+ Sheaf.Subcanonical.yoneda
+ Sheaf.Subcanonical.yonedaCompSheafToPresheaf
+ Sheaf.Subcanonical.yonedaFullyFaithful
+ hom_ext_yoneda
+ hom_ext_yonedaULift
+ instance : (J.yoneda).Faithful := (J.yonedaFullyFaithful).faithful
+ instance : (J.yoneda).Full := (J.yonedaFullyFaithful).full
+ instance : (LightCondensed.forget R).PreservesEpimorphisms
+ instance : (LightCondensed.forget R).ReflectsEpimorphisms
+ instance : (canonicalTopology C).Subcanonical
+ instance : compHausToCondensed.Faithful := inferInstanceAs (_ ⋙ _).Faithful
+ instance : compHausToCondensed.Full := inferInstanceAs (_ ⋙ _).Full
+ isLocallySurjective_π_app_zero_of_isLocallySurjective_map
+ le_canonical
+ map_yonedaEquiv
+ map_yonedaEquiv'
+ map_yonedaULiftEquiv
+ map_yonedaULiftEquiv'
+ of_isSheaf_yoneda_obj
+ yonedaEquiv
+ yonedaEquiv_apply
+ yonedaEquiv_comp
+ yonedaEquiv_naturality
+ yonedaEquiv_naturality'
+ yonedaEquiv_symm_app_apply
+ yonedaEquiv_symm_map
+ yonedaEquiv_yoneda_map
+ yonedaULeftEquiv_symm_map
+ yonedaULift
+ yonedaULiftEquiv
+ yonedaULiftEquiv_apply
+ yonedaULiftEquiv_comp
+ yonedaULiftEquiv_naturality
+ yonedaULiftEquiv_naturality'
+ yonedaULiftEquiv_symm_app_apply
+ yonedaULiftEquiv_symm_naturality_left
+ yonedaULiftEquiv_symm_naturality_right
+ yonedaULiftEquiv_yonedaULift_map
++ epi_π_app_zero_of_epi
++ yonedaEquiv_symm_naturality_left
++ yonedaEquiv_symm_naturality_right
++-- subcanonical
- instance : compHausToCondensed.Faithful := show (_ ⋙ _).Faithful from inferInstance
- instance : compHausToCondensed.Full := show (_ ⋙ _).Full from inferInstance
- instance : hJ.yoneda.Faithful := hJ.yonedaFullyFaithful.faithful
- instance : hJ.yoneda.Full := hJ.yonedaFullyFaithful.full
- of_yoneda_isSheaf

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• chore(CategoryTheory/Sites): make Subcanonical a class #18186
• feat(CategoryTheory/Sites): some API for the Yoneda embedding into sheaf categories #18185
• [Merged by Bors] - chore(CategoryTheory/Functor): dualize OfSequence #18325
  By Dependent Issues (🤖). Happy coding!