addMap_of_Z_eq_zero_left — Mathlib

English

If P lies on W and Q is a nonsingular lift with Q_z = 0, then addMap ⟦P⟧ Q equals Q.

Русский

Если P лежит на W, а Q — несингулярный подъём с Q_z = 0, то addMap ⟦P⟧ Q = Q.

LaTeX

$$$ W.addMap \\llbracket P \\rrbracket Q = Q $$$

Lean4

theorem addMap_of_Z_eq_zero_left {P : Fin 3 → F} {Q : PointClass F} (hP : W.Nonsingular P) (hQ : W.NonsingularLift Q)
    (hPz : P z = 0) : W.addMap ⟦P⟧ Q = Q := by
  revert hQ
  refine Q.inductionOn (motive := fun Q => _ → W.addMap _ Q = Q) fun Q hQ => ?_
  by_cases hQz : Q z = 0
  · rw [addMap_eq, add_of_Z_eq_zero hP hQ hPz hQz, smul_eq _ <| (isUnit_Y_of_Z_eq_zero hP hPz).pow 4, Quotient.eq]
    exact Setoid.symm <| equiv_zero_of_Z_eq_zero hQ hQz
  ·
    rw [addMap_eq, add_of_Z_eq_zero_left hP.left hPz hQz,
      smul_eq _ <| ((isUnit_Y_of_Z_eq_zero hP hPz).pow 2).mul <| Ne.isUnit hQz]

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