arrows_iff — Mathlib

English

Same as GeneratedNormal Le with explicit S.IsNormal: generatedNormal X ≤ S ↔ ∀ c d, X c d ⊆ S.arrows c d.

Русский

То же самое, что GeneratedNormal_le, но явно используется свойство S.IsNormal.

LaTeX

$$$\forall S\, (S.IsNormal) \;:\; generatedNormal X \le S \ \Leftrightarrow\ \forall c d, X c d \subseteq S.arrows c d$$$

Lean4

theorem arrows_iff (hφ : Function.Injective φ.obj) (S : Subgroupoid C) {c d : D} (f : c ⟶ d) :
    Map.Arrows φ hφ S c d f ↔
      ∃ (a b : C) (g : a ⟶ b) (ha : φ.obj a = c) (hb : φ.obj b = d) (_hg : g ∈ S.arrows a b),
        f = eqToHom ha.symm ≫ φ.map g ≫ eqToHom hb :=
  by
  constructor
  · rintro ⟨g, hg⟩; exact ⟨_, _, g, rfl, rfl, hg, eq_conj_eqToHom _⟩
  · rintro ⟨a, b, g, rfl, rfl, hg, rfl⟩; rw [← eq_conj_eqToHom]; constructor; exact hg

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