Skip to content

Commit

Permalink
Various cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
@hivert
hivert committed Jan 2, 2025
1 parent af27fb9 commit 7d804b9
Show file tree
Hide file tree
Showing 2 changed files with 58 additions and 45 deletions.
89 changes: 51 additions & 38 deletions theories/fps/dirlim.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,10 +64,10 @@ HB.builders Context
dlT of isDirLim_classical disp I Obj bonding Sys dlT.

Lemma cocone_dsyseq u :
cocone Sys (fun j (v : Obj j) => `[< dsysequal Sys u (DPair v) >]).
cocone Sys (fun j (v : Obj j) => `[< dsysequal Sys u (existT Obj j v) >]).
Proof.
move=> j k le_jk v /=.
case: (boolP `[< dsysequal Sys u (DPair v) >]) => /asboolP.
case: (boolP `[< dsysequal Sys u (existT Obj j v) >]) => /asboolP.
- move=> [l /= le_il le_jl Hbond]; apply/asboolP.
have [m le_km le_lm] := directedP k l.
apply: (Dsysequal (le_trans le_il le_lm)) => /=.
Expand All @@ -86,12 +86,11 @@ Lemma dirlim_eq i (u : Obj i) j (v : Obj j) :
Proof.
move=> eqinj.
apply contrapT; rewrite -forallNP => Hbond.
have Hcone := cocone_dsyseq (DPair v).
have /= := @dlind_commute _ _ Hcone j v; rewrite -eqinj.
have /= -> := (@dlind_commute _ _ Hcone i u).
move=> H; have {H} [_] := (asbool_eq_equiv H).
move/(_ (dsysequal_refl _ (DPair v))).
move=> [k le_jk le_ik Habs].
have Hcone := cocone_dsyseq (existT Obj j v).
have /= := dlind_commute Hcone v; rewrite -eqinj.
have /= -> := dlind_commute Hcone u.
move=> H; have {H} [_] := asbool_eq_equiv H.
move=> /(_ (dsysequal_refl _ (existT Obj j v))) [k le_jk le_ik Habs].
apply: (Hbond k); exists (le_ik); exists (le_jk); rewrite Habs.
exact: bondingE.
Qed.
Expand Down Expand Up @@ -130,7 +129,7 @@ Lemma dsyseqP u v : reflect (dsysequal Sys u v) (dsyseq Sys u v).
Proof. exact: asboolP. Qed.

Lemma dsyseq_bonding i j (le_ij : i <= j) (u : Obj i) :
dsyseq Sys (DPair u) (DPair (bonding le_ij u)).
dsyseq Sys (existT Obj i u) (existT Obj j (bonding le_ij u)).
Proof.
apply/dsyseqP; apply: (Dsysequal (k := j)) => /=.
by rewrite bonding_transE //; apply: bondingE.
Expand All @@ -146,10 +145,10 @@ Canonical SysEq :=
EquivRel (@dsyseq Sys) dsyseq_refl dsyseq_sym dsyseq_trans.

Lemma cocone_dsyseq u :
cocone Sys (fun j (v : Obj j) => dsyseq Sys u (DPair v)).
cocone Sys (fun j (v : Obj j) => dsyseq Sys u (existT Obj j v)).
Proof.
move=> j k le_jk v /=.
case: (boolP (dsyseq Sys u (DPair v))) => [/dsyseqP | /dsyseqP Hnthr].
case: (boolP (dsyseq Sys u (existT Obj j v))) => [/dsyseqP | /dsyseqP Hnthr].
- move=> [l /= le_il le_jl Hbond]; apply/asboolP.
have [m le_km le_lm] := directedP k l.
apply: (Dsysequal (le_trans le_il le_lm)) => /=.
Expand All @@ -165,7 +164,7 @@ Variable dlT : dirLimType Sys.
Implicit Type (x y z : dlT).

Lemma dsyseqE i j (u : Obj i) (v : Obj j) :
('inj[dlT] u == 'inj[dlT] v) = (dsyseq Sys (DPair u) (DPair v)).
('inj[dlT] u == 'inj[dlT] v) = (dsyseq Sys (existT Obj i u) (existT Obj j v)).
Proof. exact/dirlimE/dsyseqP. Qed.

End DirSysCongr.
Expand Down Expand Up @@ -221,7 +220,23 @@ HB.instance Definition _ :=
HB.end.


