reflects_preregular — Mathlib

English

A functor that preserves and reflects effective epis and is effective enough reflects preregularity.

Русский

Функтор, сохраняющий и отражающий эффективные эпизоды и обладающий достаточной эффективностью, отражает preregularity.

LaTeX

$$$\text{reflects_preregular}(F)$$$

Lean4

theorem reflects_preregular : Preregular C where
  exists_fac f g
    _ := by
    obtain ⟨W, f', _, i, w⟩ := Preregular.exists_fac (F.map f) (F.map g)
    refine
      ⟨_, F.preimage (F.effectiveEpiOver W ≫ f'),
        ⟨F.effectiveEpi_of_map _ ?_, F.preimage (F.effectiveEpiOver W ≫ i), ?_⟩⟩
    · simp only [Functor.map_preimage]
      infer_instance
    · apply F.map_injective
      simp [w]

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