English
If p ≤ comap(algebraMap R A) P, then there is a canonical Algebra (R/p) (A/P) structure.
Русский
Если p ≤ comap(algebraMap R A) P, существует каноническая структура Algebra (R/p) (A/P).
LaTeX
$$$algebraQuotientOfLEComap \\ (p \le comap (algebraMap R A) P) : Algebra (R/ p) (A/ P)$$$
Lean4
/-- If `P` lies over `p`, then `R / p` has a canonical map to `A / P`. -/
abbrev algebraQuotientOfLEComap {R} [CommRing R] [Algebra R A] {p : Ideal R} {P : Ideal A} [P.IsTwoSided]
(h : p ≤ comap (algebraMap R A) P) : Algebra (R ⧸ p) (A ⧸ P)
where
algebraMap := quotientMap P (algebraMap R A) h
smul :=
Quotient.lift₂ (⟦· • ·⟧) fun r₁ a₁ r₂ a₂ hr ha ↦
Quotient.sound <| by
have := h (p.quotientRel_def.mp hr)
rw [mem_comap, map_sub] at this
simpa only [Algebra.smul_def] using P.quotientRel_def.mpr (P.mul_sub_mul_mem this <| P.quotientRel_def.mp ha)
smul_def' := by rintro ⟨_⟩ ⟨_⟩; exact congr_arg (⟦·⟧) (Algebra.smul_def _ _)
commutes' := by rintro ⟨_⟩ ⟨_⟩; exact congr_arg (⟦·⟧) (Algebra.commutes _ _)