(** ComUnitRingInvLim is just a join *)
HB.factory Record DirLim_isComUnitRingDirLim
(disp : unit) (I : dirType disp)
(Obj : I -> comUnitRingType)
(bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
(Sys : is_dirsys bonding)
dlT of DirLim _ Sys dlT := {}.
HB.builders Context
(disp : unit) (I : dirType disp)
(Obj : I -> comUnitRingType)
(bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
(Sys : is_dirsys bonding)
dlT of DirLim_isComUnitRingDirLim _ _ _ _ Sys dlT.

HB.instance Definition _ := DirLim_isUnitRingDirLim.Build _ _ _ _ Sys dlT.
HB.instance Definition _ :=
SemiRingDirLim_isComSemiRingDirLim.Build _ _ _ _ Sys dlT.
HB.end.


HB.factory Record DirLim_isIDomainDirLim
Expand All @@ -240,9 +255,7 @@ HB.builders Context
Implicit Type x y : dlT.

HB.instance Definition _ :=
DirLim_isUnitRingDirLim.Build _ _ _ _ Sys dlT.
HB.instance Definition _ :=
SemiRingDirLim_isComSemiRingDirLim.Build _ _ _ _ Sys dlT.
DirLim_isComUnitRingDirLim.Build _ _ _ _ Sys dlT.
HB.instance Definition _ :=
ComUnitRingDirLim_isIntegralDirLim.Build _ _ _ _ Sys dlT.

Expand Down Expand Up @@ -286,7 +299,7 @@ Variable bonding : forall i j, i <= j -> Obj i -> Obj j.
Variable Sys : is_dirsys bonding.

Definition dirlim := {eq_quot (dsyseq Sys)}.
Definition dlinj_impl i (u : Obj i) := \pi_dirlim (DPair u).
Definition dlinj_impl i (u : Obj i) := \pi_dirlim (existT Obj i u).

HB.instance Definition _ := Choice.on dirlim.

Expand All @@ -304,8 +317,8 @@ Variable Sys : is_dirsys bonding.
Implicit Type (i j k : I) (x y : {dirlim Sys}).

Lemma dsyseq_dlinj_impl i (u : Obj i) :
dsyseq Sys (DPair u) (repr (dlinj_impl Sys u)).
Proof. by have [v /eqmodP] := piP {dirlim Sys} (DPair u). Qed.
dsyseq Sys (existT Obj i u) (repr (dlinj_impl Sys u)).
Proof. by have [v /eqmodP] := piP {dirlim Sys} (existT Obj i u). Qed.

(** Budlding the universal induced map *)
Section UniversalProperty.
Expand All @@ -323,7 +336,7 @@ by case: (repr _) (dsyseq_dlinj_impl u).
Qed.

Lemma dlind_implE i j (u : Obj i) (v : Obj j) :
dsyseq Sys (DPair u) (DPair v) ->
dsyseq Sys (existT Obj i u) (existT Obj j v) ->
dlind_impl Hcone (dlinj_impl Sys u) = dlind_impl Hcone (dlinj_impl Sys v).
Proof. by rewrite !dlind_implP => /dsyseqP/(dsysequalE Hcone). Qed.

Expand Down Expand Up @@ -429,6 +442,24 @@ HB.instance Definition _ := GRing.ComRing.on {dirlim Sys}.
Let test : comUnitRingDirLimType _ := {dirlim Sys}.
End ComUnitRing.

Section IDomain.
Variable Obj : I -> idomainType.
Variable bonding : forall i j, (i <= j)%O -> {rmorphism Obj i -> Obj j}.
Variable Sys : is_dirsys bonding.
HB.instance Definition _ :=
DirLim_isIDomainDirLim.Build _ _ _ _ Sys {dirlim Sys}.
Let test : idomainDirLimType _ := {dirlim Sys}.
End IDomain.

Section Field.
Variable Obj : I -> fieldType.
Variable bonding : forall i j, (i <= j)%O -> {rmorphism Obj i -> Obj j}.
Variable Sys : is_dirsys bonding.
HB.instance Definition _ :=
DirLim_isFieldDirLim.Build _ _ _ _ Sys {dirlim Sys}.
Let test : fieldDirLimType _ := {dirlim Sys}.
End Field.

Section Linear.
Variables (R : ringType).
Variable Obj : I -> lmodType R.
Expand Down Expand Up @@ -480,24 +511,6 @@ Variable Sys : is_dirsys bonding.
HB.instance Definition _ := GRing.Algebra.on {dirlim Sys}.
End ComUnitAlg.

Section IDomain.
Variable Obj : I -> idomainType.
Variable bonding : forall i j, (i <= j)%O -> {rmorphism Obj i -> Obj j}.
Variable Sys : is_dirsys bonding.
HB.instance Definition _ :=
DirLim_isIDomainDirLim.Build _ _ _ _ Sys {dirlim Sys}.
Let test : idomainDirLimType _ := {dirlim Sys}.
End IDomain.

Section Field.
Variable Obj : I -> fieldType.
Variable bonding : forall i j, (i <= j)%O -> {rmorphism Obj i -> Obj j}.
Variable Sys : is_dirsys bonding.
HB.instance Definition _ :=
DirLim_isFieldDirLim.Build _ _ _ _ Sys {dirlim Sys}.
Let test : fieldDirLimType _ := {dirlim Sys}.
End Field.

End Instances.


Expand Down
14 changes: 7 additions & 7 deletions theories/fps/dirlim_constr.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,6 @@ Proof. by rewrite /cocone => H i j le_ij u; rewrite -(H i j le_ij). Qed.


Implicit Types (i j k : I) (u v : {i : I & Obj i}).
Definition DPair i (u : Obj i) := (existT Obj i u).

Inductive dsysequal (Sys : is_dirsys) u v : Prop :=
| Dsysequal : forall k (le_ik : projT1 u <= k) (le_jk : projT1 v <= k),
Expand All @@ -94,7 +93,7 @@ Local Arguments Dsysequal {Sys u v k} (le_ik le_jk).
Variable Sys : is_dirsys.

Lemma dsysequal_bonding i j (le_ij : i <= j) (u : Obj i) :
dsysequal Sys (DPair u) (DPair (bonding le_ij u)).
dsysequal Sys (existT Obj i u) (existT Obj j (bonding le_ij u)).
Proof.
apply: (Dsysequal (k := j)) => /=.
by rewrite bonding_transE //; apply: bondingE.
Expand Down Expand Up @@ -126,7 +125,7 @@ Variables (T : Type) (f : forall i, Obj i -> T).
Hypothesis Hcone : cocone Sys f.

Lemma dsysequalE i j (u : Obj i) (v : Obj j) :
dsysequal Sys (DPair u) (DPair v) -> f u = f v.
dsysequal Sys (existT Obj i u) (existT Obj j v) -> f u = f v.
Proof.
move=> [k le_ik le_jk Hbond].
by rewrite -(coconeE Hcone le_ik) Hbond (coconeE Hcone).
Expand Down Expand Up @@ -237,7 +236,7 @@ Proof.
suff : { p : {i & Obj i} | 'inj (projT2 p) == x }.
by move=> [p /eqP Heq]; exists p.
apply: sigW => /=; have [i[u] <-{x}]:= dirlim_surj x.
by exists (DPair u).
by exists (existT Obj i u).
Qed.
Lemma dirlimS2P x y :
{ p : {i & (Obj i * Obj i)%type} |
Expand Down Expand Up @@ -274,8 +273,9 @@ Variable Sys : is_dirsys bonding.
Variable dlT : dirLimType Sys.
Implicit Type (x y z : dlT).

Lemma dirlimE i j (u : Obj i) (v : Obj j) :
reflect (dsysequal Sys (DPair u) (DPair v)) ('inj[dlT] u == 'inj[dlT] v).
Lemma dirlimE i j (u : Obj i) (v : Obj j) : reflect
(dsysequal Sys (existT Obj i u) (existT Obj j v))
('inj[dlT] u == 'inj[dlT] v).
Proof.
apply (iffP eqP).
by move/(dirlim_eq i u j v) => [k] [ik] [jk] Heq; exists k ik jk.
Expand Down Expand Up @@ -1134,7 +1134,7 @@ move/dlunit_decP => H.
suff : {p : {i & Obj i} |
('inj[dlT] (projT2 p) == x) && (projT2 p \is a GRing.unit)}.
by move=> [p] /andP[/eqP H1 H2]; exists p.
apply: sigW; move: H => /= [i][u][<-{x} Hunit]; exists (DPair u) => /=.
apply: sigW; move: H => /= [i][u][<-{x} Hunit]; exists (existT Obj i u).
by rewrite eq_refl Hunit.
Qed.

Expand Down

0 comments on commit 7d804b9

Please sign in to comment.