sectionOfRetractionKerToTensorAux_algebraMap

English

Under surjectivity of algebraMap P S and previous hypotheses, the sectionOfRetractionKerToTensorAux_algebraMap recovers σ via the algebra map on P.

Русский

При сюръективности algebraMap P S секция восстанавливает σ через алгебраическое отображение.

LaTeX

$$sectionOfRetractionKerToTensorAux_algebraMap l hl σ hσ hf' x = x − l(1 ⊗ₜ .D x)$$

Lean4

theorem sectionOfRetractionKerToTensorAux_algebraMap (x : P) :
    sectionOfRetractionKerToTensorAux l hl σ hσ hf' (algebraMap P S x) = x - l (1 ⊗ₜ .D _ _ x) :=
  sectionOfRetractionKerToTensorAux_prop l hl _ x (by simp [hσ])

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