of_eq_map_equiv — Mathlib

English

If P lies over p, then Q lies over p when Q = P.map σ for an equivalence σ.

Русский

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

LaTeX

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

Lean4

theorem of_eq_map_equiv [P.LiesOver p] {E : Type*} [EquivLike E B C] [AlgEquivClass E A B C] (σ : E) (h : Q = P.map σ) :
    Q.LiesOver p := by
  rw [← show _ = P.map σ from comap_symm (σ : B ≃+* C)] at h
  exact of_eq_comap p (σ : B ≃ₐ[A] C).symm h

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