English
For any P and coherence hP, the lift₂Expand operator is well-defined and respects the two-argument lifting in the Ore localization framework.
Русский
Для любого P и согласованности hP оператор lift₂Expand корректен и соблюдает подъём двух аргументов в рамках локализации Ore.
LaTeX
$$The two-argument lift on OreLocalization is well-defined and functorial in its arguments.$$
Lean4
/-- The scalar multiplication on the Ore localization of monoids. -/
@[to_additive (attr := irreducible) /-- the vector addition on the Ore localization of additive monoids. -/
]
protected def smul : R[S⁻¹] → X[S⁻¹] → X[S⁻¹] :=
liftExpand smul'' fun r₁ r₂ s hs => by
ext x
cases x with
| _ x s₂
change OreLocalization.smul' r₁ s x s₂ = OreLocalization.smul' (r₂ * r₁) ⟨_, hs⟩ x s₂
rcases oreCondition r₁ s₂ with ⟨r₁', s₁', h₁⟩
rw [smul'_char _ _ _ _ _ _ h₁]
rcases oreCondition (r₂ * r₁) s₂ with ⟨r₂', s₂', h₂⟩
rw [smul'_char _ _ _ _ _ _ h₂]
rcases oreCondition (s₂' * r₂) (s₁') with ⟨r₃', s₃', h₃⟩
have : s₃' * r₂' * s₂ = r₃' * r₁' * s₂ := by
rw [mul_assoc, ← h₂, ← mul_assoc _ r₂, ← mul_assoc, h₃, mul_assoc, h₁, mul_assoc]
rcases ore_right_cancel _ _ _ this with ⟨s₄', h₄⟩
have : (s₄' * r₃') * (s₁' * s) ∈ S :=
by
rw [← mul_assoc, mul_assoc _ r₃', ← h₃, ← mul_assoc, ← mul_assoc, mul_assoc]
exact mul_mem (s₄' * s₃' * s₂').2 hs
rw [OreLocalization.expand' (r₂' • x) _ (s₄' * s₃'), OreLocalization.expand _ _ _ this]
simp only [Submonoid.smul_def, Submonoid.coe_mul, smul_smul, mul_assoc, h₄]
congr 1
ext; simp only [Submonoid.coe_mul, ← mul_assoc]
rw [mul_assoc _ r₃', ← h₃, ← mul_assoc, ← mul_assoc]
