autEmbedding_injective — Mathlib

English

Aut F embeds injectively into the product ∏_X Aut(F.obj X). If two automorphisms map to the same family, they are equal.

Русский

Aut F инъективно вложен в произведение ∏_X Aut(F.obj X); если две автоморфизмы отображаются в одну и ту же семейство, то они равны.

LaTeX

$$∀σ τ, autEmbedding(F)(σ)=autEmbedding(F)(τ) ⇒ σ=τ$$

Lean4

theorem autEmbedding_injective : Function.Injective (autEmbedding F) :=
  by
  intro σ τ h
  ext X x
  have : σ.app X = τ.app X := congr_fun h X
  rw [← Iso.app_hom, ← Iso.app_hom, this]

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