liftEquiv — Mathlib

English

For equalizers f,g and maps φ, ψ, the relation (ι f2 g2) ∘ (map φ ψ hf hg) = φ ∘ (ι f1 g1) holds.

Русский

Для равноподобий f,g и отображений φ, ψ выполняется (ι f2 g2) ∘ (map φ ψ hf hg) = φ ∘ (ι f1 g1).

LaTeX

$$$ (\\iota f_2 g_2) \\circ (\\operatorname{map} \\phi \\psi \\text{hf} \\text{hg}) = \\phi \\circ (\\iota f_1 g_1) $$$

Lean4

/-- The lifting property of the equalizer as an equivalence. -/
@[simps]
def liftEquiv : { φ : NormedAddGroupHom V₁ V // f.comp φ = g.comp φ } ≃ NormedAddGroupHom V₁ (f.equalizer g)
    where
  toFun φ := lift φ φ.prop
  invFun ψ := ⟨(ι f g).comp ψ, by rw [← comp_assoc, ← comp_assoc, comp_ι_eq]⟩
  left_inv φ := by simp

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