Skip to content

Commit

Permalink
opaque instead of abstract in QuotientAlgebra (#1078)
Browse files Browse the repository at this point in the history 
* replace non-breaking space by normal space

* `abstract` -> `opaque` in QuotientAlgebra
@MatthiasHu
MatthiasHu authored Nov 17, 2023
1 parent 65e550f commit 3b2a50a
Showing 1 changed file with 120 additions and 95 deletions.
215 changes: 120 additions & 95 deletions Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda
View file
Original file line number Diff line number Diff line change
@@ -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/ _ _)
@@ -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_)
@@ -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))
@@ -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)

0 comments on commit 3b2a50a

Please sign in to comment.