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

opaque instead of abstract in QuotientAlgebra #1078

Merged
merged 2 commits into from
Nov 17, 2023
Merged

opaque instead of abstract in QuotientAlgebra #1078

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
6d49dd2
replace non-breaking space by normal space
MatthiasHu Nov 8, 2023
a7a89cc
`abstract` -> `opaque` in QuotientAlgebra
MatthiasHu Nov 8, 2023
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
215 changes: 120 additions & 95 deletions Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,24 +31,24 @@ private
ℓ : Level

{-
The definition of the quotient algebra (_/_ below) is marked abstract to avoid
The definition of the quotient algebra (_/_ below) is marked opaque to avoid
long type checking times. All other definitions that need to "look into" this
abstract definition must be in the same abstract scope. Note that anonymous
modules share an abstract scope but named modules do not.
opaque definition must be in an opaque block that unfolds the definition of _/_.
-}

module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where abstract
module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where
open CommRingStr {{...}} hiding (_-_; -_; ·IdL ; ·DistR+) renaming (_·_ to _·R_; _+_ to _+R_)
open CommAlgebraStr {{...}}
open RingTheory (CommRing→Ring (CommAlgebra→CommRing A)) using (-DistR·)
instance
_ : CommRingStr ⟨ R ⟩
_ : CommRingStr ⟨ R ⟩
_ = snd R
_ : CommAlgebraStr R ⟨ A ⟩
_ = snd A

_/_ : CommAlgebra R ℓ
_/_ = commAlgebraFromCommRing
opaque
_/_ : CommAlgebra R ℓ
_/_ = commAlgebraFromCommRing
A/IAsCommRing
(λ r → elim (λ _ → squash/) (λ x → [ r ⋆ x ]) (eq r))
(λ r s → elimProp (λ _ → squash/ _ _)
Expand Down Expand Up @@ -83,16 +83,19 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where abstr
r ⋆ x - r ⋆ y ∎ )
(isCommIdeal.·Closed (snd I) _ x-y∈I))

quotientHom : CommAlgebraHom A (_/_)
fst quotientHom x = [ x ]
IsAlgebraHom.pres0 (snd quotientHom) = refl
IsAlgebraHom.pres1 (snd quotientHom) = refl
IsAlgebraHom.pres+ (snd quotientHom) _ _ = refl
IsAlgebraHom.pres· (snd quotientHom) _ _ = refl
IsAlgebraHom.pres- (snd quotientHom) _ = refl
IsAlgebraHom.pres⋆ (snd quotientHom) _ _ = refl
opaque
unfolding _/_

quotientHom : CommAlgebraHom A (_/_)
fst quotientHom x = [ x ]
IsAlgebraHom.pres0 (snd quotientHom) = refl
IsAlgebraHom.pres1 (snd quotientHom) = refl
IsAlgebraHom.pres+ (snd quotientHom) _ _ = refl
IsAlgebraHom.pres· (snd quotientHom) _ _ = refl
IsAlgebraHom.pres- (snd quotientHom) _ = refl
IsAlgebraHom.pres⋆ (snd quotientHom) _ _ = refl

module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where abstract
module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where
open CommRingStr {{...}}
hiding (_-_; -_; ·IdL; ·DistR+; is-set)
renaming (_·_ to _·R_; _+_ to _+R_)
Expand All @@ -104,21 +107,24 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where abstr
_ : CommAlgebraStr R ⟨ A ⟩
_ = snd A

-- sanity check / maybe a helper function some day
-- (These two rings are not definitionally equal, but only because of proofs, not data.)
CommForget/ : RingEquiv (CommAlgebra→Ring (A / I)) ((CommAlgebra→Ring A) Ring./ (CommIdeal→Ideal I))
fst CommForget/ = idEquiv _
IsRingHom.pres0 (snd CommForget/) = refl
IsRingHom.pres1 (snd CommForget/) = refl
IsRingHom.pres+ (snd CommForget/) = λ _ _ → refl
IsRingHom.pres· (snd CommForget/) = λ _ _ → refl
IsRingHom.pres- (snd CommForget/) = λ _ → refl
opaque
unfolding _/_

-- sanity check / maybe a helper function some day
-- (These two rings are not definitionally equal, but only because of proofs, not data.)
CommForget/ : RingEquiv (CommAlgebra→Ring (A / I)) ((CommAlgebra→Ring A) Ring./ (CommIdeal→Ideal I))
fst CommForget/ = idEquiv _
IsRingHom.pres0 (snd CommForget/) = refl
IsRingHom.pres1 (snd CommForget/) = refl
IsRingHom.pres+ (snd CommForget/) = λ _ _ → refl
IsRingHom.pres· (snd CommForget/) = λ _ _ → refl
IsRingHom.pres- (snd CommForget/) = λ _ → refl

