English
A function on X × S that is compatible with left expansion can be lifted to X[S⁻¹] consistently.
Русский
Функцию на X × S можно однозначно вытолкнуть в X[S⁻¹], если она совместима с левым разширением.
LaTeX
$$liftExpand : (P : X → S → C) → (∀ (r) (t) (s) (ht), P r s = P (t • r) ⟨t s, ht⟩) → X[S⁻¹] → C$$
Lean4
/-- A function or predicate over `X` and `S` can be lifted to `X[S⁻¹]` if it is invariant
under expansion on the left. -/
@[to_additive /-- A function or predicate over `X` and `S` can be lifted to the localization if it
is invariant under expansion on the left. -/
]
def liftExpand {C : Sort*} (P : X → S → C)
(hP : ∀ (r : X) (t : R) (s : S) (ht : t * s ∈ S), P r s = P (t • r) ⟨t * s, ht⟩) : X[S⁻¹] → C :=
Quotient.lift (fun p : X × S => P p.1 p.2) fun (r₁, s₁) (r₂, s₂) ⟨u, v, hr₂, hs₂⟩ =>
by
dsimp at *
have s₁vS : v * s₁ ∈ S := by
rw [← hs₂, ← S.coe_mul]
exact SetLike.coe_mem (u * s₂)
replace hs₂ : u * s₂ = ⟨_, s₁vS⟩ := by ext; simp [hs₂]
rw [hP r₁ v s₁ s₁vS, hP r₂ u s₂ (by norm_cast; rwa [hs₂]), ← hr₂]
simp only [← hs₂]; rfl
