English
There exists a two-argument lifting mechanism that extends a function P on X × S × X × S to the localized setting X[S⁻¹] × X[S⁻¹] → C, provided a coherence condition hP holds relating the two arguments via localization data.
Русский
Существует механизм подъёма двух аргументов, расширяющий функцию P на X × S × X × S до локализации X[S⁻¹] × X[S⁻¹] → C, при условии согласованности hP между двумя аргументами через данные локализации.
LaTeX
$$$lift_{2}^{\\mathrm{Expand}}: (X \\to S \\to X \\to S \\to C) \\to (\\text{coherence}) \\to X[S^{-1}] \\to X[S^{-1}] \\to C$$$
Lean4
/-- A version of `liftExpand` used to simultaneously lift functions with two arguments
in `X[S⁻¹]`. -/
@[to_additive /-- A version of `liftExpand` used to simultaneously lift functions with two arguments. -/
]
def lift₂Expand {C : Sort*} (P : X → S → X → S → C)
(hP :
∀ (r₁ : X) (t₁ : R) (s₁ : S) (ht₁ : t₁ * s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : S) (ht₂ : t₂ * s₂ ∈ S),
P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * s₂, ht₂⟩) :
X[S⁻¹] → X[S⁻¹] → C :=
liftExpand
(fun r₁ s₁ =>
liftExpand (P r₁ s₁) fun r₂ t₂ s₂ ht₂ =>
by
have := hP r₁ 1 s₁ (by simp) r₂ t₂ s₂ ht₂
simp [this])
fun r₁ t₁ s₁ ht₁ => by
ext x;
cases x with
| _ r₂ s₂
dsimp only
rw [liftExpand_of, liftExpand_of, hP r₁ t₁ s₁ ht₁ r₂ 1 s₂ (by simp)]; simp