module _
(B : CommAlgebra R ℓ)
(ϕ : CommAlgebraHom A B)
(I⊆kernel : (fst I) ⊆ (fst (kernel A B ϕ)))
where abstract
where

open IsAlgebraHom
open RingTheory (CommRing→Ring (CommAlgebra→CommRing B))
Expand All @@ -130,95 +136,114 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where abstr
_ : CommRingStr ⟨ B ⟩
_ = snd (CommAlgebra→CommRing B)

inducedHom : CommAlgebraHom (A / I) B
fst inducedHom =
rec is-set (λ x → fst ϕ x)
λ a b a-b∈I →
equalByDifference
(fst ϕ a) (fst ϕ b)
((fst ϕ a) - (fst ϕ b) ≡⟨ cong (λ u → (fst ϕ a) + u) (sym (IsAlgebraHom.pres- (snd ϕ) _)) ⟩
(fst ϕ a) + (fst ϕ (- b)) ≡⟨ sym (IsAlgebraHom.pres+ (snd ϕ) _ _) ⟩
fst ϕ (a - b) ≡⟨ I⊆kernel (a - b) a-b∈I ⟩
0r ∎)
pres0 (snd inducedHom) = pres0 (snd ϕ)
pres1 (snd inducedHom) = pres1 (snd ϕ)
pres+ (snd inducedHom) = elimProp2 (λ _ _ → is-set _ _) (pres+ (snd ϕ))
pres· (snd inducedHom) = elimProp2 (λ _ _ → is-set _ _) (pres· (snd ϕ))
pres- (snd inducedHom) = elimProp (λ _ → is-set _ _) (pres- (snd ϕ))
pres⋆ (snd inducedHom) = λ r → elimProp (λ _ → is-set _ _) (pres⋆ (snd ϕ) r)

inducedHom∘quotientHom : inducedHom ∘a quotientHom A I ≡ ϕ
inducedHom∘quotientHom = Σ≡Prop (isPropIsCommAlgebraHom {M = A} {N = B}) (funExt (λ a → refl))

injectivePrecomp : (B : CommAlgebra R ℓ) (f g : CommAlgebraHom (A / I) B)
→ f ∘a (quotientHom A I) ≡ g ∘a (quotientHom A I)
→ f ≡ g
injectivePrecomp B f g p =
Σ≡Prop
(λ h → isPropIsCommAlgebraHom {M = A / I} {N = B} h)
(descendMapPath (fst f) (fst g) is-set
λ x → λ i → fst (p i) x)
where
instance
_ : CommAlgebraStr R ⟨ B ⟩
_ = str B
opaque
unfolding _/_

inducedHom : CommAlgebraHom (A / I) B
fst inducedHom =
rec is-set (λ x → fst ϕ x)
λ a b a-b∈I →
equalByDifference
(fst ϕ a) (fst ϕ b)
((fst ϕ a) - (fst ϕ b) ≡⟨ cong (λ u → (fst ϕ a) + u) (sym (IsAlgebraHom.pres- (snd ϕ) _)) ⟩
(fst ϕ a) + (fst ϕ (- b)) ≡⟨ sym (IsAlgebraHom.pres+ (snd ϕ) _ _) ⟩
fst ϕ (a - b) ≡⟨ I⊆kernel (a - b) a-b∈I ⟩
0r ∎)
pres0 (snd inducedHom) = pres0 (snd ϕ)
pres1 (snd inducedHom) = pres1 (snd ϕ)
pres+ (snd inducedHom) = elimProp2 (λ _ _ → is-set _ _) (pres+ (snd ϕ))
pres· (snd inducedHom) = elimProp2 (λ _ _ → is-set _ _) (pres· (snd ϕ))
pres- (snd inducedHom) = elimProp (λ _ → is-set _ _) (pres- (snd ϕ))
pres⋆ (snd inducedHom) = λ r → elimProp (λ _ → is-set _ _) (pres⋆ (snd ϕ) r)

opaque
unfolding inducedHom quotientHom

inducedHom∘quotientHom : inducedHom ∘a quotientHom A I ≡ ϕ
inducedHom∘quotientHom = Σ≡Prop (isPropIsCommAlgebraHom {M = A} {N = B}) (funExt (λ a → refl))

opaque
unfolding quotientHom

injectivePrecomp : (B : CommAlgebra R ℓ) (f g : CommAlgebraHom (A / I) B)
→ f ∘a (quotientHom A I) ≡ g ∘a (quotientHom A I)
→ f ≡ g
injectivePrecomp B f g p =
Σ≡Prop
(λ h → isPropIsCommAlgebraHom {M = A / I} {N = B} h)
(descendMapPath (fst f) (fst g) is-set
λ x → λ i → fst (p i) x)
where
instance
_ : CommAlgebraStr R ⟨ B ⟩
_ = str B


