ext — Mathlib

English

Extensionality principle for RepresentableBy: equality of homEquiv at identity implies equality of the two representations.

Русский

Принцип экстентности для RepresentableBy: равенство h omEquiv на идентичности влечёт равенство двух представляемых структур.

LaTeX

$$ext {F : C^{op} ⥤ Type v} {Y : C} {e e' : F.RepresentableBy Y} (h : e.homEquiv (1_Y) = e'.homEquiv (1_Y)) : e = e'$$

Lean4

@[ext]
theorem ext {F : Cᵒᵖ ⥤ Type v} {Y : C} {e e' : F.RepresentableBy Y} (h : e.homEquiv (𝟙 Y) = e'.homEquiv (𝟙 Y)) :
    e = e' :=
  by
  have : ∀ {X : C} (f : X ⟶ Y), e.homEquiv f = e'.homEquiv f := fun {X} f ↦ by rw [e.homEquiv_eq, e'.homEquiv_eq, h]
  obtain ⟨e, he⟩ := e
  obtain ⟨e', he'⟩ := e'
  obtain rfl : @e = @e' := by ext; apply this
  rfl

Похожие утверждения