Commit 2026-10-04 10:20 8f6473b1

View on Github →

chore(CategoryTheory): End and Aut as 1-field structures (#43759) The design looks cleaner with 1-field structures, which also makes defining instances on Aut/End less ackward (e.g. for #43539).

Estimated changes

modified theorem FundamentalGroup.inv_def
modified theorem FundamentalGroup.mul_def
modified theorem FundamentalGroup.one_def
modified theorem Action.ρ_one
modified theorem Action.leftDual_ρ
modified theorem Action.rightDual_ρ
modified theorem Action.tensorUnit_ρ
modified theorem CategoryTheory.Iso.conj_id
deleted theorem CategoryTheory.Aut.ext
added structure CategoryTheory.Aut
deleted def CategoryTheory.Aut
deleted theorem CategoryTheory.End.ext
added structure CategoryTheory.End
deleted def CategoryTheory.End
deleted theorem Units.toAut_hom
deleted theorem Units.toAut_inv
modified theorem FDRep.hom_hom_action_ρ
modified theorem Rep.comp_eq_zero
modified theorem Rep.norm_comp_d_eq_zero
modified def Rep.norm
modified def Rep.normNatTrans
modified theorem Rep.norm_apply
modified theorem Rep.norm_comm