English
AlgHom from the top of a tower are equivalent to pairs of AlgHoms: one on the intermediate level and one on the bottom level.
Русский
Алгебра-гомоморфизмы на вершине башни эквивалентны парам гомоморфизмов: на промежуточном уровне и на нижнем уровне.
LaTeX
$$$$ algHomEquivSigma : (C \toₐ[A] D) \simeq \Sigma f : B \toₐ[A] D, @AlgHom B C D $$$$
Lean4
/-- `AlgHom`s from the top of a tower are equivalent to a pair of `AlgHom`s. -/
def algHomEquivSigma : (C →ₐ[A] D) ≃ Σ f : B →ₐ[A] D, @AlgHom B C D _ _ _ _ f.toRingHom.toAlgebra
where
toFun f := ⟨f.restrictDomain B, f.extendScalars B⟩
invFun
fg :=
let _ := fg.1.toRingHom.toAlgebra
fg.2.restrictScalars A
left_inv
f := by
dsimp only
ext
rfl
right_inv := by
rintro ⟨⟨⟨⟨⟨f, _⟩, _⟩, _⟩, _⟩, ⟨⟨⟨⟨g, _⟩, _⟩, _⟩, hg⟩⟩
obtain rfl : f = fun x => g (algebraMap B C x) := by
ext x
exact (hg x).symm
rfl
