English
An algebraic closure equivalence between L and M exists under suitable algebraicity assumptions.
Русский
Существет эквивалентность замыкания между L и M при подходящих алгебраических предпосылках.
LaTeX
$$$L \\cong_R M$ under the given algebraic hypotheses.$$
Lean4
/-- Used in the definition of `equivOfEquiv` -/
noncomputable def equivOfEquivAux (hSR : S ≃+* R) :
{ e : L ≃+* M // e.toRingHom.comp (algebraMap S L) = (algebraMap R M).comp hSR.toRingHom } :=
by
letI : Algebra R S := RingHom.toAlgebra hSR.symm.toRingHom
letI : Algebra S R := RingHom.toAlgebra hSR.toRingHom
have : IsDomain S := (FaithfulSMul.algebraMap_injective S L).isDomain _
letI : Algebra R L := RingHom.toAlgebra ((algebraMap S L).comp (algebraMap R S))
haveI : IsScalarTower R S L := .of_algebraMap_eq fun _ => rfl
haveI : IsScalarTower S R L := .of_algebraMap_eq (by simp [RingHom.algebraMap_toAlgebra])
have : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr hSR.symm.injective
have : Algebra.IsAlgebraic R L :=
(IsAlgClosure.isAlgebraic.extendScalars (show Function.Injective (algebraMap S R) from hSR.injective))
refine ⟨equivOfAlgebraic' R S L M, ?_⟩
ext x
simp only [RingEquiv.toRingHom_eq_coe, Function.comp_apply, RingHom.coe_comp, AlgEquiv.coe_ringEquiv,
RingEquiv.coe_toRingHom]
conv_lhs => rw [← hSR.symm_apply_apply x]
change equivOfAlgebraic' R S L M (algebraMap R L (hSR x)) = _
rw [AlgEquiv.commutes]
