of_eq_comap — Mathlib

English

If P lies over p and there is an equivalence σ with Q = P.map σ, then Q lies over p.

Русский

Если P лежит над p и существует эквивалентность σ с Q = P.map σ, тогда Q лежит над p.

LaTeX

$$$ P.LiesOver p \\Rightarrow (Q = P.map\\, \\sigma) \\Rightarrow Q.LiesOver p. $$$

Lean4

theorem of_eq_comap [Q.LiesOver p] {F : Type*} [FunLike F B C] [AlgHomClass F A B C] (f : F) (h : P = Q.comap f) :
    P.LiesOver p where
  over := by
    rw [h]
    exact (over_def Q p).trans <| congrFun (congrFun (congrArg comap ((f : B →ₐ[A] C).comp_algebraMap.symm)) _) Q

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