{- trivial quotient -}
module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where abstract
module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where
open CommAlgebraStr (snd A)

oneIdealQuotient : CommAlgebraEquiv (A / (1Ideal A)) (UnitCommAlgebra R {ℓ' = ℓ})
fst oneIdealQuotient =
isoToEquiv (iso (fst (terminalMap R (A / (1Ideal A))))
(λ _ → [ 0a ])
(λ _ → isPropUnit* _ _)
(elimProp (λ _ → squash/ _ _)
λ a → eq/ 0a a tt*))
snd oneIdealQuotient = snd (terminalMap R (A / (1Ideal A)))

zeroIdealQuotient : CommAlgebraEquiv A (A / (0Ideal A))
fst zeroIdealQuotient =
let open RingTheory (CommRing→Ring (CommAlgebra→CommRing A))
in isoToEquiv (iso (fst (quotientHom A (0Ideal A)))
(rec is-set (λ x → x) λ x y x-y≡0 → equalByDifference x y x-y≡0)
(elimProp (λ _ → squash/ _ _) λ _ → refl)
λ _ → refl)
snd zeroIdealQuotient = snd (quotientHom A (0Ideal A))

-- non-abstract notation
opaque
unfolding _/_

oneIdealQuotient : CommAlgebraEquiv (A / (1Ideal A)) (UnitCommAlgebra R {ℓ' = ℓ})
fst oneIdealQuotient =
isoToEquiv (iso (fst (terminalMap R (A / (1Ideal A))))
(λ _ → [ 0a ])
(λ _ → isPropUnit* _ _)
(elimProp (λ _ → squash/ _ _)
λ a → eq/ 0a a tt*))
snd oneIdealQuotient = snd (terminalMap R (A / (1Ideal A)))

opaque
unfolding quotientHom

zeroIdealQuotient : CommAlgebraEquiv A (A / (0Ideal A))
fst zeroIdealQuotient =
let open RingTheory (CommRing→Ring (CommAlgebra→CommRing A))
in isoToEquiv (iso (fst (quotientHom A (0Ideal A)))
(rec is-set (λ x → x) λ x y x-y≡0 → equalByDifference x y x-y≡0)
(elimProp (λ _ → squash/ _ _) λ _ → refl)
λ _ → refl)
snd zeroIdealQuotient = snd (quotientHom A (0Ideal A))

[_]/ : {R : CommRing ℓ} {A : CommAlgebra R ℓ} {I : IdealsIn A}
→ (a : fst A) → fst (A / I)
[_]/ = fst (quotientHom _ _)



module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where abstract
module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where
open CommIdeal using (isPropIsCommIdeal)

private module _ where
-- non-abstract abbreviation
private
π : CommAlgebraHom A (A / I)
π = quotientHom A I

kernel≡I : kernel A (A / I) π ≡ I
kernel≡I =
kernel A (A / I) π ≡⟨ Σ≡Prop
(isPropIsCommIdeal (CommAlgebra→CommRing A))
refl ⟩
_ ≡⟨ CommRing.kernel≡I {R = CommAlgebra→CommRing A} I ⟩
I ∎
opaque
unfolding quotientHom

kernel≡I : kernel A (A / I) π ≡ I
kernel≡I =
kernel A (A / I) π ≡⟨ Σ≡Prop
(isPropIsCommIdeal (CommAlgebra→CommRing A))
refl ⟩
_ ≡⟨ CommRing.kernel≡I {R = CommAlgebra→CommRing A} I ⟩
I ∎


module _
{R : CommRing ℓ}
{A : CommAlgebra R ℓ}
{I : IdealsIn A}
where abstract
where

isZeroFromIdeal : (x : ⟨ A ⟩) → x ∈ (fst I) → fst (quotientHom A I) x ≡ CommAlgebraStr.0a (snd (A / I))
isZeroFromIdeal x x∈I = eq/ x 0a (subst (_∈ fst I) (step x) x∈I )
where
open CommAlgebraStr (snd A)
step : (x : ⟨ A ⟩) → x ≡ x - 0a
step = solve (CommAlgebra→CommRing A)
opaque
unfolding quotientHom

isZeroFromIdeal : (x : ⟨ A ⟩) → x ∈ (fst I) → fst (quotientHom A I) x ≡ CommAlgebraStr.0a (snd (A / I))
isZeroFromIdeal x x∈I = eq/ x 0a (subst (_∈ fst I) (step x) x∈I )
where
open CommAlgebraStr (snd A)
step : (x : ⟨ A ⟩) → x ≡ x - 0a
step = solve (CommAlgebra→CommRing A)