equivPushout' — Mathlib

English

Under mono f, equality of quotients in Pushout corresponds to Rel' a b.

Русский

При моно f равенство методических частичных эквивалентов Pushout соответствует Rel' a b.

LaTeX

$$(Quot.mk a) = (Quot.mk b) ↔ Rel' a b$$

Lean4

/-- The obvious equivalence `Pushout f g ≃ Pushout' f g`. -/
def equivPushout' : Pushout f g ≃ Pushout' f g
    where
  toFun :=
    Quot.lift (Quot.mk _)
      (by
        rintro _ _ ⟨⟩
        apply Quot.sound
        apply Rel'.inl_inr)
  invFun :=
    Quot.lift (Quot.mk _)
      (by
        rintro a b (_ | ⟨x₀, y₀, h⟩ | _ | _)
        · rfl
        · have h₀ : Rel f g _ _ := Rel.inl_inr x₀
          rw [Quot.sound h₀, h]
          symm
          apply Quot.sound
          apply Rel.inl_inr
        · apply Quot.sound
          apply Rel.inl_inr
        · symm
          apply Quot.sound
          apply Rel.inl_inr)
  left_inv := by rintro ⟨x⟩; rfl
  right_inv := by rintro ⟨x⟩; rfl

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