English
An A⧸p-algebra isomorphism between B⧸P and C⧸Q is induced by an A-algebra isomorphism between B and C when P = Q.comap σ.
Русский
Изоморфизм A⧸p-алгебр между B⧸P и C⧸Q индуцируется A-алгебраическим изоморфизмом между B и C при условии P = Q.comap σ.
LaTeX
$$$\text{AlgEquiv}_{A/ p}(B/P, C/Q) \text{ exists if } P = Q.comap σ$ and is given by algEquivOfEqComap.$$
Lean4
/-- The action on an ideal corresponding to applying the action to every element.
This is available as an instance in the `Pointwise` locale. -/
protected def pointwiseDistribMulAction : DistribMulAction M (Ideal R)
where
smul a := Ideal.map (MulSemiringAction.toRingHom _ _ a)
one_smul I := congr_arg (I.map ·) (RingHom.ext <| one_smul M) |>.trans I.map_id
mul_smul _ _ I := congr_arg (I.map ·) (RingHom.ext <| mul_smul _ _) |>.trans (I.map_map _ _).symm
smul_zero _ := Ideal.map_bot
smul_add _ I J := Ideal.map_sup _ I J
