reflects_precoherent — Mathlib

English

Equalizer condition is preserved under a natural isomorphism between functors.

Русский

Условие равнителя сохраняется при натуральном изоморфизме между функторaми.

LaTeX

$$$P \cong P' \Rightarrow (\text{equalizerCondition } P) \Rightarrow (\text{equalizerCondition } P')$$$

Lean4

theorem reflects_precoherent : Precoherent C where
  pullback {B₁ B₂} f α _ X₁ π₁
    _ :=
    by
    obtain ⟨β, _, Y₂, τ₂, H, i, ι, hh⟩ := Precoherent.pullback (F.map f) _ _ (fun a ↦ F.map (π₁ a)) inferInstance
    refine
      ⟨β, inferInstance, _, fun b ↦ F.preimage (F.effectiveEpiOver (Y₂ b) ≫ τ₂ b),
        F.finite_effectiveEpiFamily_of_map _ _ ?_, ⟨i, fun b ↦ F.preimage (F.effectiveEpiOver (Y₂ b) ≫ ι b), ?_⟩⟩
    · simp only [Functor.map_preimage]
      infer_instance
    · intro b
      apply F.map_injective
      simp [hh b]

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