isoMk — Mathlib

Lean4
/-- Construct an isomorphism in a Grothendieck construction from isomorphisms in its base and fiber.
-/
@[simps]
def isoMk {X Y : Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).obj X.fiber ≅ Y.fiber) : X ≅ Y
    where
  hom := ⟨e₁.hom, e₂.hom⟩
  inv := ⟨e₁.inv, (F.map e₁.inv).map e₂.inv ≫ eqToHom (Functor.congr_obj (F.mapIso e₁).hom_inv_id X.fiber)⟩
  hom_inv_id := Grothendieck.ext _ _ (by simp) (by simp)
  inv_hom_id :=
    Grothendieck.ext _ _ (by simp)
      (by
        have := Functor.congr_hom (F.mapIso e₁).inv_hom_id e₂.inv
        dsimp at this
        simp [this])
Похожие утверждения