toAlgHom_comp_sectionOfRetractionKerToTensorAux

English

The composite IsScalarTower.toAlgHom R P S) ∘ (sectionOfRetractionKerToTensorAux l hl σ hσ hf') equals the identity on S.

Русский

Композит IsScalarTower.toAlgHom ∘ sectionOfRetractionKerToTensorAux равен тождественному отображению на S.

LaTeX

$$(IsScalarTower.toAlgHom R P S).comp (sectionOfRetractionKerToTensorAux l hl σ hσ hf') = AlgHom.id _ _$$

Lean4

theorem toAlgHom_comp_sectionOfRetractionKerToTensorAux :
    (IsScalarTower.toAlgHom R P S).comp (sectionOfRetractionKerToTensorAux l hl σ hσ hf') = AlgHom.id _ _ :=
  by
  ext x
  obtain ⟨x, rfl⟩ := hf x
  simp [sectionOfRetractionKerToTensorAux_algebraMap, RingHom.mem_ker.mp]

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