English
Under hypotheses on R, S, S' and algebra maps between them, the construction mkOfAlgebra yields an IsLocalizedModule M f.toLinearMap with specified surjectivity and kernel properties.
Русский
При гипотезах над R, S, S' и алгебра-перемещениях между ними конструирование mkOfAlgebra даёт IsLocalizedModule M f.toLinearMap со заданными свойствами сюръективности и ядра.
LaTeX
$$$$ \\text{IsLocalizedModule } M f^{\\text{toLinearMap}} $$$$
Lean4
theorem mkOfAlgebra {R S S' : Type*} [CommSemiring R] [Ring S] [Ring S'] [Algebra R S] [Algebra R S'] (M : Submonoid R)
(f : S →ₐ[R] S') (h₁ : ∀ x ∈ M, IsUnit (algebraMap R S' x)) (h₂ : ∀ y, ∃ x : S × M, x.2 • y = f x.1)
(h₃ : ∀ x, f x = 0 → ∃ m : M, m • x = 0) : IsLocalizedModule M f.toLinearMap :=
by
replace h₃ := fun x =>
Iff.intro (h₃ x) fun ⟨⟨m, hm⟩, e⟩ =>
(h₁ m hm).mul_left_cancel <| by
rw [← Algebra.smul_def]
simpa [Submonoid.smul_def] using f.congr_arg e
constructor
· intro x
rw [Module.End.isUnit_iff]
constructor
· rintro a b (e : x • a = x • b)
simp_rw [Submonoid.smul_def, Algebra.smul_def] at e
exact (h₁ x x.2).mul_left_cancel e
· intro a
refine ⟨((h₁ x x.2).unit⁻¹ :) * a, ?_⟩
rw [Module.algebraMap_end_apply, Algebra.smul_def, ← mul_assoc, IsUnit.mul_val_inv, one_mul]
· exact h₂
· intro x y
dsimp only [AlgHom.toLinearMap_apply]
rw [← sub_eq_zero, ← map_sub, h₃]
simp_rw [smul_sub, sub_eq_zero]
exact id
