English
There is a compatible scalar-tower structure in the natural lift along kernels of algebra maps, also when using natural numbers indexing.
Русский
Существуют совместимые скалярные структуры в естественном подъёме через ядра алгебраических отображений, включая индексы по естественным числам.
LaTeX
$$IsScalarTower R A B$$
Lean4
/-- The map `I/I² → J/J²` if `I ≤ f⁻¹(J)`. -/
def mapCotangent (I₁ : Ideal A) (I₂ : Ideal B) (f : A →ₐ[R] B) (h : I₁ ≤ I₂.comap f) :
I₁.Cotangent →ₗ[R] I₂.Cotangent :=
by
refine
Submodule.mapQ ((I₁ • ⊤ : Submodule A I₁).restrictScalars R) ((I₂ • ⊤ : Submodule B I₂).restrictScalars R) ?_ ?_
· exact f.toLinearMap.restrict (p := I₁.restrictScalars R) (q := I₂.restrictScalars R) h
· intro x hx
rw [Submodule.restrictScalars_mem] at hx
refine Submodule.smul_induction_on hx ?_ (fun _ _ ↦ add_mem)
rintro a ha ⟨b, hb⟩ -
simp only [SetLike.mk_smul_mk, smul_eq_mul, Submodule.mem_comap, Submodule.restrictScalars_mem]
convert (Submodule.smul_mem_smul (M := I₂) (r := f a) (n := ⟨f b, h hb⟩) (h ha) (Submodule.mem_top)) using 1
ext
exact map_mul f a b
