Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Simplify (and generalize) invElPropElimN #1102

Merged
merged 4 commits into from
Feb 16, 2024
Merged

Simplify (and generalize) invElPropElimN #1102

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
dc6b415
generalize equalizerLemma
MatthiasHu Feb 15, 2024
fb89c7c
also simplify ZariskiLattice.StructureSheaf a bit
MatthiasHu Feb 15, 2024
0d8b458
fix layout
MatthiasHu Feb 15, 2024
871eee7
Merge branch 'master' into generalize-equalizerLemma
MatthiasHu Feb 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 8 additions & 14 deletions Cubical/Algebra/CommRing/Localisation/InvertingElements.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -175,26 +175,22 @@ module InvertingElementsBase (R' : CommRing ℓ) where
1r · s · g ^ l ∎


invElPropElimN : (n : ℕ) (f : FinVec R (suc n)) (P : ((i : Fin (suc n)) → R[1/ (f i) ]) → Type ℓ')
invElPropElimN : (n : ℕ) (f : FinVec R n) (P : ((i : Fin n) → R[1/ (f i) ]) → Type ℓ')
→ (∀ x → isProp (P x))
→ (∀ (r : FinVec R (suc n)) (m : ℕ) → P (λ i → [ r i , (f i ^ m) , PT.∣ m , refl ∣₁ ]))
→ (∀ (r : FinVec R n) (m : ℕ) → P (λ i → [ r i , (f i ^ m) , PT.∣ m , refl ∣₁ ]))
-------------------------------------------------------------------------------------
→ ∀ x → P x
invElPropElimN zero f P isPropP baseCase x =
subst P (funExt (λ { zero → refl })) (invElPropElim {P = P'} (λ _ → isPropP _)
(λ r n → subst P (funExt (λ { zero → refl })) (baseCase (λ {zero → r}) n)) (x zero))
where
P' : R[1/ (f zero) ] → Type _
P' x = P (λ {zero → x})
subst P (funExt (λ ())) (baseCase (λ ()) zero)

invElPropElimN (suc n) f P isPropP baseCase x =
subst P (funExt (λ { zero → refl ; (suc i) → refl }))
(invElPropElimN n (f ∘ suc) P' (λ _ → isPropP _) baseCase' (x ∘ suc))
where
P' : ((i : Fin (suc n)) → R[1/ (f (suc i)) ]) → Type _
P' : ((i : Fin n) → R[1/ (f (suc i)) ]) → Type _
P' y = P (λ { zero → x zero ; (suc i) → y i })

baseCase' : ∀ (rₛ : FinVec R (suc n)) (m : ℕ)
baseCase' : ∀ (rₛ : FinVec R n) (m : ℕ)
→ P' (λ i → [ rₛ i , f (suc i) ^ m , ∣ m , refl ∣₁ ])
baseCase' rₛ m =
subst P (funExt (λ { zero → refl ; (suc i) → refl }))
Expand All @@ -209,15 +205,15 @@ module InvertingElementsBase (R' : CommRing ℓ) where
where
l = max m k

newEnumVec : FinVec R (suc (suc n))
newEnumVec : FinVec R (suc n)
newEnumVec zero = r₀ · (f zero) ^ (l ∸ k)
newEnumVec (suc i) = rₛ i · (f (suc i)) ^ (l ∸ m)

oldBaseVec : (i : Fin (suc (suc n))) → R[1/ (f i) ]
oldBaseVec : (i : Fin (suc n)) → R[1/ (f i) ]
oldBaseVec = λ { zero → [ r₀ , f zero ^ k , ∣ k , refl ∣₁ ]
; (suc i) → [ rₛ i , f (suc i) ^ m , ∣ m , (λ _ → f (suc i) ^ m) ∣₁ ] }

newBaseVec : (i : Fin (suc (suc n))) → R[1/ (f i) ]
newBaseVec : (i : Fin (suc n)) → R[1/ (f i) ]
newBaseVec zero = [ r₀ · (f zero) ^ (l ∸ k) , (f zero) ^ l , ∣ l , refl ∣₁ ]
newBaseVec (suc i) = [ rₛ i · (f (suc i)) ^ (l ∸ m) , (f (suc i)) ^ l , ∣ l , refl ∣₁ ]

Expand Down Expand Up @@ -292,8 +288,6 @@ module _ {A B : CommRing ℓ} (φ : CommRingHom A B) (f : fst A) where
(fst χ) ∘ (fst AU./1AsCommRingHom) ≡ (fst φ/1)
uniqInvElemHom = AU.invElemUniversalProp _ φ/1 (BU.S/1⊆S⁻¹Rˣ _ ∣ 1 , sym (·IdR _) ∣₁)



module _ (R : CommRing ℓ) (f : fst R) where
open CommRingTheory R
open RingTheory (CommRing→Ring R)
Expand Down
56 changes: 28 additions & 28 deletions Cubical/Algebra/CommRing/Localisation/Limit.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ private

-- were not dealing with case 0 here
-- but then R = 0 = lim {} (limit of the empty diagram)
module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') n) where
open isMultClosedSubset
open CommRingTheory R'
open RingTheory (CommRing→Ring R')
Expand All @@ -84,13 +84,13 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
module UP i j = S⁻¹RUniversalProp R' [ f i · f j ⁿ|n≥0] (powersFormMultClosedSubset (f i · f j))

-- some syntax to make things readable
0at : (i : Fin (suc n)) → R[1/ (f i) ]
0at : (i : Fin n) → R[1/ (f i) ]
0at i = R[1/ (f i) ]AsCommRing .snd .CommRingStr.0r

_/1ˢ : R → {i : Fin (suc n)} → R[1/ (f i) ]
_/1ˢ : R → {i : Fin n} → R[1/ (f i) ]
(r /1ˢ) {i = i} = U._/1 i r

_/1ᵖ : R → {i j : Fin (suc n)} → R[1/ (f i) · (f j) ]
_/1ᵖ : R → {i j : Fin n} → R[1/ (f i) · (f j) ]
(r /1ᵖ) {i = i} {j = j} = UP._/1 i j r


Expand All @@ -108,7 +108,7 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
→ x ≡ 0r
annihilatorHelper ann = recFin (is-set _ _) exponentHelper uIsPower
where
u : FinVec R (suc n)
u : FinVec R n
u i = ann i .fst .fst

uIsPower : ∀ i → u i ∈ₚ [ (f i) ⁿ|n≥0]
Expand All @@ -121,15 +121,15 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
→ x ≡ 0r
exponentHelper pows = PT.rec (is-set _ _) Σhelper (GeneratingPowers.thm R' l _ _ 1∈⟨f₀,⋯,fₙ⟩)
where
m : FinVec ℕ (suc n)
m : FinVec ℕ n
m i = pows i .fst

u≡fᵐ : ∀ i → u i ≡ f i ^ m i
u≡fᵐ i = pows i .snd

l = Max m

fˡ : FinVec R (suc n)
fˡ : FinVec R n
fˡ i = f i ^ l

fˡx≡0 : ∀ i → f i ^ l · x ≡ 0r
Expand All @@ -145,7 +145,7 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
0r ∎


Σhelper : Σ[ α ∈ FinVec R (suc n) ] 1r ≡ ∑ (λ i → α i · f i ^ l)
Σhelper : Σ[ α ∈ FinVec R n ] 1r ≡ ∑ (λ i → α i · f i ^ l)
→ x ≡ 0r
Σhelper (α , 1≡∑αfˡ) =
x ≡⟨ sym (·IdL _) ⟩
Expand All @@ -155,13 +155,13 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
(f i ^ l) x)) ⟩
∑ (λ i → α i · (f i ^ l · x)) ≡⟨ ∑Ext (λ i → cong (α i ·_) (fˡx≡0 i)) ⟩
∑ (λ i → α i · 0r) ≡⟨ ∑Ext (λ i → 0RightAnnihilates (α i)) ⟩
∑ (replicateFinVec (suc n) 0r) ≡⟨ ∑0r (suc n) ⟩
∑ (replicateFinVec n 0r) ≡⟨ ∑0r n ⟩
0r ∎


-- the morphisms into localisations of products from the left/right
-- we need to define them by hand as using RadicalLemma wouldn't compute later
χˡUnique : (i j : Fin (suc n))
χˡUnique : (i j : Fin n)
→ ∃![ χ ∈ CommRingHom R[1/ f i ]AsCommRing R[1/ f i · f j ]AsCommRing ]
(fst χ) ∘ (U._/1 i) ≡ (UP._/1 i j)
χˡUnique i j = U.S⁻¹RHasUniversalProp i _ (UP./1AsCommRingHom i j) unitHelper
Expand All @@ -175,10 +175,10 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
path : (n : ℕ) → 1r · (f i ^ n · f j ^ n) · 1r ≡ (1r · 1r) · (1r · ((f i · f j) ^ n))
path n = solve! R' ∙ sym (^-ldist-· (f i) (f j) n) ∙ solve! R'

χˡ : (i j : Fin (suc n)) → CommRingHom R[1/ f i ]AsCommRing R[1/ f i · f j ]AsCommRing
χˡ : (i j : Fin n) → CommRingHom R[1/ f i ]AsCommRing R[1/ f i · f j ]AsCommRing
χˡ i j = χˡUnique i j .fst .fst

χʳUnique : (i j : Fin (suc n))
χʳUnique : (i j : Fin n)
→ ∃![ χ ∈ CommRingHom R[1/ f j ]AsCommRing R[1/ f i · f j ]AsCommRing ]
(fst χ) ∘ (U._/1 j) ≡ (UP._/1 i j)
χʳUnique i j = U.S⁻¹RHasUniversalProp j _ (UP./1AsCommRingHom i j) unitHelper
Expand All @@ -192,14 +192,14 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
path : (n : ℕ) → 1r · (f j ^ n · f i ^ n) · 1r ≡ (1r · 1r) · (1r · ((f i · f j) ^ n))
path n = solve! R' ∙ sym (^-ldist-· (f i) (f j) n) ∙ solve! R'

χʳ : (i j : Fin (suc n)) → CommRingHom R[1/ f j ]AsCommRing R[1/ f i · f j ]AsCommRing
χʳ : (i j : Fin n) → CommRingHom R[1/ f j ]AsCommRing R[1/ f i · f j ]AsCommRing
χʳ i j = χʳUnique i j .fst .fst



-- super technical stuff, please don't look at it
private
χ≡Elim<Only : (x : (i : Fin (suc n)) → R[1/ f i ])
χ≡Elim<Only : (x : (i : Fin n) → R[1/ f i ])
→ (∀ i j → i < j → χˡ i j .fst (x i) ≡ χʳ i j .fst (x j))
→ ∀ i j → χˡ i j .fst (x i) ≡ χʳ i j .fst (x j)
χ≡Elim<Only x <hyp i j = aux (i ≟ j) -- doesn't type check in reasonable time using with syntax
Expand All @@ -218,32 +218,32 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
χˡsubst i j (x j) ≡⟨ sym (χSwapR→L i j (x j)) ⟩
χʳ i j .fst (x j) ∎
where
χʳsubst : (i j : Fin (suc n)) → R[1/ f i ] → R[1/ f i · f j ]
χʳsubst : (i j : Fin n) → R[1/ f i ] → R[1/ f i · f j ]
χʳsubst i j x = subst (λ r → R[1/ r ]) (·Comm (f j) (f i)) (χʳ j i .fst x)

χSwapL→R : ∀ i j x → χˡ i j .fst x ≡ χʳsubst i j x
χSwapL→R i j = invElPropElim (λ _ → squash/ _ _)
λ r m → cong [_] (ΣPathP (sym (transportRefl _) , Σ≡Prop (∈-isProp _)
(sym (transportRefl _ ∙ cong (λ x → 1r · transport refl (x ^ m)) (·Comm _ _)))))
χˡsubst : (i j : Fin (suc n)) → R[1/ f j ] → R[1/ f i · f j ]
χˡsubst : (i j : Fin n) → R[1/ f j ] → R[1/ f i · f j ]
χˡsubst i j x = subst (λ r → R[1/ r ]) (·Comm (f j) (f i)) (χˡ j i .fst x)

χSwapR→L : ∀ i j x → χʳ i j .fst x ≡ χˡsubst i j x
χSwapR→L i j = invElPropElim (λ _ → squash/ _ _)
λ r m → cong [_] (ΣPathP (sym (transportRefl _) , Σ≡Prop (∈-isProp _)
(sym (transportRefl _ ∙ cong (λ x → 1r · transport refl (x ^ m)) (·Comm _ _)))))

χ≡PropElim : {B : ((i : Fin (suc n)) → R[1/ f i ]) → Type ℓ''} (isPropB : ∀ {x} → isProp (B x))
→ (∀ (r : FinVec R (suc n)) (m l : ℕ)
χ≡PropElim : {B : ((i : Fin n) → R[1/ f i ]) → Type ℓ''} (isPropB : ∀ {x} → isProp (B x))
→ (∀ (r : FinVec R n) (m l : ℕ)
→ (∀ i j → r i · f j ^ m · (f i · f j) ^ l ≡ r j · f i ^ m · (f i · f j) ^ l)
→ B (λ i → [ r i , f i ^ m , ∣ m , refl ∣₁ ]))
-------------------------------------------------------------------------------------
→ (x : (i : Fin (suc n)) → R[1/ f i ])
→ (x : (i : Fin n) → R[1/ f i ])
→ (∀ i j → χˡ i j .fst (x i) ≡ χʳ i j .fst (x j))
→ B x
χ≡PropElim {B = B} isPropB baseHyp = invElPropElimN n f _ (λ _ → isProp→ isPropB) baseCase
where
baseCase : ∀ (r : FinVec R (suc n)) (m : ℕ)
baseCase : ∀ (r : FinVec R n) (m : ℕ)
→ (∀ i j → χˡ i j .fst ([ r i , f i ^ m , ∣ m , refl ∣₁ ])
≡ χʳ i j .fst ([ r j , f j ^ m , ∣ m , refl ∣₁ ]))
→ B (λ i → [ r i , f i ^ m , ∣ m , refl ∣₁ ])
Expand All @@ -269,7 +269,7 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
annihilatorHelper anns = recFin2 isPropB exponentHelper sIsPow
where
-- notation
s : (i j : Fin (suc n)) → R
s : (i j : Fin n) → R
s i j = anns i j .fst .fst

sIsPow : ∀ i j → s i j ∈ₚ [ (f i · f j) ⁿ|n≥0]
Expand Down Expand Up @@ -305,7 +305,7 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
exponentHelper pows = baseHyp r m (m +ℕ k) paths
where
-- sᵢⱼ = fᵢfⱼ ^ lᵢⱼ, so need to take max over all of these...
l : (i j : Fin (suc n)) → ℕ
l : (i j : Fin n) → ℕ
l i j = pows i j .fst

k = Max (λ i → Max (l i))
Expand Down Expand Up @@ -400,23 +400,23 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where

-- this will do all the heavy lifting
equalizerLemma : 1r ∈ ⟨f₀,⋯,fₙ⟩
→ ∀ (x : (i : Fin (suc n)) → R[1/ f i ]) -- s.t.
→ ∀ (x : (i : Fin n) → R[1/ f i ]) -- s.t.
→ (∀ i j → χˡ i j .fst (x i) ≡ χʳ i j .fst (x j))
→ ∃![ y ∈ R ] (∀ i → y /1ˢ ≡ x i)
equalizerLemma 1∈⟨f₀,⋯,fₙ⟩ = χ≡PropElim isProp∃! baseCase
where
baseCase : ∀ (r : FinVec R (suc n)) (m l : ℕ)
baseCase : ∀ (r : FinVec R n) (m l : ℕ)
→ (∀ i j → r i · f j ^ m · (f i · f j) ^ l ≡ r j · f i ^ m · (f i · f j) ^ l)
→ ∃![ y ∈ R ] (∀ i → y /1ˢ ≡ [ r i , f i ^ m , ∣ m , refl ∣₁ ])
baseCase r m l <Paths = PT.rec isProp∃! Σhelper (GeneratingPowers.thm R' 2m+l _ _ 1∈⟨f₀,⋯,fₙ⟩)
where
-- critical exponent
2m+l = m +ℕ (m +ℕ l)

f²ᵐ⁺ˡ : FinVec R (suc n)
f²ᵐ⁺ˡ : FinVec R n
f²ᵐ⁺ˡ i = f i ^ 2m+l

Σhelper : Σ[ α ∈ FinVec R (suc n) ] 1r ≡ linearCombination R' α f²ᵐ⁺ˡ
Σhelper : Σ[ α ∈ FinVec R n ] 1r ≡ linearCombination R' α f²ᵐ⁺ˡ
→ ∃![ y ∈ R ] (∀ i → y /1ˢ ≡ [ r i , f i ^ m , ∣ m , refl ∣₁ ])
Σhelper (α , linCombi) = (z , z≡r/fᵐ)
, λ y' → Σ≡Prop (λ _ → isPropΠ (λ _ → squash/ _ _)) (unique _ (y' .snd))
Expand Down Expand Up @@ -524,7 +524,7 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
open Cone
open Functor

locDiagram : Functor (DLShfDiag (suc n) ℓ) CommRingsCategory
locDiagram : Functor (DLShfDiag n ℓ) CommRingsCategory
F-ob locDiagram (sing i) = R[1/ f i ]AsCommRing
F-ob locDiagram (pair i j _) = R[1/ f i · f j ]AsCommRing
F-hom locDiagram idAr = idCommRingHom _
Expand All @@ -549,7 +549,7 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
instance
_ = snd A'

φ : (i : Fin (suc n)) → CommRingHom A' R[1/ f i ]AsCommRing
φ : (i : Fin n) → CommRingHom A' R[1/ f i ]AsCommRing
φ i = cᴬ .coneOut (sing i)

applyEqualizerLemma : ∀ a → ∃![ r ∈ R ] ∀ i → r /1ˢ ≡ φ i .fst a
Expand Down
35 changes: 8 additions & 27 deletions Cubical/Algebra/ZariskiLattice/StructureSheaf.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -211,28 +211,9 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
private instance _ = snd ZariskiLattice

isSheaf𝓞ᴮ : isDLBasisSheaf 𝓞ᴮ
isSheaf𝓞ᴮ {n = zero} α isBO⋁α A cᴬ = uniqueExists
(isTerminal𝓞ᴮ[0] A .fst)
(λ {(sing ()) ; (pair () _ _) }) -- the unique morphism is a cone morphism
(isPropIsConeMor _ _)
λ φ _ → isTerminal𝓞ᴮ[0] A .snd φ
where
-- D(0) is not 0 of the Zariski lattice by refl!
p : 𝓞ᴮ .F-ob (0l , isBO⋁α) ≡ R[1/ 0r ]AsCommRing
p = 𝓞ᴮ .F-ob (0l , isBO⋁α)
≡⟨ cong (𝓞ᴮ .F-ob) (Σ≡Prop (λ _ → ∈ₚ-isProp _ _)
(eq/ _ _ ((λ ()) , λ {zero → ∣ 1 , ∣ (λ ()) , 0LeftAnnihilates _ ∣₁ ∣₁ }))) ⟩
𝓞ᴮ .F-ob (D 0r , ∣ 0r , refl ∣₁)
≡⟨ 𝓞ᴮOb≡ 0r ⟩
R[1/ 0r ]AsCommRing ∎

isTerminal𝓞ᴮ[0] : isTerminal CommRingsCategory (𝓞ᴮ .F-ob (0l , isBO⋁α))
isTerminal𝓞ᴮ[0] = subst (isTerminal CommRingsCategory)
(sym (p ∙ R[1/0]≡0)) (TerminalCommRing .snd)

isSheaf𝓞ᴮ {n = suc n} α = curriedHelper (fst ∘ α) (snd ∘ α)
isSheaf𝓞ᴮ {n = n} α = curriedHelper (fst ∘ α) (snd ∘ α)
where
curriedHelper : (𝔞 : FinVec ZL (suc n)) (𝔞∈BO : ∀ i → 𝔞 i ∈ₚ BasicOpens)
curriedHelper : (𝔞 : FinVec ZL n) (𝔞∈BO : ∀ i → 𝔞 i ∈ₚ BasicOpens)
(⋁𝔞∈BO : ⋁ 𝔞 ∈ₚ BasicOpens)
→ isLimCone _ _ (F-cone 𝓞ᴮ
(condCone.B⋁Cone (λ i → 𝔞 i , 𝔞∈BO i) ⋁𝔞∈BO))
Expand All @@ -254,7 +235,7 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
open condCone (λ i → 𝔞 i , ∣ f i , Df≡𝔞 i ∣₁)
theSheafCone = B⋁Cone ∣ h , Dh≡⋁𝔞 ∣₁

DHelper : D h ≡ [ suc n , f ] --⋁ (D ∘ f)
DHelper : D h ≡ [ n , f ] --⋁ (D ∘ f)
DHelper = Dh≡⋁𝔞 ∙ ⋁Ext (λ i → sym (Df≡𝔞 i)) ∙ ⋁D≡ f

open Exponentiation R'
Expand All @@ -279,7 +260,7 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
ff∈√⟨h⟩ : ∀ i j → f i · f j ∈ √ ⟨ h ⟩ₛ
ff∈√⟨h⟩ i j = √ ⟨ h ⟩ₛ .snd .·Closed (f i) (f∈√⟨h⟩ j)

f/1 : FinVec (R[1/ h ]) (suc n)
f/1 : FinVec (R[1/ h ]) n
f/1 i = (f i) /1

1∈⟨f/1⟩ : 1r ∈ₕ ⟨ f/1 ⟩[ R[1/ h ]AsCommRing ]
Expand All @@ -291,9 +272,9 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
helper1 : (m : ℕ) → h ^ m ∈ ⟨ f ⟩[ R' ] → 1r ∈ₕ ⟨ f/1 ⟩[ R[1/ h ]AsCommRing ]
helper1 m = PT.map helper2
where
helper2 : Σ[ α ∈ FinVec R (suc n) ]
helper2 : Σ[ α ∈ FinVec R n ]
h ^ m ≡ linearCombination R' α f
→ Σ[ β ∈ FinVec R[1/ h ] (suc n) ]
→ Σ[ β ∈ FinVec R[1/ h ] n ]
1r ≡ linearCombination R[1/ h ]AsCommRing β f/1
helper2 (α , hᵐ≡∑αf) = β , path
where
Expand All @@ -306,7 +287,7 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
h⁻ᵐ = [ 1r , h ^ m , ∣ m , refl ∣₁ ]
, eq/ _ _ ((1r , containsOne) , solve! R')

β : FinVec R[1/ h ] (suc n)
β : FinVec R[1/ h ] n
β i = ((h ^ m) /1) ⁻¹ · α i /1

/1Path : (h ^ m) /1 ≡ ∑ (λ i → α i /1 · f i /1)
Expand Down Expand Up @@ -375,7 +356,7 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
(Σ≡Prop (λ _ → isPropPropTrunc) (cong (1r ·_) (transportRefl 1r) ∙ ·IdR 1r))))
(Σ≡Prop (λ _ → isPropPropTrunc) (cong (1r ·_) (transportRefl 1r) ∙ ·IdR 1r)))))

open LimitFromCommRing R' R[1/ h ]AsCommRing (DLShfDiag (suc n) ℓ)
open LimitFromCommRing R' R[1/ h ]AsCommRing (DLShfDiag n ℓ)
doubleLocDiag doubleLocCone /1/1Cone

-- get the desired cone in algebras:
Expand Down
Loading