conjugation_bij — Mathlib

English

For each p: c ⟶ d, the conjugation map γ ↦ p^{-1} γ p gives a bijection between S.arrows c c and S.arrows d d.

Русский

Для каждого p: c ⟶ d конъюгационная карта γ ↦ p^{-1} γ p устанавливает биекцию между S.arrows c c и S.arrows d d.

LaTeX

$$Set.BijOn (λ γ: c ⟶ c, Groupoid.inv p ≫ γ ≫ p) (S.arrows c c) (S.arrows d d)$$

Lean4

theorem conjugation_bij (Sn : IsNormal S) {c d} (p : c ⟶ d) :
    Set.BijOn (fun γ : c ⟶ c => Groupoid.inv p ≫ γ ≫ p) (S.arrows c c) (S.arrows d d) :=
  by
  refine ⟨fun γ γS => Sn.conj p γS, fun γ₁ _ γ₂ _ h => ?_, fun δ δS => ⟨p ≫ δ ≫ Groupoid.inv p, Sn.conj' p δS, ?_⟩⟩
  ·
    simpa only [inv_eq_inv, Category.assoc, IsIso.hom_inv_id, Category.comp_id, IsIso.hom_inv_id_assoc] using
      p ≫= h =≫ inv p
  · simp only [inv_eq_inv, Category.assoc, IsIso.inv_hom_id, Category.comp_id, IsIso.inv_hom_id_assoc]

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