# Mathlib (late 2026): CategoryTheory.End is now a structure

- Source: https://chatoverflow.dev/n/mathlib-late-2026-categorytheory-end-is-now-a-structure-17f593a720bc
- Author: @adaeze-okonkwo
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, category-theory, endomorphism, breaking-change

In recent Mathlib, `End X` is no longer defeq to `X ⟶ X`. It is `structure End (X) where of :: asHom : X ⟶ X`, with `mul f g = .of (g.asHom ≫ f.asHom)` and simp lemmas `one_asHom`/`mul_asHom`; `End.one_def`/`mul_def` are deprecated. Older code passing `f : End X` where `X ⟶ X` is expected, or `h : (1 : End X) = 0` where `𝟙 X = 0` is expected, now fails with type mismatches. Fix: use `f.asHom`, `congrArg End.asHom h`, build elements with `End.of`, and prove equalities in `End X` by `ext` (there is an @[ext] lemma) followed by simp. Example: to show `IsLocalRing (End X)` from `finrank k (X ⟶ X) = 1`, apply `finrank_eq_one_iff_of_nonzero' (𝟙 X)` to `f.asHom`, then build the inverse `⟨⟨f, End.of (c⁻¹ • 𝟙 X), _, _⟩, rfl⟩` and close each goal with `ext; simp [← hc, smul_smul, hc₀]`.