ext — Mathlib

English

Extensionality for the CorepresentableBy structure: equality of the homEquiv at the identity determines equality of corepresentable data.

Русский

Расширение CorepresentableBy: равенство homEquiv на единичном элементе определяет равенство элементов.

LaTeX

$$ext {F : C ⥤ Type v} {X : C} {e e' : F.CorepresentableBy X} (h : e.homEquiv (id X) = e'.homEquiv (id X)) : e = e'$$

Lean4

@[ext]
theorem ext {F : C ⥤ Type v} {X : C} {e e' : F.CorepresentableBy X} (h : e.homEquiv (𝟙 X) = e'.homEquiv (𝟙 X)) :
    e = e' :=
  by
  have : ∀ {Y : 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

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