Commit 2026-09-04 11:59 8e4ed63e

View on Github →

chore(CategoryTheory): use the new ↧ notation in concrete categories (#41811) ... as well as the corresponding delaborator. Also remove one extra line break added by the previous PR. Generated by Claude Opus, reviewed line-by-line by myself. Assisted-by: Claude Opus 4.8

Estimated changes

modified theorem CommAlgCat.binaryCofan_pt
modified theorem FGModuleCat.ihom_obj
modified def AddCommGrpCat.asHom
modified theorem AddCommGrpCat.int_hom_ext
modified def AddCommGrpCat.image
modified def ModuleCat.image
modified def unitInterval.uhpath01
modified theorem CategoryTheory.Cat.coe_of
modified def smoothPresheafRing
modified def smoothSheaf
modified def smoothSheafCommRing
modified def smoothSheafRing
modified def groupCohomology.H0Iso
modified def groupCohomology.H1π
modified def groupCohomology.H2π
modified def groupHomology.H0π
modified def groupHomology.H1π
modified def groupHomology.H2π
modified def Profinite.pi
modified def TopCat.piIsoPi
modified def TopCat.prodIsoProd
modified def TopCat.sigmaIsoSigma
modified def TopCat.I