From 9f9f44b725ffdaf735f525a3ed35766870548666 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 12 Sep 2024 20:13:00 +0200 Subject: [PATCH 01/28] localizations of commutative rings Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/CRing.v | 13 + theories/Algebra/Rings/Localization.v | 620 ++++++++++++++++++++++++++ theories/Algebra/Rings/Ring.v | 67 ++- theories/Modalities/Descent.v | 2 +- theories/Modalities/Lex.v | 2 +- theories/Modalities/Nullification.v | 2 +- 6 files changed, 702 insertions(+), 4 deletions(-) create mode 100644 theories/Algebra/Rings/Localization.v diff --git a/theories/Algebra/Rings/CRing.v b/theories/Algebra/Rings/CRing.v index fd803e35f42..238d81a2936 100644 --- a/theories/Algebra/Rings/CRing.v +++ b/theories/Algebra/Rings/CRing.v @@ -56,6 +56,19 @@ Proof. f_ap. Defined. +Definition rng_mult_move_left_assoc {R : CRing} (x y z : R) + : x * y * z = y * x * z. +Proof. + f_ap; apply rng_mult_comm. +Defined. + +Definition rng_mult_move_right_assoc {R : CRing} (x y z : R) + : x * (y * z) = y * (x * z). +Proof. + refine (rng_mult_assoc _ _ _ @ _ @ (rng_mult_assoc _ _ _)^). + apply rng_mult_move_left_assoc. +Defined. + (** ** Ideals in commutative rings *) Section IdealCRing. diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v new file mode 100644 index 00000000000..3581ef5ed05 --- /dev/null +++ b/theories/Algebra/Rings/Localization.v @@ -0,0 +1,620 @@ +Require Import Basics.Overture Basics.Trunc Basics.Tactics WildCat.Core + abstract_algebra Rings.CRing Truncations.Core Nat.Core. + +Local Open Scope mc_scope. + +(** * Localizaiton of commutative rings *) + +(** ** Localization is a way to make elements in a commutative ring invertible by adding inverses, in the most minimal way possible. It generalizes the familar operation of a field of fractions. *) + +(** ** Multiplicative subsets *) + +(** A multiplicative subset is formally a submonoid of the multiplicative monoid of a ring. Essentially it is a subset closed under finite products. *) + +(** *** Definition *) + +(** Multiplicative subsets of a ring [R] consist of: *) +Class IsMultiplicativeSubset {R : CRing} (S : R -> Type) : Type := { + (** Contains one *) + mss_one : S 1 ; + (** Closed under multiplication *) + mss_mult : forall x y, S x -> S y -> S (x * y) ; +}. + +Arguments mss_one {R _ _}. +Arguments mss_mult {R _ _ _ _}. + +(** *** Examples *) + +(** The multplicative subset of powers of a ring element. *) +Global Instance ismultiplicative_powers (R : CRing) (x : R) + : IsMultiplicativeSubset (fun r => exists n, rng_power x n = r). +Proof. + srapply Build_IsMultiplicativeSubset. + 1: by exists 0%nat. + intros a b np mq. + destruct np as [n p], mq as [m q]. + exists (n + m)%nat. + lhs_V nrapply rng_power_mult_law. + f_ap. +Defined. + +(** Invertible elements of a ring form a multiplicative subset. *) +Global Instance ismultiplicative_isinvertible (R : CRing) + : IsMultiplicativeSubset (@IsInvertible R) := {}. + +(** TODO: Property of being a localization. *) + +(** ** Construction of localization. *) + +Section Localization. + + (** We now construct the localization of a ring at a multiplicative subset as the following HIT: + + <<< + HIT Localization_type (R : CRing) (S : R -> Type) + `{IsMultiplicativeSubset R} := + | loc_frac (n d : R) (p : S d) : Localization R S + | loc_frac_eq (n1 d1 n2 d2 : R) (p1 : S d1) (p2 : S d2) + (x : R) (q : S x) (r : x * (d2 * n1 - n2 * d1) = 0) + : loc_frac n1 d1 p1 = loc_frac n2 d2 p2 + . + >>> + + We will implement this HIT by writing it as a quotient. + *) + + Context (R : CRing) (S : R -> Type) `{!IsMultiplicativeSubset S}. + + (** *** Construction of underlying Localization type *) + + (** The base type will be the type of fractions with respect to a multiplicative subset. This consists of pairs of elements of a ring [R] where the [denominator] is in the multiplicative subset [S]. *) + Record Fraction := { + numerator : R ; + denominator : R ; + in_mult_subset_denominator : S denominator ; + }. + + Definition fraction_eq : Relation Fraction. + Proof. + intros [n1 d1 ?] [n2 d2 ?]. + refine (exists (x : R), S x /\ _). + exact (x * (n1 * d2 - n2 * d1) = 0). + Defined. + + (** It is convenient to produce elements of this relation specalized to when the scaling factor is 1 *) + Definition fraction_eq_simple f1 f2 + (p : numerator f1 * denominator f2 = numerator f2 * denominator f1) + : fraction_eq f1 f2. + Proof. + exists 1. + refine (mss_one ,_). + refine (rng_mult_one_l _ @ _). + by apply rng_moveL_0M^-1. + Defined. + + Definition fraction_eq_refl f1 : fraction_eq f1 f1. + Proof. + apply fraction_eq_simple. + reflexivity. + Defined. + + Definition Localization_type : Type := Quotient fraction_eq. + + Definition loc_frac : Fraction -> Localization_type + := class_of fraction_eq. + + Definition loc_frac_eq {f1 f2 : Fraction} (p : fraction_eq f1 f2) + : loc_frac f1 = loc_frac f2 + := qglue p. + + Definition Localization_type_ind (Q : Localization_type -> Type) + `{forall x, IsHSet (Q x)} + (frac : forall f, Q (loc_frac f)) + (eq : forall f1 f2 p, loc_frac_eq p # frac f1 = frac f2) + : forall x, Q x + := Quotient_ind _ Q frac eq. + + Definition Localization_type_ind_hprop (Q : Localization_type -> Type) + `{forall x, IsHProp (Q x)} (f : forall f, Q (loc_frac f)) + : forall x, Q x + := Quotient_ind_hprop _ Q f. + + Definition Localization_type_rec (Q : Type) `{IsHSet Q} + (f : Fraction -> Q) + (t : forall f1 f2, fraction_eq f1 f2 -> f f1 = f f2) + : Localization_type -> Q + := Quotient_rec _ Q f t. + + Arguments loc_frac : simpl never. + Arguments loc_frac_eq : simpl never. + + (** Elements of [R] can be considered fractions. *) + Definition frac_in : R -> Fraction + := fun r => Build_Fraction r 1 mss_one. + + (** Now that we have defined the HIT as above, we can define the ring structure. *) + + (** *** Addition operation *) + + (** Fraction addition *) + Definition frac_add : Fraction -> Fraction -> Fraction := + fun '(Build_Fraction n1 d1 p1) '(Build_Fraction n2 d2 p2) + => Build_Fraction (n1 * d2 + n2 * d1) (d1 * d2) (mss_mult p1 p2). + + (** Fraction addition is well-defined upto equality of fractions. *) + + (** It is easier to prove well-definedness of both arguments at once. *) + Definition frac_add_wd (f1 f1' f2 f2' : Fraction) + (p : fraction_eq f1 f1') (q : fraction_eq f2 f2') + : fraction_eq (frac_add f1 f2) (frac_add f1' f2'). + Proof. + destruct f1 as [a s ss], f1' as [a' s' ss'], + f2 as [b t st], f2' as [b' t' st'], + p as [x [sx p]], q as [y [sy q]]. + refine (x * y ; (mss_mult sx sy, _)). + simpl. + rewrite rng_dist_l_negate. + rewrite 2 rng_dist_r. + rewrite 2 rng_dist_l. + rewrite <- rng_plus_assoc. + rewrite (rng_plus_comm _ (- _)). + rewrite rng_negate_plus. + rewrite 2 rng_plus_assoc. + rewrite <- (rng_plus_assoc _ (- _)). + rewrite (rng_plus_comm (- _)). + rewrite <- 2 rng_dist_l_negate. + rewrite <- ? rng_mult_assoc. + rewrite 2 (rng_mult_move_right_assoc a'). + rewrite (rng_mult_comm a' t). + rewrite (rng_mult_move_right_assoc s). + rewrite (rng_mult_comm s a'). + rewrite (rng_mult_move_right_assoc t). + rewrite (rng_mult_comm t t'). + rewrite <- 2 (rng_mult_move_right_assoc t'). + rewrite <- (rng_dist_l_negate t'). + rewrite (rng_mult_comm _ t). + rewrite (rng_mult_move_right_assoc _ t). + rewrite <- (rng_dist_l_negate t). + rewrite <- 2 (rng_mult_move_right_assoc t'). + rewrite <- 2 (rng_mult_move_right_assoc t). + rewrite (rng_mult_move_right_assoc x). + rewrite p. + rewrite 3 rng_mult_zero_r. + rewrite rng_plus_zero_l. + rewrite 2 (rng_mult_move_right_assoc b). + rewrite 2 (rng_mult_move_right_assoc b'). + rewrite (rng_mult_move_right_assoc s). + rewrite <- 2 rng_dist_l_negate. + rewrite 2 (rng_mult_move_right_assoc y). + rewrite q. + by rewrite 3 rng_mult_zero_r. + Qed. + + Definition frac_add_wd_l (f1 f1' f2 : Fraction) (p : fraction_eq f1 f1') + : fraction_eq (frac_add f1 f2) (frac_add f1' f2). + Proof. + pose (fraction_eq_refl f2). + by apply frac_add_wd. + Defined. + + Definition frac_add_wd_r (f1 f2 f2' : Fraction) (p : fraction_eq f2 f2') + : fraction_eq (frac_add f1 f2) (frac_add f1 f2'). + Proof. + pose (fraction_eq_refl f1). + by apply frac_add_wd. + Defined. + + (** The addition operation for fractions is the usual fraction addition. Most of the work is spent showing that this is well-defined. *) + Instance plus_localization_type : Plus Localization_type. + Proof. + intros x; srapply Localization_type_rec. + { intros f2; revert x. + srapply Localization_type_rec. + { intros f1. + apply loc_frac. + exact (frac_add f1 f2). } + intros f1 f1' p. + by apply loc_frac_eq, frac_add_wd_l. } + intros f2 f2' p; revert x; cbn. + srapply Localization_type_ind_hprop. + intros f1. + by apply loc_frac_eq, frac_add_wd_r. + Defined. + + (** *** Multiplication operation *) + + Definition frac_mult : Fraction -> Fraction -> Fraction := + fun '(Build_Fraction n1 d1 p1) '(Build_Fraction n2 d2 p2) + => Build_Fraction (n1 * n2) (d1 * d2) (mss_mult p1 p2). + + Definition frac_mult_wd_l f1 f1' f2 (p : fraction_eq f1 f1') + : fraction_eq (frac_mult f1 f2) (frac_mult f1' f2). + Proof. + destruct p as [x [s p]]. + refine (x; (s, _)); simpl. + rewrite rng_dist_l. + rewrite rng_dist_l in p. + rewrite rng_mult_negate_r. + rewrite rng_mult_negate_r in p. + apply rng_moveL_0M in p. + apply rng_moveL_0M^-1. + rewrite 2 (rng_mult_comm _ (numerator f2)). + rewrite 2 (rng_mult_comm _ (denominator f2)). + rewrite <- 2 (rng_mult_assoc (numerator f2)). + rewrite 2 (rng_mult_comm (numerator _) (denominator f2 * _)). + rewrite ? (rng_mult_assoc (numerator f2)). + rewrite <- ? (rng_mult_assoc (numerator f2 * denominator f2)). + rewrite 2 (rng_mult_comm (denominator _) (numerator _)). + rewrite 2 (rng_mult_comm (numerator f2 * denominator f2)). + rewrite 2 (rng_mult_assoc x (numerator _ * denominator _)). + f_ap. + Defined. + + Definition frac_mult_wd_r f1 f2 f2' (p : fraction_eq f2 f2') + : fraction_eq (frac_mult f1 f2) (frac_mult f1 f2'). + Proof. + destruct p as [x [s p]]. + refine (x; (s, _)); simpl. + rewrite rng_dist_l. + rewrite rng_dist_l in p. + rewrite rng_mult_negate_r. + rewrite rng_mult_negate_r in p. + apply rng_moveL_0M in p. + apply rng_moveL_0M^-1. + rewrite 2 (rng_mult_comm (numerator f1)). + rewrite <- 2 rng_mult_assoc. + rewrite 2 (rng_mult_comm (numerator f1)). + rewrite <- ? rng_mult_assoc. + rewrite 2 (rng_mult_move_right_assoc (denominator f1)). + rewrite ? rng_mult_assoc. + rewrite ? rng_mult_assoc in p. + do 2 f_ap. + Defined. + + Instance mult_localization_type : Mult Localization_type. + Proof. + intros x; srapply Localization_type_rec. + { intros f2; revert x. + srapply Localization_type_rec. + { intros f1. + apply loc_frac. + exact (frac_mult f1 f2). } + intros f1 f1' p. + by apply loc_frac_eq, frac_mult_wd_l. } + intros f2 f2' p; revert x. + srapply Localization_type_ind_hprop. + intros f1. + by apply loc_frac_eq, frac_mult_wd_r. + Defined. + + (** *** Zero element *) + + Instance zero_localization_type : Zero Localization_type := + loc_frac (Build_Fraction 0 1 mss_one). + + (** *** One element *) + + Instance one_localization_type : One Localization_type := + loc_frac (Build_Fraction 1 1 mss_one). + + (** *** Negation operation *) + + Definition frac_negate : Fraction -> Fraction := + fun '(Build_Fraction n d p) => Build_Fraction (- n) d p. + + Definition frac_negate_wd f1 f2 (p : fraction_eq f1 f2) + : fraction_eq (frac_negate f1) (frac_negate f2). + Proof. + destruct p as [x [s p]]. + refine (x; (s,_)); simpl. + rewrite 2 rng_mult_negate_l. + rewrite <- rng_negate_plus. + rewrite rng_mult_negate_r. + rewrite p. + apply rng_negate_zero. + Defined. + + Instance negate_localization_type : Negate Localization_type. + Proof. + srapply Localization_type_rec. + { intros f. + apply loc_frac. + exact (frac_negate f). } + intros f1 f2 p. + by apply loc_frac_eq, frac_negate_wd. + Defined. + + (** *** Ring laws *) + + (** Left additive identity *) + Instance leftidentity_plus_localization_type + : LeftIdentity plus_localization_type zero_localization_type. + Proof. + srapply Localization_type_ind_hprop; intros f. + apply loc_frac_eq, fraction_eq_simple; simpl. + f_ap. + - rewrite rng_mult_zero_l. + rewrite rng_plus_zero_l. + apply rng_mult_one_r. + - symmetry. + apply rng_mult_one_l. + Defined. + + Instance rightidentity_plus_localization_type + : RightIdentity plus_localization_type zero_localization_type. + Proof. + srapply Localization_type_ind_hprop; intros f. + apply loc_frac_eq, fraction_eq_simple; simpl. + f_ap. + - rewrite rng_mult_zero_l. + rewrite rng_plus_zero_r. + apply rng_mult_one_r. + - symmetry. + apply rng_mult_one_r. + Defined. + + Instance leftinverse_plus_localization_type + : LeftInverse plus_localization_type negate_localization_type zero_localization_type. + Proof. + srapply Localization_type_ind_hprop; intros f. + apply loc_frac_eq, fraction_eq_simple; simpl. + refine (rng_mult_one_r _ @ _). + refine (_ @ (rng_mult_zero_l _)^). + rewrite rng_mult_negate_l. + apply rng_plus_negate_l. + Defined. + + Instance rightinverse_plus_localization_type + : RightInverse plus_localization_type negate_localization_type zero_localization_type. + Proof. + srapply Localization_type_ind_hprop; intros f. + apply loc_frac_eq, fraction_eq_simple; simpl. + refine (rng_mult_one_r _ @ _). + refine (_ @ (rng_mult_zero_l _)^). + rewrite rng_mult_negate_l. + apply rng_plus_negate_r. + Defined. + + Instance associative_plus_localization_type + : Associative plus_localization_type. + Proof. + intros x y; srapply Localization_type_ind_hprop; intros z; revert y. + srapply Localization_type_ind_hprop; intros y; revert x. + srapply Localization_type_ind_hprop; intros x. + apply loc_frac_eq, fraction_eq_simple. + simpl. + rewrite ? rng_dist_r. + rewrite ? rng_mult_assoc. + rewrite ? rng_plus_assoc. + do 4 f_ap. + all: rewrite <- ? rng_mult_assoc. + all: f_ap. + 2: apply rng_mult_comm. + rewrite rng_mult_assoc. + apply rng_mult_comm. + Defined. + + Instance commutative_plus_localization_type + : Commutative plus_localization_type. + Proof. + intros x; srapply Localization_type_ind_hprop; intros y; revert x. + srapply Localization_type_ind_hprop; intros x. + apply loc_frac_eq, fraction_eq_simple; simpl. + rewrite (rng_mult_comm (denominator y) (denominator x)). + f_ap; apply rng_plus_comm. + Defined. + + Instance leftidentity_mult_localization_type + : LeftIdentity mult_localization_type one_localization_type. + Proof. + srapply Localization_type_ind_hprop; intros f. + apply loc_frac_eq, fraction_eq_simple; simpl. + f_ap; [|symmetry]; apply rng_mult_one_l. + Defined. + + Instance rightidentity_mult_localization_type + : RightIdentity mult_localization_type one_localization_type. + Proof. + srapply Localization_type_ind_hprop; intros f. + apply loc_frac_eq, fraction_eq_simple; simpl. + f_ap; [|symmetry]; apply rng_mult_one_r. + Defined. + + Instance associative_mult_localization_type + : Associative mult_localization_type. + Proof. + intros x y; srapply Localization_type_ind_hprop; intros z; revert y. + srapply Localization_type_ind_hprop; intros y; revert x. + srapply Localization_type_ind_hprop; intros x. + apply loc_frac_eq, fraction_eq_simple. + f_ap; [|symmetry]; apply rng_mult_assoc. + Defined. + + Instance commutative_mult_localization_type + : Commutative mult_localization_type. + Proof. + intros x; srapply Localization_type_ind_hprop; intros y; revert x. + srapply Localization_type_ind_hprop; intros x. + apply loc_frac_eq, fraction_eq_simple; simpl. + f_ap; rapply rng_mult_comm. + Defined. + + Instance leftdistribute_localization_type + : LeftDistribute mult_localization_type plus_localization_type. + Proof. + intros x y; srapply Localization_type_ind_hprop; intros z; revert y. + srapply Localization_type_ind_hprop; intros y; revert x. + srapply Localization_type_ind_hprop; intros x. + apply loc_frac_eq, fraction_eq_simple. + simpl. + rewrite ? rng_dist_l, ? rng_dist_r. + rewrite ? rng_mult_assoc. + do 2 f_ap. + all: rewrite <- ? rng_mult_assoc. + all: do 2 f_ap. + all: rewrite ? rng_mult_assoc. + all: rewrite (rng_mult_comm (_ x)). + all: rewrite <- ? rng_mult_assoc. + all: f_ap. + all: rewrite (rng_mult_comm _ (_ y)). + all: rewrite <- ? rng_mult_assoc. + all: f_ap. + Defined. + + Instance rightdistribute_localization_type + : RightDistribute mult_localization_type plus_localization_type. + Proof. + intros x y z. + rewrite 3 (commutative_mult_localization_type _ z). + snrapply leftdistribute_localization_type. + Defined. + + Instance isring_localization_type : IsRing Localization_type + := ltac:(repeat split; exact _). + + Definition abgroup_localization : AbGroup. + Proof. + snrapply Build_AbGroup. + - snrapply Build_Group. + + exact Localization_type. + + exact plus_localization_type. + + exact zero_localization_type. + + exact negate_localization_type. + + exact _. + - exact _. + Defined. + + Definition rng_localization : CRing. + Proof. + snrapply Build_CRing. + - snrapply Build_Ring. + + exact abgroup_localization. + + exact mult_localization_type. + + exact one_localization_type. + + exact leftdistribute_localization_type. + + exact rightdistribute_localization_type. + + exact _. + - exact _. + Defined. + + Definition loc_in : R $-> rng_localization. + Proof. + snrapply Build_RingHomomorphism. + 1: exact (loc_frac o frac_in). + snrapply Build_IsSemiRingPreserving. + - snrapply Build_IsMonoidPreserving. + + intros x y. + snrapply loc_frac_eq. + exists 1; split. + 1: exact mss_one. + simpl. + rewrite 5 rng_mult_one_r. + lhs nrapply rng_mult_one_l. + apply rng_plus_negate_r. + + reflexivity. + - snrapply Build_IsMonoidPreserving. + + intros x y. + snrapply loc_frac_eq. + exists 1; split. + 1: exact mss_one. + simpl. + rewrite 3 rng_mult_one_r. + lhs nrapply rng_mult_one_l. + nrapply rng_plus_negate_r. + + reflexivity. + Defined. + + Section Rec. + + Context (T : CRing) (f : R $-> T) + (H : forall x, IsInvertible T (f x)). + + Definition rng_localization_rec_map : rng_localization -> T. + Proof. + srapply Localization_type_rec. + - exact (fun x => f (numerator x) * inverse_elem (f (denominator x))). + - simpl. + intros x y z. + apply rng_inv_moveR_rV. + rhs_V nrapply rng_mult_move_left_assoc. + rhs_V nrapply rng_mult_assoc. + apply rng_inv_moveL_Vr. + lhs nrapply rng_mult_comm. + lhs_V nrapply rng_homo_mult. + rhs_V nrapply rng_homo_mult. + apply rng_moveL_0M. + lhs_V nrapply ap. + 1: nrapply rng_homo_negate. + lhs_V nrapply rng_homo_plus. + apply (equiv_ap (f z.1 *.)). + lhs_V nrapply rng_homo_mult. + rhs nrapply rng_mult_zero_r. + rhs_V nrapply (rng_homo_zero f). + exact (ap f (snd z.2)). + Defined. + + Instance issemiringpreserving_rng_localization_rec_map + : IsSemiRingPreserving rng_localization_rec_map. + Proof. + snrapply Build_IsSemiRingPreserving. + - snrapply Build_IsMonoidPreserving. + + intros x; rapply Localization_type_ind_hprop. + intros y; revert x; rapply Localization_type_ind_hprop; intros x. + simpl. + apply rng_inv_moveR_rV. + rhs nrapply rng_dist_r. + rewrite rng_homo_plus. + rewrite 3 rng_homo_mult. + f_ap. + 1,2: rhs_V nrapply rng_mult_assoc. + 1,2: f_ap. + 1,2: lhs_V nrapply rng_mult_one_l. + 1,2: rhs nrapply rng_mult_assoc. + 2: rhs nrapply rng_mult_comm. + 2: rhs nrapply rng_mult_assoc. + 1,2: f_ap. + 1,2: symmetry. + * apply rng_inv_l. + * apply rng_inv_r. + + hnf; simpl; rewrite rng_homo_zero. + nrapply rng_mult_zero_l. + - snrapply Build_IsMonoidPreserving. + + intros x; rapply Localization_type_ind_hprop. + intros y; revert x; rapply Localization_type_ind_hprop; intros x. + simpl. + apply rng_inv_moveR_rV. + lhs nrapply rng_homo_mult. + rhs_V nrapply rng_mult_assoc. + rhs_V nrapply rng_mult_assoc. + apply ap. + apply rng_inv_moveL_Vr. + lhs nrapply rng_mult_comm. + rhs_V nrapply rng_mult_assoc. + apply ap. + apply rng_inv_moveL_Vr. + symmetry. + rhs nrapply rng_mult_comm. + nrapply rng_homo_mult. + + apply rng_inv_moveR_rV; symmetry. + apply rng_mult_one_l. + Defined. + + Definition rng_localization_rec : rng_localization $-> T + := Build_RingHomomorphism rng_localization_rec_map _. + + Definition rng_localization_rec_beta + : rng_localization_rec $o loc_in $== f. + Proof. + intros x; simpl. + apply rng_inv_moveR_rV. + lhs_V nrapply rng_mult_one_r. + nrapply ap; symmetry. + apply rng_homo_one. + Defined. + + End Rec. + +End Localization. + +(** TODO: Show construction is a localization. *) diff --git a/theories/Algebra/Rings/Ring.v b/theories/Algebra/Rings/Ring.v index ab438bf8fcb..02191310916 100644 --- a/theories/Algebra/Rings/Ring.v +++ b/theories/Algebra/Rings/Ring.v @@ -93,6 +93,7 @@ Section RingLaws. Definition rng_negate_negate : - (- x) = x := groups.negate_involutive _. Definition rng_negate_zero : - (0 : A) = 0 := groups.negate_mon_unit. + Definition rng_negate_plus : - (x + y) = - x - y := negate_plus_distr _ _. Definition rng_mult_one_l : 1 * x = x := left_identity _. Definition rng_mult_one_r : x * 1 = x := right_identity _. @@ -105,6 +106,22 @@ Section RingLaws. End RingLaws. +Definition rng_dist_l_negate {A : Ring} (x y z : A) + : x * (y - z) = x * y - x * z. +Proof. + lhs nrapply rng_dist_l. + nrapply ap. + nrapply rng_mult_negate_r. +Defined. + +Definition rng_dist_r_negate {A : Ring} (x y z : A) + : (x - y) * z = x * z - y * z. +Proof. + lhs nrapply rng_dist_r. + nrapply ap. + nrapply rng_mult_negate_l. +Defined. + Section RingHomoLaws. Context {A B : Ring} (f : RingHomomorphism A B) (x y : A). @@ -785,7 +802,7 @@ Defined. (** *** Group of units *) (** Invertible elements are typically called "units" in ring theory and the collection of units forms a group under the ring multiplication. *) -Definition rng_unit_group {R : Ring} : Group. +Definition rng_unit_group (R : Ring) : Group. Proof. (** TODO: Use a generalised version of [Build_Subgroup] that works for subgroups of monoids. *) snrapply Build_Group. @@ -808,4 +825,52 @@ Proof. + apply rng_inv_r. Defined. +(** *** Invertible element movement lemmas *) + +Global Instance isequiv_rng_inv_mult_l {R : Ring} {x : R} + `{IsInvertible R x} + : IsEquiv (x *.). +Proof. + snrapply isequiv_adjointify. + 1: exact (inverse_elem x *.). + 1,2: intros y. + 1,2: lhs nrapply rng_mult_assoc. + 1,2: rhs_V nrapply rng_mult_one_l. + 1,2: snrapply (ap (.* y)). + - nrapply rng_inv_r. + - nrapply rng_inv_l. +Defined. + +Global Instance isequiv_rng_inv_mult_r {R : Ring} {x : R} + `{IsInvertible R x} + : IsEquiv (.* x). +Proof. + snrapply isequiv_adjointify. + 1: exact (.* inverse_elem x). + 1,2: intros y. + 1,2: lhs_V nrapply rng_mult_assoc. + 1,2: rhs_V nrapply rng_mult_one_r. + 1,2: snrapply (ap (y *.)). + - nrapply rng_inv_l. + - nrapply rng_inv_r. +Defined. + +(** ** These cannot be proven using the corresponding group laws in the group of units since not all elements involved are invertible. *) + +Definition rng_inv_moveL_Vr {R : Ring} {x y z : R} `{IsInvertible R y} + : y * x = z <~> x = inverse_elem y * z + := equiv_moveL_equiv_V (f := (y *.)) z x. + +Definition rng_inv_moveL_rV {R : Ring} {x y z : R} `{IsInvertible R y} + : x * y = z <~> x = z * inverse_elem y + := equiv_moveL_equiv_V (f := (.* y)) z x. + +Definition rng_inv_moveR_Vr {R : Ring} {x y z : R} `{IsInvertible R y} + : x = y * z <~> inverse_elem y * x = z + := equiv_moveR_equiv_V (f := (y *.)) x z. + +Definition rng_inv_moveR_rV {R : Ring} {x y z : R} `{IsInvertible R y} + : x = z * y <~> x * inverse_elem y = z + := equiv_moveR_equiv_V (f := (.* y)) x z. + (** TODO: The group of units construction is a functor from [Ring -> Group] and is right adjoint to the group ring construction. *) diff --git a/theories/Modalities/Descent.v b/theories/Modalities/Descent.v index a6c6bdba951..2bb68d9cff3 100644 --- a/theories/Modalities/Descent.v +++ b/theories/Modalities/Descent.v @@ -1,7 +1,7 @@ (* -*- mode: coq; mode: visual-line -*- *) Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Limits.Pullback. -Require Import Modality Accessible Localization. +Require Import Modality Accessible Modalities.Localization. Local Open Scope path_scope. Local Open Scope subuniverse_scope. diff --git a/theories/Modalities/Lex.v b/theories/Modalities/Lex.v index 7ffc61cabe4..68c0c725d55 100644 --- a/theories/Modalities/Lex.v +++ b/theories/Modalities/Lex.v @@ -1,7 +1,7 @@ (* -*- mode: coq; mode: visual-line -*- *) Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. -Require Import Modality Accessible Localization Descent Separated. +Require Import Modality Accessible Modalities.Localization Descent Separated. Local Open Scope path_scope. Local Open Scope subuniverse_scope. diff --git a/theories/Modalities/Nullification.v b/theories/Modalities/Nullification.v index cc037219ceb..ac6dda799fc 100644 --- a/theories/Modalities/Nullification.v +++ b/theories/Modalities/Nullification.v @@ -4,7 +4,7 @@ Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import Modality Accessible. -Require Export Localization. (** Nullification is a special case of localization *) +Require Export Modalities.Localization. (** Nullification is a special case of localization *) Local Open Scope path_scope. From df18704ec164b730d12da1271748d3bb763205b0 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Mon, 16 Sep 2024 16:24:06 -0400 Subject: [PATCH 02/28] Ring.v: adjust comments --- theories/Algebra/Rings/Ring.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/theories/Algebra/Rings/Ring.v b/theories/Algebra/Rings/Ring.v index 02191310916..127a0152f12 100644 --- a/theories/Algebra/Rings/Ring.v +++ b/theories/Algebra/Rings/Ring.v @@ -825,7 +825,7 @@ Proof. + apply rng_inv_r. Defined. -(** *** Invertible element movement lemmas *) +(** *** Multiplication by an invertible element is an equivalence *) Global Instance isequiv_rng_inv_mult_l {R : Ring} {x : R} `{IsInvertible R x} @@ -855,7 +855,9 @@ Proof. - nrapply rng_inv_r. Defined. -(** ** These cannot be proven using the corresponding group laws in the group of units since not all elements involved are invertible. *) +(** *** Invertible element movement lemmas *) + +(** These cannot be proven using the corresponding group laws in the group of units since not all elements involved are invertible. *) Definition rng_inv_moveL_Vr {R : Ring} {x y z : R} `{IsInvertible R y} : y * x = z <~> x = inverse_elem y * z From 554912a3484089cdb32c2b3d00bd958cb9da9802 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Mon, 16 Sep 2024 16:24:19 -0400 Subject: [PATCH 03/28] Ring.v: add isinvertible_rng_op, and add a comment about it later --- theories/Algebra/Rings/Ring.v | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/theories/Algebra/Rings/Ring.v b/theories/Algebra/Rings/Ring.v index 127a0152f12..a1705191527 100644 --- a/theories/Algebra/Rings/Ring.v +++ b/theories/Algebra/Rings/Ring.v @@ -633,6 +633,15 @@ Proof. by exists (inv : rng_op R). Defined. +(** The invertible elements in [R] and [rng_op R] agree, by swapping the proofs of left and right invertibility. *) +Definition isinvertible_rng_op (R : Ring) (x : R) `{!IsInvertible R x} + : IsInvertible (rng_op R) x. +Proof. + split. + - exact (isrightinvertible_isinvertible). + - exact (isleftinvertible_isinvertible). +Defined. + (** *** Uniqueness of inverses *) (** This general lemma will be used for uniqueness results. *) @@ -841,6 +850,7 @@ Proof. - nrapply rng_inv_l. Defined. +(** This can be proved by combining [isequiv_rng_inv_mult_l (R:=rng_op R)] with [isinvertible_rng_op], but then the inverse map is given by multiplying by [right_inverse_elem x] not [inverse_elem x], which complicates calculations. *) Global Instance isequiv_rng_inv_mult_r {R : Ring} {x : R} `{IsInvertible R x} : IsEquiv (.* x). From 25b130daa215dfc4b285ef7cc73678f0d47ce994 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Tue, 17 Sep 2024 19:29:18 +0200 Subject: [PATCH 04/28] add rng_localization_ind and rng_localization_ind_homotopy Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/CRing.v | 11 +++++ theories/Algebra/Rings/Localization.v | 69 +++++++++++++++++++++++++++ theories/Algebra/Rings/Ring.v | 38 +++++++++++++++ 3 files changed, 118 insertions(+) diff --git a/theories/Algebra/Rings/CRing.v b/theories/Algebra/Rings/CRing.v index 238d81a2936..249b099f822 100644 --- a/theories/Algebra/Rings/CRing.v +++ b/theories/Algebra/Rings/CRing.v @@ -69,6 +69,17 @@ Proof. apply rng_mult_move_left_assoc. Defined. +Definition isinvertible_cring (R : CRing) (x : R) + (inv : R) (inv_l : inv * x = 1) + : IsInvertible R x. +Proof. + snrapply Build_IsInvertible. + - exact inv. + - exact inv_l. + - lhs nrapply rng_mult_comm. + exact inv_l. +Defined. + (** ** Ideals in commutative rings *) Section IdealCRing. diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v index 3581ef5ed05..db7bbcd9654 100644 --- a/theories/Algebra/Rings/Localization.v +++ b/theories/Algebra/Rings/Localization.v @@ -614,6 +614,75 @@ Section Localization. Defined. End Rec. + + (** Elements belonging to the multiplicative subset [S] of [R] become invertible in [rng_localization R S]. *) + Global Instance isinvertible_rng_localization (x : R) (Sx : S x) + : IsInvertible rng_localization (loc_in x). + Proof. + snrapply isinvertible_cring. + - exact (loc_frac (Build_Fraction 1 x Sx)). + - apply loc_frac_eq, fraction_eq_simple. + exact (rng_mult_assoc _ _ _)^. + Defined. + + (** As a special case, any denominator of a fraction must necesserily be invertible. *) + Global Instance isinvertible_denominator (f : Fraction) + : IsInvertible rng_localization (loc_in (denominator f)). + Proof. + snrapply isinvertible_rng_localization. + exact (in_mult_subset_denominator f). + Defined. + + (** We can factor any fraction as the multiplication of the numerator and the inverse of the denominator. *) + Definition fraction_decompose (f : Fraction) + : loc_frac f + = loc_in (numerator f) * inverse_elem (loc_in (denominator f)). + Proof. + apply loc_frac_eq, fraction_eq_simple. + nrapply rng_mult_assoc. + Defined. + + Section Ind. + + Context (P : rng_localization -> Type) + (H : forall x, IsHProp (P x)) + (Hin : forall x, P (loc_in x)) + (Hinv : forall x (H : IsInvertible rng_localization x), + P x -> P (inverse_elem x)) + (Hmul : forall x y, P x -> P y -> P (x * y)) + . + + Definition rng_localization_ind + : forall x, P x. + Proof. + srapply Localization_type_ind. + - intros f. + refine (transport P (fraction_decompose f)^ _). + apply Hmul. + + apply Hin. + + apply Hinv, Hin. + - intros f1 f2 p. + apply path_ishprop. + Defined. + + End Ind. + + Definition rng_localization_ind_homotopy {T : CRing} + {f g : rng_localization $-> T} + (p : f $o loc_in $== g $o loc_in) + : f $== g. + Proof. + srapply rng_localization_ind. + - exact p. + - hnf; intros x H q. + change (inverse_elem (f x) = inverse_elem (g x)). + apply equiv_path_inverse_elem. + exact q. + - hnf; intros x y q r. + lhs nrapply rng_homo_mult. + rhs nrapply rng_homo_mult. + f_ap. + Defined. End Localization. diff --git a/theories/Algebra/Rings/Ring.v b/theories/Algebra/Rings/Ring.v index a1705191527..05561cc00aa 100644 --- a/theories/Algebra/Rings/Ring.v +++ b/theories/Algebra/Rings/Ring.v @@ -808,6 +808,20 @@ Proof. - apply rng_mult_one_l. Defined. +(** Ring homomorphisms preserve invertible elements. *) +Global Instance isinvertible_rng_homo {R S} (f : R $-> S) + : forall x, IsInvertible R x -> IsInvertible S (f x). +Proof. + intros x H. + snrapply Build_IsInvertible. + 1: exact (f (inverse_elem x)). + 1,2: lhs_V nrapply rng_homo_mult. + 1,2: rhs_V nrapply (rng_homo_one f). + 1,2: nrapply (ap f). + - exact (rng_inv_l x). + - exact (rng_inv_r x). +Defined. + (** *** Group of units *) (** Invertible elements are typically called "units" in ring theory and the collection of units forms a group under the ring multiplication. *) @@ -885,4 +899,28 @@ Definition rng_inv_moveR_rV {R : Ring} {x y z : R} `{IsInvertible R y} : x = z * y <~> x * inverse_elem y = z := equiv_moveR_equiv_V (f := (.* y)) x z. +Definition inverse_elem_inverse_elem {R : Ring} (x : R) + `{IsInvertible R x} + : inverse_elem (inverse_elem x) = x. +Proof. + lhs_V nrapply rng_mult_one_r. + apply rng_inv_moveR_Vr. + exact (rng_inv_l x)^. +Defined. + +Definition equiv_path_inverse_elem {R : Ring} {x y : R} + `{IsInvertible R x, IsInvertible R y} + : x = y <~> inverse_elem x = inverse_elem y. +Proof. + srapply equiv_iff_hprop. + - intros p. + snrapply (ap011D inverse_elem p). + apply path_ishprop. + - intros p. + lhs_V nrapply inverse_elem_inverse_elem. + rhs_V nrapply inverse_elem_inverse_elem. + snrapply (ap011D inverse_elem p). + apply path_ishprop. +Defined. + (** TODO: The group of units construction is a functor from [Ring -> Group] and is right adjoint to the group ring construction. *) From bc0a423230f551ffe64fbe41c804eac8e61fd3a0 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Tue, 17 Sep 2024 19:40:18 -0400 Subject: [PATCH 05/28] Ring.v: simplify a few proofs --- theories/Algebra/Rings/Ring.v | 34 +++++++++++++--------------------- 1 file changed, 13 insertions(+), 21 deletions(-) diff --git a/theories/Algebra/Rings/Ring.v b/theories/Algebra/Rings/Ring.v index 05561cc00aa..a08093c51ae 100644 --- a/theories/Algebra/Rings/Ring.v +++ b/theories/Algebra/Rings/Ring.v @@ -687,10 +687,11 @@ Proof. apply path_left_inverse_elem_right_inverse_elem. Defined. -(** Furthermore, any two proofs of invertibility have the same inverse. *) -Definition isinvertible_unique {R x} (H1 H2 : IsInvertible R x) - : @inverse_elem R x H1 = @inverse_elem R x H2. +(** Equal elements have equal inverses. Note that we don't require that the proofs of invertibility are equal (over [p]). It follows that the inverse of an invertible element [x] depends only on [x]. *) +Definition isinvertible_unique {R : Ring} (x y : R) `{IsInvertible R x} `{IsInvertible R y} (p : x = y) + : inverse_elem x = inverse_elem y. Proof. + destruct p. snrapply (path_left_right_inverse x). - apply rng_inv_l. - apply rng_inv_r. @@ -793,10 +794,8 @@ Global Instance isinvertible_inverse_elem {R : Ring} (x : R) : IsInvertible R (inverse_elem x). Proof. split. - - unfold inverse_elem. - rewrite (path_left_inverse_elem_right_inverse_elem x). - exact _. - - exact _. + - exists x; apply rng_inv_r. + - apply isrightinvertible_left_inverse_elem. Defined. (** [1] is always invertible, and by the above [-1]. *) @@ -899,28 +898,21 @@ Definition rng_inv_moveR_rV {R : Ring} {x y z : R} `{IsInvertible R y} : x = z * y <~> x * inverse_elem y = z := equiv_moveR_equiv_V (f := (.* y)) x z. +(** TODO: The next two results should probably go after isinvertible_inverse_elem. + But maybe the first one should be dropped, since it is now definitional? *) + Definition inverse_elem_inverse_elem {R : Ring} (x : R) `{IsInvertible R x} - : inverse_elem (inverse_elem x) = x. -Proof. - lhs_V nrapply rng_mult_one_r. - apply rng_inv_moveR_Vr. - exact (rng_inv_l x)^. -Defined. + : inverse_elem (inverse_elem x) = x + := idpath. Definition equiv_path_inverse_elem {R : Ring} {x y : R} `{IsInvertible R x, IsInvertible R y} : x = y <~> inverse_elem x = inverse_elem y. Proof. srapply equiv_iff_hprop. - - intros p. - snrapply (ap011D inverse_elem p). - apply path_ishprop. - - intros p. - lhs_V nrapply inverse_elem_inverse_elem. - rhs_V nrapply inverse_elem_inverse_elem. - snrapply (ap011D inverse_elem p). - apply path_ishprop. + - exact (isinvertible_unique x y). + - exact (isinvertible_unique (inverse_elem x) (inverse_elem y)). Defined. (** TODO: The group of units construction is a functor from [Ring -> Group] and is right adjoint to the group ring construction. *) From 7b5080677ed1e287160060fb1f1ba054df7cb510 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Tue, 17 Sep 2024 19:40:53 -0400 Subject: [PATCH 06/28] Localization: fix typo in comment --- theories/Algebra/Rings/Localization.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v index db7bbcd9654..864b993fae2 100644 --- a/theories/Algebra/Rings/Localization.v +++ b/theories/Algebra/Rings/Localization.v @@ -625,7 +625,7 @@ Section Localization. exact (rng_mult_assoc _ _ _)^. Defined. - (** As a special case, any denominator of a fraction must necesserily be invertible. *) + (** As a special case, any denominator of a fraction must necessarily be invertible. *) Global Instance isinvertible_denominator (f : Fraction) : IsInvertible rng_localization (loc_in (denominator f)). Proof. From ed34bd7202c119166589a14dd96c3977fe5ab1f0 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Tue, 17 Sep 2024 19:46:12 -0400 Subject: [PATCH 07/28] Ring.v: rm definitional inverse_elem_inverse_elem and mv equiv_path_inverse_elem --- theories/Algebra/Rings/Ring.v | 29 +++++++++++------------------ 1 file changed, 11 insertions(+), 18 deletions(-) diff --git a/theories/Algebra/Rings/Ring.v b/theories/Algebra/Rings/Ring.v index a08093c51ae..da5d0134355 100644 --- a/theories/Algebra/Rings/Ring.v +++ b/theories/Algebra/Rings/Ring.v @@ -788,7 +788,7 @@ Proof. exact (right_inverse_eq x). Defined. -(** Inverses of invertible elements are themselves invertible. *) +(** Inverses of invertible elements are themselves invertible. We take both inverses of [inverse_elem x] to be [x]. *) Global Instance isinvertible_inverse_elem {R : Ring} (x : R) `{IsInvertible R x} : IsInvertible R (inverse_elem x). @@ -798,6 +798,16 @@ Proof. - apply isrightinvertible_left_inverse_elem. Defined. +(** Since [inverse_elem (inverse_elem x) = x], we get the following equivalence. *) +Definition equiv_path_inverse_elem {R : Ring} {x y : R} + `{IsInvertible R x, IsInvertible R y} + : x = y <~> inverse_elem x = inverse_elem y. +Proof. + srapply equiv_iff_hprop. + - exact (isinvertible_unique x y). + - exact (isinvertible_unique (inverse_elem x) (inverse_elem y)). +Defined. + (** [1] is always invertible, and by the above [-1]. *) Global Instance isinvertible_one {R} : IsInvertible R 1. Proof. @@ -898,21 +908,4 @@ Definition rng_inv_moveR_rV {R : Ring} {x y z : R} `{IsInvertible R y} : x = z * y <~> x * inverse_elem y = z := equiv_moveR_equiv_V (f := (.* y)) x z. -(** TODO: The next two results should probably go after isinvertible_inverse_elem. - But maybe the first one should be dropped, since it is now definitional? *) - -Definition inverse_elem_inverse_elem {R : Ring} (x : R) - `{IsInvertible R x} - : inverse_elem (inverse_elem x) = x - := idpath. - -Definition equiv_path_inverse_elem {R : Ring} {x y : R} - `{IsInvertible R x, IsInvertible R y} - : x = y <~> inverse_elem x = inverse_elem y. -Proof. - srapply equiv_iff_hprop. - - exact (isinvertible_unique x y). - - exact (isinvertible_unique (inverse_elem x) (inverse_elem y)). -Defined. - (** TODO: The group of units construction is a functor from [Ring -> Group] and is right adjoint to the group ring construction. *) From d5541f10e80e5f3b819d1a9d9fb6a0bcf1857475 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Tue, 17 Sep 2024 20:55:19 -0400 Subject: [PATCH 08/28] Rings/Localization: updates to comments and whitespace --- theories/Algebra/Rings/Localization.v | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v index 864b993fae2..3156764c111 100644 --- a/theories/Algebra/Rings/Localization.v +++ b/theories/Algebra/Rings/Localization.v @@ -3,9 +3,9 @@ Require Import Basics.Overture Basics.Trunc Basics.Tactics WildCat.Core Local Open Scope mc_scope. -(** * Localizaiton of commutative rings *) +(** * Localization of commutative rings *) -(** ** Localization is a way to make elements in a commutative ring invertible by adding inverses, in the most minimal way possible. It generalizes the familar operation of a field of fractions. *) +(** Localization is a way to make elements in a commutative ring invertible by adding inverses, in the most minimal way possible. It generalizes the familiar operation of a field of fractions. *) (** ** Multiplicative subsets *) @@ -26,7 +26,7 @@ Arguments mss_mult {R _ _ _ _}. (** *** Examples *) -(** The multplicative subset of powers of a ring element. *) +(** The multiplicative subset of powers of a ring element. *) Global Instance ismultiplicative_powers (R : CRing) (x : R) : IsMultiplicativeSubset (fun r => exists n, rng_power x n = r). Proof. @@ -45,7 +45,7 @@ Global Instance ismultiplicative_isinvertible (R : CRing) (** TODO: Property of being a localization. *) -(** ** Construction of localization. *) +(** ** Construction of localization *) Section Localization. @@ -60,8 +60,9 @@ Section Localization. : loc_frac n1 d1 p1 = loc_frac n2 d2 p2 . >>> - - We will implement this HIT by writing it as a quotient. + along with the condition that this HIT be a set. + + We will implement this HIT by writing it as a set quotient. *) Context (R : CRing) (S : R -> Type) `{!IsMultiplicativeSubset S}. @@ -82,13 +83,13 @@ Section Localization. exact (x * (n1 * d2 - n2 * d1) = 0). Defined. - (** It is convenient to produce elements of this relation specalized to when the scaling factor is 1 *) + (** It is convenient to produce elements of this relation specalized to when the scaling factor is [1]. *) Definition fraction_eq_simple f1 f2 (p : numerator f1 * denominator f2 = numerator f2 * denominator f1) : fraction_eq f1 f2. Proof. exists 1. - refine (mss_one ,_). + refine (mss_one, _). refine (rng_mult_one_l _ @ _). by apply rng_moveL_0M^-1. Defined. @@ -137,14 +138,14 @@ Section Localization. (** *** Addition operation *) - (** Fraction addition *) + (** Fraction addition is the usual addition of fractions. *) Definition frac_add : Fraction -> Fraction -> Fraction := fun '(Build_Fraction n1 d1 p1) '(Build_Fraction n2 d2 p2) => Build_Fraction (n1 * d2 + n2 * d1) (d1 * d2) (mss_mult p1 p2). (** Fraction addition is well-defined upto equality of fractions. *) - (** It is easier to prove well-definedness of both arguments at once. *) + (** It is easier to prove well-definedness as a function of both arguments at once. *) Definition frac_add_wd (f1 f1' f2 f2' : Fraction) (p : fraction_eq f1 f1') (q : fraction_eq f2 f2') : fraction_eq (frac_add f1 f2) (frac_add f1' f2'). @@ -205,7 +206,7 @@ Section Localization. by apply frac_add_wd. Defined. - (** The addition operation for fractions is the usual fraction addition. Most of the work is spent showing that this is well-defined. *) + (** The addition operation on the localization is induced from the addition operation for fractions. *) Instance plus_localization_type : Plus Localization_type. Proof. intros x; srapply Localization_type_rec. From a2dea01f2c184548dd419783fa87a8ee8b0f79e9 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Tue, 17 Sep 2024 20:56:28 -0400 Subject: [PATCH 09/28] Colimits/Quotient: avoid Funext in Quotient_rec2; simplify other proofs --- theories/Colimits/Quotient.v | 29 ++++++++++++++++------------- 1 file changed, 16 insertions(+), 13 deletions(-) diff --git a/theories/Colimits/Quotient.v b/theories/Colimits/Quotient.v index e3c8f4b7b3d..aa71e8624a9 100644 --- a/theories/Colimits/Quotient.v +++ b/theories/Colimits/Quotient.v @@ -99,12 +99,10 @@ Section Equiv. (* The proposition of being in a given class in a quotient. *) Definition in_class : A / R -> A -> HProp. Proof. - srapply Quotient_ind. - { intros a b. - exact (Build_HProp (R a b)). } - intros x y p. - refine (transport_const _ _ @ _). - funext z. + intros a b; revert a. + srapply Quotient_rec. + 1: intro a; exact (Build_HProp (R a b)). + intros x y p; cbn beta. apply path_hprop. srapply equiv_iff_hprop; cbn. 1: apply (transitivity (symmetry _ _ p)). @@ -134,7 +132,7 @@ Section Equiv. Proof. srapply Quotient_ind. { intros x y p. - apply (qglue p). } + exact (qglue p). } intros x y p. funext ? ?. apply hset_path2. @@ -159,19 +157,24 @@ Section Equiv. - apply related_quotient_paths. Defined. - Definition Quotient_rec2 `{Funext} {B : HSet} {dclass : A -> A -> B} + Definition Quotient_rec2 {B : HSet} {dclass : A -> A -> B} {dequiv : forall x x', R x x' -> forall y y', R y y' -> dclass x y = dclass x' y'} : A / R -> A / R -> B. Proof. + clear H. (* Ensure that we don't use Univalence. *) + intro a. srapply Quotient_rec. - { intro a. + { intro a'. + revert a. srapply Quotient_rec. - { revert a. - assumption. } - by apply (dequiv a a). } + { intro a. exact (dclass a a'). } + cbn beta. + intros x y p. + by apply (dequiv x y p a' a'). } + cbn beta. intros x y p. - apply path_forall. + revert a. srapply Quotient_ind. { cbn; intro a. by apply dequiv. } From 7fff38f2c6b19826765963ee50ecb2d1c00fd153 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Tue, 17 Sep 2024 20:57:19 -0400 Subject: [PATCH 10/28] Rings/Localization: simplify addition using Quotient_rec2 --- theories/Algebra/Rings/Localization.v | 22 +++++++++------------- 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v index 3156764c111..15e0872f250 100644 --- a/theories/Algebra/Rings/Localization.v +++ b/theories/Algebra/Rings/Localization.v @@ -30,7 +30,7 @@ Arguments mss_mult {R _ _ _ _}. Global Instance ismultiplicative_powers (R : CRing) (x : R) : IsMultiplicativeSubset (fun r => exists n, rng_power x n = r). Proof. - srapply Build_IsMultiplicativeSubset. + srapply Build_IsMultiplicativeSubset; cbn beta. 1: by exists 0%nat. intros a b np mq. destruct np as [n p], mq as [m q]. @@ -209,18 +209,14 @@ Section Localization. (** The addition operation on the localization is induced from the addition operation for fractions. *) Instance plus_localization_type : Plus Localization_type. Proof. - intros x; srapply Localization_type_rec. - { intros f2; revert x. - srapply Localization_type_rec. - { intros f1. - apply loc_frac. - exact (frac_add f1 f2). } - intros f1 f1' p. - by apply loc_frac_eq, frac_add_wd_l. } - intros f2 f2' p; revert x; cbn. - srapply Localization_type_ind_hprop. - intros f1. - by apply loc_frac_eq, frac_add_wd_r. + srapply Quotient_rec2. + 1: rapply fraction_eq_refl. + { cbn. + intros f1 f2. + exact (loc_frac (frac_add f1 f2)). } + cbn beta. + intros f1 f1' p f2 f2' q. + by apply loc_frac_eq, frac_add_wd. Defined. (** *** Multiplication operation *) From 2e501c49e4fc912dd02c90b899238e7244832222 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 18 Sep 2024 14:13:01 +0200 Subject: [PATCH 11/28] explode section for rng_localization_ind Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/Localization.v | 42 ++++++++++++--------------- 1 file changed, 18 insertions(+), 24 deletions(-) diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v index 15e0872f250..258bd302aa3 100644 --- a/theories/Algebra/Rings/Localization.v +++ b/theories/Algebra/Rings/Localization.v @@ -639,30 +639,24 @@ Section Localization. nrapply rng_mult_assoc. Defined. - Section Ind. - - Context (P : rng_localization -> Type) - (H : forall x, IsHProp (P x)) - (Hin : forall x, P (loc_in x)) - (Hinv : forall x (H : IsInvertible rng_localization x), - P x -> P (inverse_elem x)) - (Hmul : forall x y, P x -> P y -> P (x * y)) - . - - Definition rng_localization_ind - : forall x, P x. - Proof. - srapply Localization_type_ind. - - intros f. - refine (transport P (fraction_decompose f)^ _). - apply Hmul. - + apply Hin. - + apply Hinv, Hin. - - intros f1 f2 p. - apply path_ishprop. - Defined. - - End Ind. + Definition rng_localization_ind + (P : rng_localization -> Type) + (H : forall x, IsHProp (P x)) + (Hin : forall x, P (loc_in x)) + (Hinv : forall x (H : IsInvertible rng_localization x), + P x -> P (inverse_elem x)) + (Hmul : forall x y, P x -> P y -> P (x * y)) + : forall x, P x. + Proof. + srapply Localization_type_ind. + - intros f. + refine (transport P (fraction_decompose f)^ _). + apply Hmul. + + apply Hin. + + apply Hinv, Hin. + - intros f1 f2 p. + apply path_ishprop. + Defined. Definition rng_localization_ind_homotopy {T : CRing} {f g : rng_localization $-> T} From 43b204f1e2001b1c9eabb212edc603bceee43800 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 18 Sep 2024 19:35:32 +0200 Subject: [PATCH 12/28] simplilfy definition of fraction_eq and simplify proofs Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/CRing.v | 8 ++ theories/Algebra/Rings/Localization.v | 190 ++++++++++---------------- 2 files changed, 81 insertions(+), 117 deletions(-) diff --git a/theories/Algebra/Rings/CRing.v b/theories/Algebra/Rings/CRing.v index 249b099f822..a4f2ee3cd01 100644 --- a/theories/Algebra/Rings/CRing.v +++ b/theories/Algebra/Rings/CRing.v @@ -56,6 +56,14 @@ Proof. f_ap. Defined. +Definition rng_mult_permute_2_3 {R : CRing} (x y z : R) + : x * y * z = x * z * y. +Proof. + lhs_V nrapply rng_mult_assoc. + rhs_V nrapply rng_mult_assoc. + apply ap, rng_mult_comm. +Defined. + Definition rng_mult_move_left_assoc {R : CRing} (x y z : R) : x * y * z = y * x * z. Proof. diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v index 258bd302aa3..f7191db3378 100644 --- a/theories/Algebra/Rings/Localization.v +++ b/theories/Algebra/Rings/Localization.v @@ -80,7 +80,7 @@ Section Localization. Proof. intros [n1 d1 ?] [n2 d2 ?]. refine (exists (x : R), S x /\ _). - exact (x * (n1 * d2 - n2 * d1) = 0). + exact (x * n1 * d2 = x * n2 * d1). Defined. (** It is convenient to produce elements of this relation specalized to when the scaling factor is [1]. *) @@ -90,8 +90,9 @@ Section Localization. Proof. exists 1. refine (mss_one, _). - refine (rng_mult_one_l _ @ _). - by apply rng_moveL_0M^-1. + lhs_V nrapply rng_mult_assoc. + rhs_V nrapply rng_mult_assoc. + exact (ap (1 *.) p). Defined. Definition fraction_eq_refl f1 : fraction_eq f1 f1. @@ -155,42 +156,25 @@ Section Localization. p as [x [sx p]], q as [y [sy q]]. refine (x * y ; (mss_mult sx sy, _)). simpl. - rewrite rng_dist_l_negate. - rewrite 2 rng_dist_r. - rewrite 2 rng_dist_l. - rewrite <- rng_plus_assoc. - rewrite (rng_plus_comm _ (- _)). - rewrite rng_negate_plus. - rewrite 2 rng_plus_assoc. - rewrite <- (rng_plus_assoc _ (- _)). - rewrite (rng_plus_comm (- _)). - rewrite <- 2 rng_dist_l_negate. - rewrite <- ? rng_mult_assoc. - rewrite 2 (rng_mult_move_right_assoc a'). - rewrite (rng_mult_comm a' t). - rewrite (rng_mult_move_right_assoc s). - rewrite (rng_mult_comm s a'). - rewrite (rng_mult_move_right_assoc t). - rewrite (rng_mult_comm t t'). - rewrite <- 2 (rng_mult_move_right_assoc t'). - rewrite <- (rng_dist_l_negate t'). - rewrite (rng_mult_comm _ t). - rewrite (rng_mult_move_right_assoc _ t). - rewrite <- (rng_dist_l_negate t). - rewrite <- 2 (rng_mult_move_right_assoc t'). - rewrite <- 2 (rng_mult_move_right_assoc t). - rewrite (rng_mult_move_right_assoc x). - rewrite p. - rewrite 3 rng_mult_zero_r. - rewrite rng_plus_zero_l. - rewrite 2 (rng_mult_move_right_assoc b). - rewrite 2 (rng_mult_move_right_assoc b'). - rewrite (rng_mult_move_right_assoc s). - rewrite <- 2 rng_dist_l_negate. - rewrite 2 (rng_mult_move_right_assoc y). - rewrite q. - by rewrite 3 rng_mult_zero_r. - Qed. + rewrite 2 rng_dist_l, 2 rng_dist_r. + snrapply (ap011 (+)). + - rewrite 4 rng_mult_assoc. + rewrite 8 (rng_mult_permute_2_3 _ y). + apply (ap (.* y)). + rewrite 2 (rng_mult_permute_2_3 _ t). + apply (ap (.* t)). + rewrite (rng_mult_permute_2_3 _ t'). + f_ap. + - do 2 lhs_V nrapply rng_mult_assoc. + do 2 rhs_V nrapply rng_mult_assoc. + f_ap. + rewrite 6 rng_mult_assoc. + rewrite 2 (rng_mult_permute_2_3 _ _ t'). + rewrite 2 (rng_mult_permute_2_3 _ _ t). + lhs_V nrapply rng_mult_assoc. + rhs_V nrapply rng_mult_assoc. + f_ap; apply rng_mult_comm. + Defined. Definition frac_add_wd_l (f1 f1' f2 : Fraction) (p : fraction_eq f1 f1') : fraction_eq (frac_add f1 f2) (frac_add f1' f2). @@ -210,13 +194,13 @@ Section Localization. Instance plus_localization_type : Plus Localization_type. Proof. srapply Quotient_rec2. - 1: rapply fraction_eq_refl. - { cbn. + - rapply fraction_eq_refl. + - cbn. intros f1 f2. - exact (loc_frac (frac_add f1 f2)). } - cbn beta. - intros f1 f1' p f2 f2' q. - by apply loc_frac_eq, frac_add_wd. + exact (loc_frac (frac_add f1 f2)). + - cbn beta. + intros f1 f1' p f2 f2' q. + by apply loc_frac_eq, frac_add_wd. Defined. (** *** Multiplication operation *) @@ -230,21 +214,11 @@ Section Localization. Proof. destruct p as [x [s p]]. refine (x; (s, _)); simpl. - rewrite rng_dist_l. - rewrite rng_dist_l in p. - rewrite rng_mult_negate_r. - rewrite rng_mult_negate_r in p. - apply rng_moveL_0M in p. - apply rng_moveL_0M^-1. - rewrite 2 (rng_mult_comm _ (numerator f2)). - rewrite 2 (rng_mult_comm _ (denominator f2)). - rewrite <- 2 (rng_mult_assoc (numerator f2)). - rewrite 2 (rng_mult_comm (numerator _) (denominator f2 * _)). - rewrite ? (rng_mult_assoc (numerator f2)). - rewrite <- ? (rng_mult_assoc (numerator f2 * denominator f2)). - rewrite 2 (rng_mult_comm (denominator _) (numerator _)). - rewrite 2 (rng_mult_comm (numerator f2 * denominator f2)). - rewrite 2 (rng_mult_assoc x (numerator _ * denominator _)). + rewrite 4 rng_mult_assoc. + rewrite (rng_mult_permute_2_3 _ _ (denominator f1')). + rewrite (rng_mult_permute_2_3 _ _ (denominator f1)). + lhs_V nrapply rng_mult_assoc. + rhs_V nrapply rng_mult_assoc. f_ap. Defined. @@ -253,73 +227,64 @@ Section Localization. Proof. destruct p as [x [s p]]. refine (x; (s, _)); simpl. - rewrite rng_dist_l. - rewrite rng_dist_l in p. - rewrite rng_mult_negate_r. - rewrite rng_mult_negate_r in p. - apply rng_moveL_0M in p. - apply rng_moveL_0M^-1. - rewrite 2 (rng_mult_comm (numerator f1)). - rewrite <- 2 rng_mult_assoc. - rewrite 2 (rng_mult_comm (numerator f1)). - rewrite <- ? rng_mult_assoc. - rewrite 2 (rng_mult_move_right_assoc (denominator f1)). - rewrite ? rng_mult_assoc. - rewrite ? rng_mult_assoc in p. - do 2 f_ap. + rewrite 4 rng_mult_assoc. + rewrite (rng_mult_permute_2_3 _ _ (numerator f2)). + rewrite 2 (rng_mult_permute_2_3 _ _ (denominator f2')). + rewrite (rng_mult_permute_2_3 _ _ (numerator f2')). + rewrite 2 (rng_mult_permute_2_3 _ _ (denominator f2)). + lhs_V nrapply rng_mult_assoc. + rhs_V nrapply rng_mult_assoc. + f_ap. Defined. Instance mult_localization_type : Mult Localization_type. Proof. intros x; srapply Localization_type_rec. - { intros f2; revert x. + - intros f2; revert x. srapply Localization_type_rec. - { intros f1. + + intros f1. apply loc_frac. - exact (frac_mult f1 f2). } - intros f1 f1' p. - by apply loc_frac_eq, frac_mult_wd_l. } - intros f2 f2' p; revert x. - srapply Localization_type_ind_hprop. - intros f1. - by apply loc_frac_eq, frac_mult_wd_r. + exact (frac_mult f1 f2). + + intros f1 f1' p. + by apply loc_frac_eq, frac_mult_wd_l. + - intros f2 f2' p; revert x. + srapply Localization_type_ind_hprop. + intros f1. + by apply loc_frac_eq, frac_mult_wd_r. Defined. (** *** Zero element *) - Instance zero_localization_type : Zero Localization_type := - loc_frac (Build_Fraction 0 1 mss_one). + Instance zero_localization_type : Zero Localization_type + := loc_frac (Build_Fraction 0 1 mss_one). (** *** One element *) - Instance one_localization_type : One Localization_type := - loc_frac (Build_Fraction 1 1 mss_one). + Instance one_localization_type : One Localization_type + := loc_frac (Build_Fraction 1 1 mss_one). (** *** Negation operation *) - Definition frac_negate : Fraction -> Fraction := - fun '(Build_Fraction n d p) => Build_Fraction (- n) d p. + Definition frac_negate : Fraction -> Fraction + := fun '(Build_Fraction n d p) => Build_Fraction (- n) d p. Definition frac_negate_wd f1 f2 (p : fraction_eq f1 f2) : fraction_eq (frac_negate f1) (frac_negate f2). Proof. destruct p as [x [s p]]. refine (x; (s,_)); simpl. - rewrite 2 rng_mult_negate_l. - rewrite <- rng_negate_plus. - rewrite rng_mult_negate_r. - rewrite p. - apply rng_negate_zero. + rewrite 2 rng_mult_negate_r, 2 rng_mult_negate_l. + f_ap. Defined. Instance negate_localization_type : Negate Localization_type. Proof. srapply Localization_type_rec. - { intros f. + - intros f. apply loc_frac. - exact (frac_negate f). } - intros f1 f2 p. - by apply loc_frac_eq, frac_negate_wd. + exact (frac_negate f). + - intros f1 f2 p. + by apply loc_frac_eq, frac_negate_wd. Defined. (** *** Ring laws *) @@ -503,22 +468,14 @@ Section Localization. - snrapply Build_IsMonoidPreserving. + intros x y. snrapply loc_frac_eq. - exists 1; split. - 1: exact mss_one. - simpl. - rewrite 5 rng_mult_one_r. - lhs nrapply rng_mult_one_l. - apply rng_plus_negate_r. + apply fraction_eq_simple. + by simpl; rewrite 5 rng_mult_one_r. + reflexivity. - snrapply Build_IsMonoidPreserving. + intros x y. snrapply loc_frac_eq. - exists 1; split. - 1: exact mss_one. - simpl. - rewrite 3 rng_mult_one_r. - lhs nrapply rng_mult_one_l. - nrapply rng_plus_negate_r. + apply fraction_eq_simple. + by simpl; rewrite 3 rng_mult_one_r. + reflexivity. Defined. @@ -537,17 +494,16 @@ Section Localization. rhs_V nrapply rng_mult_move_left_assoc. rhs_V nrapply rng_mult_assoc. apply rng_inv_moveL_Vr. - lhs nrapply rng_mult_comm. lhs_V nrapply rng_homo_mult. rhs_V nrapply rng_homo_mult. - apply rng_moveL_0M. - lhs_V nrapply ap. - 1: nrapply rng_homo_negate. - lhs_V nrapply rng_homo_plus. apply (equiv_ap (f z.1 *.)). lhs_V nrapply rng_homo_mult. - rhs nrapply rng_mult_zero_r. - rhs_V nrapply (rng_homo_zero f). + rhs_V nrapply rng_homo_mult. + lhs nrapply ap. + 1: lhs nrapply rng_mult_assoc. + 1: nrapply rng_mult_permute_2_3. + rhs nrapply ap. + 2: nrapply rng_mult_assoc. exact (ap f (snd z.2)). Defined. From 189b7df4ba22a86f40e656130ea540769fc2766d Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Wed, 18 Sep 2024 20:54:45 -0400 Subject: [PATCH 13/28] Rings/Localization: use Quotient_rec2 in mult_localization_type too --- theories/Algebra/Rings/Localization.v | 22 ++++++++++------------ 1 file changed, 10 insertions(+), 12 deletions(-) diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v index f7191db3378..71259fa93f7 100644 --- a/theories/Algebra/Rings/Localization.v +++ b/theories/Algebra/Rings/Localization.v @@ -239,18 +239,16 @@ Section Localization. Instance mult_localization_type : Mult Localization_type. Proof. - intros x; srapply Localization_type_rec. - - intros f2; revert x. - srapply Localization_type_rec. - + intros f1. - apply loc_frac. - exact (frac_mult f1 f2). - + intros f1 f1' p. - by apply loc_frac_eq, frac_mult_wd_l. - - intros f2 f2' p; revert x. - srapply Localization_type_ind_hprop. - intros f1. - by apply loc_frac_eq, frac_mult_wd_r. + srapply Quotient_rec2. + - rapply fraction_eq_refl. + - cbn. + intros f1 f2. + exact (loc_frac (frac_mult f1 f2)). + - cbn beta. + intros f1 f1' p f2 f2' q. + transitivity (loc_frac (frac_mult f1' f2)). + + by apply loc_frac_eq, frac_mult_wd_l. + + by apply loc_frac_eq, frac_mult_wd_r. Defined. (** *** Zero element *) From 9524c0df54b12e1110d807856def6f0b4414327b Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 19 Sep 2024 10:58:37 +0200 Subject: [PATCH 14/28] merge abgroup_localization into rng_localization Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/Localization.v | 35 ++++++++++++--------------- 1 file changed, 15 insertions(+), 20 deletions(-) diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v index 71259fa93f7..0ff826727d5 100644 --- a/theories/Algebra/Rings/Localization.v +++ b/theories/Algebra/Rings/Localization.v @@ -433,29 +433,24 @@ Section Localization. Instance isring_localization_type : IsRing Localization_type := ltac:(repeat split; exact _). - Definition abgroup_localization : AbGroup. - Proof. - snrapply Build_AbGroup. - - snrapply Build_Group. - + exact Localization_type. - + exact plus_localization_type. - + exact zero_localization_type. - + exact negate_localization_type. - + exact _. - - exact _. - Defined. - Definition rng_localization : CRing. Proof. snrapply Build_CRing. - - snrapply Build_Ring. - + exact abgroup_localization. - + exact mult_localization_type. - + exact one_localization_type. - + exact leftdistribute_localization_type. - + exact rightdistribute_localization_type. - + exact _. - - exact _. + { snrapply Build_Ring. + - snrapply Build_AbGroup. + + snrapply Build_Group. + * exact Localization_type. + * exact plus_localization_type. + * exact zero_localization_type. + * exact negate_localization_type. + * exact _. + + exact _. + - exact mult_localization_type. + - exact one_localization_type. + - exact leftdistribute_localization_type. + - exact rightdistribute_localization_type. + - exact _. } + exact _. Defined. Definition loc_in : R $-> rng_localization. From 3fc281be495ba00aae6b8f380fb734c43e94426a Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 19 Sep 2024 11:33:35 +0200 Subject: [PATCH 15/28] add smart constructors for AbGroup and CRing, drop laws for Loc Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/AbelianGroup.v | 22 +++++++ theories/Algebra/AbGroups/Z.v | 16 +++-- theories/Algebra/Rings/CRing.v | 20 +++--- theories/Algebra/Rings/Localization.v | 83 ++++-------------------- theories/Algebra/Rings/Z.v | 5 +- 5 files changed, 58 insertions(+), 88 deletions(-) diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v index 5cd6a5d22ec..89b27f2e93e 100644 --- a/theories/Algebra/AbGroups/AbelianGroup.v +++ b/theories/Algebra/AbGroups/AbelianGroup.v @@ -29,6 +29,28 @@ Proof. split; exact _. Defined. +(** Easier way to build abelian groups without redundant information. *) +Definition Build_AbGroup' (G : Type) + `{Zero G, Negate G, Plus G, IsHSet G} + (comm : Commutative (A:=G) (+)) + (assoc : Associative (A:=G) (+)) + (unit_l : LeftIdentity (A:=G) (+) 0) + (inv_l : LeftInverse (A:=G) (+) (-) 0) + : AbGroup. +Proof. + snrapply Build_AbGroup. + - (* TODO: introduce smart constructor for [Build_Group] *) + rapply (Build_Group G). + repeat split; only 1-3, 5: exact _. + + intros x. + lhs nrapply comm. + exact (unit_l x). + + intros x. + lhs nrapply comm. + exact (inv_l x). + - exact comm. +Defined. + Definition issig_abgroup : _ <~> AbGroup := ltac:(issig). Global Instance zero_abgroup (A : AbGroup) : Zero A := group_unit. diff --git a/theories/Algebra/AbGroups/Z.v b/theories/Algebra/AbGroups/Z.v index c8a31d9eec2..2c9b32a525f 100644 --- a/theories/Algebra/AbGroups/Z.v +++ b/theories/Algebra/AbGroups/Z.v @@ -12,14 +12,16 @@ Local Open Scope int_scope. Definition abgroup_Z@{} : AbGroup@{Set}. Proof. - snrapply Build_AbGroup. - - refine (Build_Group Int int_add 0 int_neg _); repeat split. - + exact _. - + exact int_add_assoc. - + exact int_add_0_r. - + exact int_add_neg_l. - + exact int_add_neg_r. + snrapply Build_AbGroup'. + - exact Int. + - exact 0. + - exact int_neg. + - exact int_add. + - exact _. - exact int_add_comm. + - exact int_add_assoc. + - exact int_add_0_l. + - exact int_add_neg_l. Defined. (** For every group [G] and element [g : G], the map sending an integer to that power of [g] is a homomorphism. See [ab_mul] for the homomorphism [G -> G] when [G] is abelian. *) diff --git a/theories/Algebra/Rings/CRing.v b/theories/Algebra/Rings/CRing.v index a4f2ee3cd01..91fd19cd668 100644 --- a/theories/Algebra/Rings/CRing.v +++ b/theories/Algebra/Rings/CRing.v @@ -23,17 +23,21 @@ Global Instance cring_plus {R : CRing} : Plus R := plus_abgroup R. Global Instance cring_zero {R : CRing} : Zero R := zero_abgroup R. Global Instance cring_negate {R : CRing} : Negate R := negate_abgroup R. -Definition Build_CRing' (R : AbGroup) - `(!One R, !Mult R, !Commutative (.*.), !LeftDistribute (.*.) (+), @IsMonoid R (.*.) 1) +Definition Build_CRing' (R : AbGroup) `(!One R, !Mult R) + (comm : Commutative (.*.)) (assoc : Associative (.*.)) + (dist_l : LeftDistribute (.*.) (+)) (unit_l : LeftIdentity (.*.) 1) : CRing. Proof. snrapply Build_CRing. - - snrapply (Build_Ring R). - 1-3,5: exact _. - intros x y z. - lhs rapply commutativity. - lhs rapply simple_distribute_l. - f_ap. + - rapply (Build_Ring R); only 1: exact _. + 2: repeat split; only 1-3: exact _. + + intros x y z. + lhs nrapply comm. + lhs rapply dist_l. + f_ap. + + intros x. + lhs rapply comm. + apply unit_l. - exact _. Defined. diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v index 0ff826727d5..957da4537ec 100644 --- a/theories/Algebra/Rings/Localization.v +++ b/theories/Algebra/Rings/Localization.v @@ -286,6 +286,17 @@ Section Localization. Defined. (** *** Ring laws *) + + (** Commutativity of addition *) + Instance commutative_plus_localization_type + : Commutative plus_localization_type. + Proof. + intros x; srapply Localization_type_ind_hprop; intros y; revert x. + srapply Localization_type_ind_hprop; intros x. + apply loc_frac_eq, fraction_eq_simple; simpl. + rewrite (rng_mult_comm (denominator y) (denominator x)). + f_ap; apply rng_plus_comm. + Defined. (** Left additive identity *) Instance leftidentity_plus_localization_type @@ -301,19 +312,6 @@ Section Localization. apply rng_mult_one_l. Defined. - Instance rightidentity_plus_localization_type - : RightIdentity plus_localization_type zero_localization_type. - Proof. - srapply Localization_type_ind_hprop; intros f. - apply loc_frac_eq, fraction_eq_simple; simpl. - f_ap. - - rewrite rng_mult_zero_l. - rewrite rng_plus_zero_r. - apply rng_mult_one_r. - - symmetry. - apply rng_mult_one_r. - Defined. - Instance leftinverse_plus_localization_type : LeftInverse plus_localization_type negate_localization_type zero_localization_type. Proof. @@ -325,17 +323,6 @@ Section Localization. apply rng_plus_negate_l. Defined. - Instance rightinverse_plus_localization_type - : RightInverse plus_localization_type negate_localization_type zero_localization_type. - Proof. - srapply Localization_type_ind_hprop; intros f. - apply loc_frac_eq, fraction_eq_simple; simpl. - refine (rng_mult_one_r _ @ _). - refine (_ @ (rng_mult_zero_l _)^). - rewrite rng_mult_negate_l. - apply rng_plus_negate_r. - Defined. - Instance associative_plus_localization_type : Associative plus_localization_type. Proof. @@ -355,16 +342,6 @@ Section Localization. apply rng_mult_comm. Defined. - Instance commutative_plus_localization_type - : Commutative plus_localization_type. - Proof. - intros x; srapply Localization_type_ind_hprop; intros y; revert x. - srapply Localization_type_ind_hprop; intros x. - apply loc_frac_eq, fraction_eq_simple; simpl. - rewrite (rng_mult_comm (denominator y) (denominator x)). - f_ap; apply rng_plus_comm. - Defined. - Instance leftidentity_mult_localization_type : LeftIdentity mult_localization_type one_localization_type. Proof. @@ -373,14 +350,6 @@ Section Localization. f_ap; [|symmetry]; apply rng_mult_one_l. Defined. - Instance rightidentity_mult_localization_type - : RightIdentity mult_localization_type one_localization_type. - Proof. - srapply Localization_type_ind_hprop; intros f. - apply loc_frac_eq, fraction_eq_simple; simpl. - f_ap; [|symmetry]; apply rng_mult_one_r. - Defined. - Instance associative_mult_localization_type : Associative mult_localization_type. Proof. @@ -422,35 +391,11 @@ Section Localization. all: f_ap. Defined. - Instance rightdistribute_localization_type - : RightDistribute mult_localization_type plus_localization_type. - Proof. - intros x y z. - rewrite 3 (commutative_mult_localization_type _ z). - snrapply leftdistribute_localization_type. - Defined. - - Instance isring_localization_type : IsRing Localization_type - := ltac:(repeat split; exact _). - Definition rng_localization : CRing. Proof. - snrapply Build_CRing. - { snrapply Build_Ring. - - snrapply Build_AbGroup. - + snrapply Build_Group. - * exact Localization_type. - * exact plus_localization_type. - * exact zero_localization_type. - * exact negate_localization_type. - * exact _. - + exact _. - - exact mult_localization_type. - - exact one_localization_type. - - exact leftdistribute_localization_type. - - exact rightdistribute_localization_type. - - exact _. } - exact _. + snrapply Build_CRing'. + 1: rapply (Build_AbGroup' Localization_type). + all: exact _. Defined. Definition loc_in : R $-> rng_localization. diff --git a/theories/Algebra/Rings/Z.v b/theories/Algebra/Rings/Z.v index 8f8c8a25098..0d9cf3b124b 100644 --- a/theories/Algebra/Rings/Z.v +++ b/theories/Algebra/Rings/Z.v @@ -10,16 +10,13 @@ Require Import WildCat.Core. Definition cring_Z : CRing. Proof. snrapply Build_CRing'. - 6: repeat split. - exact abgroup_Z. - exact 1%int. - exact int_mul. - exact int_mul_comm. - - exact int_dist_l. - - exact _. - exact int_mul_assoc. + - exact int_dist_l. - exact int_mul_1_l. - - exact int_mul_1_r. Defined. Local Open Scope mc_scope. From 3883168db9fd446a12e5094a23879c734c975fdd Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 19 Sep 2024 18:13:52 +0200 Subject: [PATCH 16/28] add more comments Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/Localization.v | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v index 957da4537ec..5de15c7430f 100644 --- a/theories/Algebra/Rings/Localization.v +++ b/theories/Algebra/Rings/Localization.v @@ -76,6 +76,7 @@ Section Localization. in_mult_subset_denominator : S denominator ; }. + (** We consider two fractions to be equal if we can rearrange the fractions as products and ask for equality upto some scaling factor from the multiplicative subset [S]. *) Definition fraction_eq : Relation Fraction. Proof. intros [n1 d1 ?] [n2 d2 ?]. @@ -95,21 +96,26 @@ Section Localization. exact (ap (1 *.) p). Defined. + (** Fraction equality is a reflexive relation. *) Definition fraction_eq_refl f1 : fraction_eq f1 f1. Proof. apply fraction_eq_simple. reflexivity. Defined. + (** The underlying type of the localization of a commutative ring is the quotient of the type of fractions by fraction equality. *) Definition Localization_type : Type := Quotient fraction_eq. + (** Given any fraction, we have an obvious inclusion into the localization type. *) Definition loc_frac : Fraction -> Localization_type := class_of fraction_eq. + (** In order to give an equality of included fractions, it suffices to show that the fractions are equal under fraction equality. *) Definition loc_frac_eq {f1 f2 : Fraction} (p : fraction_eq f1 f2) : loc_frac f1 = loc_frac f2 := qglue p. + (** We can give an induction principle for the localization type. *) Definition Localization_type_ind (Q : Localization_type -> Type) `{forall x, IsHSet (Q x)} (frac : forall f, Q (loc_frac f)) From a803cb023e6adf8587c2eed84fb20fdbe35c14ed Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 19 Sep 2024 18:35:53 +0200 Subject: [PATCH 17/28] add invertibility being preserved Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/Localization.v | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v index 5de15c7430f..609095b2d0e 100644 --- a/theories/Algebra/Rings/Localization.v +++ b/theories/Algebra/Rings/Localization.v @@ -530,6 +530,11 @@ Section Localization. exact (in_mult_subset_denominator f). Defined. + (** Elements that were invertible in the original ring [R], continue to be invertible in [rng_localization R S]. Since [loc_in] is a ring homomorphism this is automatic. *) + Definition isinvertible_rng_localization_preserved (x : R) + : IsInvertible R x -> IsInvertible rng_localization (loc_in x) + := _. + (** We can factor any fraction as the multiplication of the numerator and the inverse of the denominator. *) Definition fraction_decompose (f : Fraction) : loc_frac f From 051368f5ef37860e95b1c264d791124c059f5fcc Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Thu, 19 Sep 2024 14:56:24 -0400 Subject: [PATCH 18/28] Rings/Localization: fix hyp for rng_localization_rec_map --- theories/Algebra/Rings/Localization.v | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v index 609095b2d0e..57097ad3105 100644 --- a/theories/Algebra/Rings/Localization.v +++ b/theories/Algebra/Rings/Localization.v @@ -426,12 +426,14 @@ Section Localization. Section Rec. Context (T : CRing) (f : R $-> T) - (H : forall x, IsInvertible T (f x)). + (H : forall x, S x -> IsInvertible T (f x)). Definition rng_localization_rec_map : rng_localization -> T. Proof. srapply Localization_type_rec. - - exact (fun x => f (numerator x) * inverse_elem (f (denominator x))). + - intros [n d sd]. + refine (f n * inverse_elem (f d)). + exact (H d sd). - simpl. intros x y z. apply rng_inv_moveR_rV. @@ -440,7 +442,9 @@ Section Localization. apply rng_inv_moveL_Vr. lhs_V nrapply rng_homo_mult. rhs_V nrapply rng_homo_mult. - apply (equiv_ap (f z.1 *.)). + nrapply (equiv_inj (f z.1 *.)). + { nrapply isequiv_rng_inv_mult_l. + exact (H _ (fst z.2)). } lhs_V nrapply rng_homo_mult. rhs_V nrapply rng_homo_mult. lhs nrapply ap. From 2a32e134af50ead423583fc56401f6ed00cdce49 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Thu, 19 Sep 2024 15:07:15 -0400 Subject: [PATCH 19/28] Rings/Localization: two minor changes --- theories/Algebra/Rings/Localization.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v index 57097ad3105..cf75674b9c1 100644 --- a/theories/Algebra/Rings/Localization.v +++ b/theories/Algebra/Rings/Localization.v @@ -478,7 +478,7 @@ Section Localization. 1,2: symmetry. * apply rng_inv_l. * apply rng_inv_r. - + hnf; simpl; rewrite rng_homo_zero. + + hnf; simpl. rewrite rng_homo_zero. nrapply rng_mult_zero_l. - snrapply Build_IsMonoidPreserving. + intros x; rapply Localization_type_ind_hprop. @@ -576,7 +576,7 @@ Section Localization. - exact p. - hnf; intros x H q. change (inverse_elem (f x) = inverse_elem (g x)). - apply equiv_path_inverse_elem. + apply isinvertible_unique. exact q. - hnf; intros x y q r. lhs nrapply rng_homo_mult. From 62ba9933da3fdea7997cc568ee40e5afbf045712 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 19 Sep 2024 22:43:35 +0200 Subject: [PATCH 20/28] add Quotient_ind_hprop, Quotient_ind2_hprop and Quotient_ind3_hprop Signed-off-by: Ali Caglayan --- theories/Colimits/Quotient.v | 42 ++++++++++++++++++++++++++---------- 1 file changed, 31 insertions(+), 11 deletions(-) diff --git a/theories/Colimits/Quotient.v b/theories/Colimits/Quotient.v index aa71e8624a9..f8dfda5c1a8 100644 --- a/theories/Colimits/Quotient.v +++ b/theories/Colimits/Quotient.v @@ -91,6 +91,37 @@ Arguments Quotient_rec_beta_qglue : simpl never. Notation "A / R" := (Quotient (A:=A) R). +(* Quotient induction into a hprop. *) +Definition Quotient_ind_hprop {A : Type@{i}} (R : Relation@{i j} A) + (P : A / R -> Type) `{forall x, IsHProp (P x)} + (dclass : forall x, P (class_of R x)) : forall q, P q. +Proof. + srapply (Quotient_ind R P dclass). + all: try (intro; apply trunc_succ). + intros x y p. + apply path_ishprop. +Defined. + +Definition Quotient_ind2_hprop {A : Type@{i}} (R : Relation@{i j} A) + (P : A / R -> A / R -> Type) `{forall x y, IsHProp (P x y)} + (dclass : forall x y, P (class_of R x) (class_of R y)) + : forall x y, P x y. +Proof. + intros x; srapply Quotient_ind_hprop; intros y. + revert x; srapply Quotient_ind_hprop; intros x. + exact (dclass x y). +Defined. + +Definition Quotient_ind3_hprop {A : Type@{i}} (R : Relation@{i j} A) + (P : A / R -> A / R -> A / R -> Type) `{forall x y z, IsHProp (P x y z)} + (dclass : forall x y z, P (class_of R x) (class_of R y) (class_of R z)) + : forall x y z, P x y z. +Proof. + intros x; srapply Quotient_ind2_hprop; intros y z. + revert x; srapply Quotient_ind_hprop; intros x. + exact (dclass x y z). +Defined. + Section Equiv. Context `{Univalence} {A : Type} (R : Relation A) `{is_mere_relation _ R} @@ -109,17 +140,6 @@ Section Equiv. apply (transitivity p). Defined. - (* Quotient induction into a hprop. *) - Definition Quotient_ind_hprop - (P : A / R -> Type) `{forall x, IsHProp (P x)} - (dclass : forall x, P (class_of R x)) : forall q, P q. - Proof. - srapply (Quotient_ind R P dclass). - all: try (intro; apply trunc_succ). - intros x y p. - apply path_ishprop. - Defined. - (* Being in a class is decidable if the Relation is decidable. *) Global Instance decidable_in_class `{forall x y, Decidable (R x y)} : forall x a, Decidable (in_class x a). From ca2dbd073f2b901b1f8a0ab71e468eaf5ef890e3 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 19 Sep 2024 22:44:37 +0200 Subject: [PATCH 21/28] add QuotientRing_rec and QuotientRing_ind2_hprop Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/QuotientRing.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/theories/Algebra/Rings/QuotientRing.v b/theories/Algebra/Rings/QuotientRing.v index caeec5bcb26..24817b35ed1 100644 --- a/theories/Algebra/Rings/QuotientRing.v +++ b/theories/Algebra/Rings/QuotientRing.v @@ -138,6 +138,25 @@ Definition QuotientRing_ind_hprop {R : Ring} {I : Ideal R} (P : R / I -> Type) : forall (r : R / I), P r := Quotient_ind_hprop _ P c. +Definition QuotientRing_ind2_hprop {R : Ring} {I : Ideal R} (P : R / I -> R / I -> Type) + `{forall x y, IsHProp (P x y)} + (c : forall (x y : R), P (rng_quotient_map I x) (rng_quotient_map I y)) + : forall (r s : R / I), P r s + := Quotient_ind2_hprop _ P c. + +Definition QuotientRing_rec {R : Ring} {I : Ideal R} (S : Ring) + (f : R $-> S) (H : forall x, I x -> f x = 0) + : R / I $-> S. +Proof. + snrapply Build_RingHomomorphism'. + - snrapply (grp_quotient_rec _ _ f). + exact H. + - split. + + srapply QuotientRing_ind2_hprop. + nrapply rng_homo_mult. + + nrapply rng_homo_one. +Defined. + (** ** Quotient thoery *) (** First isomorphism theorem for commutative rings *) From ba5ff3accecd3b4c01eff822f60f01a0d0540023 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 19 Sep 2024 22:46:19 +0200 Subject: [PATCH 22/28] add cring variants of ring quotient Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/CRing.v | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/theories/Algebra/Rings/CRing.v b/theories/Algebra/Rings/CRing.v index 91fd19cd668..1259284c0fb 100644 --- a/theories/Algebra/Rings/CRing.v +++ b/theories/Algebra/Rings/CRing.v @@ -2,7 +2,7 @@ Require Import WildCat. (* Some of the material in abstract_algebra and canonical names could be selectively exported to the user, as is done in Groups/Group.v. *) Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.AbGroups. -Require Export Algebra.Rings.Ring Algebra.Rings.Ideal. +Require Export Algebra.Rings.Ring Algebra.Rings.Ideal Algebra.Rings.QuotientRing. (** * Commutative Rings *) @@ -259,3 +259,23 @@ Global Instance is01cat_CRing : Is01Cat CRing := is01cat_induced cring_ring. Global Instance is2graph_CRing : Is2Graph CRing := is2graph_induced cring_ring. Global Instance is1cat_CRing : Is1Cat CRing := is1cat_induced cring_ring. Global Instance hasequiv_CRing : HasEquivs CRing := hasequivs_induced cring_ring. + +(** ** Quotient rings *) + +Global Instance commutative_quotientring_mult (R : CRing) (I : Ideal R) + : Commutative (A:=QuotientRing R I) (.*.). +Proof. + intros x; srapply QuotientRing_ind_hprop; intros y; revert x. + srapply QuotientRing_ind_hprop; intros x; hnf. + lhs_V nrapply rng_homo_mult. + rhs_V nrapply rng_homo_mult. + snrapply ap. + apply commutativity. +Defined. + +Definition cring_quotient (R : CRing) (I : Ideal R) : CRing + := Build_CRing (QuotientRing R I) _. + +Definition cring_quotient_map {R : CRing} (I : Ideal R) + : R $-> cring_quotient R I + := rng_quotient_map I. From 90465149312a180887bd387c380609c5ebb6e973 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 19 Sep 2024 22:52:01 +0200 Subject: [PATCH 23/28] remove Localization_type and simplify using new quotient inds Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/Localization.v | 114 ++++++++++---------------- 1 file changed, 42 insertions(+), 72 deletions(-) diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v index cf75674b9c1..e3800379b0f 100644 --- a/theories/Algebra/Rings/Localization.v +++ b/theories/Algebra/Rings/Localization.v @@ -1,5 +1,6 @@ -Require Import Basics.Overture Basics.Trunc Basics.Tactics WildCat.Core - abstract_algebra Rings.CRing Truncations.Core Nat.Core. +Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient + abstract_algebra Rings.CRing Truncations.Core Nat.Core + Rings.QuotientRing WildCat.Core WildCat.Equiv. Local Open Scope mc_scope. @@ -52,7 +53,7 @@ Section Localization. (** We now construct the localization of a ring at a multiplicative subset as the following HIT: <<< - HIT Localization_type (R : CRing) (S : R -> Type) + HIT (Quotient fraction_eq) (R : CRing) (S : R -> Type) `{IsMultiplicativeSubset R} := | loc_frac (n d : R) (p : S d) : Localization R S | loc_frac_eq (n1 d1 n2 d2 : R) (p1 : S d1) (p2 : S d2) @@ -103,11 +104,9 @@ Section Localization. reflexivity. Defined. - (** The underlying type of the localization of a commutative ring is the quotient of the type of fractions by fraction equality. *) - Definition Localization_type : Type := Quotient fraction_eq. (** Given any fraction, we have an obvious inclusion into the localization type. *) - Definition loc_frac : Fraction -> Localization_type + Definition loc_frac : Fraction -> Quotient fraction_eq := class_of fraction_eq. (** In order to give an equality of included fractions, it suffices to show that the fractions are equal under fraction equality. *) @@ -115,25 +114,6 @@ Section Localization. : loc_frac f1 = loc_frac f2 := qglue p. - (** We can give an induction principle for the localization type. *) - Definition Localization_type_ind (Q : Localization_type -> Type) - `{forall x, IsHSet (Q x)} - (frac : forall f, Q (loc_frac f)) - (eq : forall f1 f2 p, loc_frac_eq p # frac f1 = frac f2) - : forall x, Q x - := Quotient_ind _ Q frac eq. - - Definition Localization_type_ind_hprop (Q : Localization_type -> Type) - `{forall x, IsHProp (Q x)} (f : forall f, Q (loc_frac f)) - : forall x, Q x - := Quotient_ind_hprop _ Q f. - - Definition Localization_type_rec (Q : Type) `{IsHSet Q} - (f : Fraction -> Q) - (t : forall f1 f2, fraction_eq f1 f2 -> f f1 = f f2) - : Localization_type -> Q - := Quotient_rec _ Q f t. - Arguments loc_frac : simpl never. Arguments loc_frac_eq : simpl never. @@ -197,7 +177,7 @@ Section Localization. Defined. (** The addition operation on the localization is induced from the addition operation for fractions. *) - Instance plus_localization_type : Plus Localization_type. + Instance plus_rng_localization : Plus (Quotient fraction_eq). Proof. srapply Quotient_rec2. - rapply fraction_eq_refl. @@ -243,7 +223,7 @@ Section Localization. f_ap. Defined. - Instance mult_localization_type : Mult Localization_type. + Instance mult_rng_localization: Mult (Quotient fraction_eq). Proof. srapply Quotient_rec2. - rapply fraction_eq_refl. @@ -259,12 +239,12 @@ Section Localization. (** *** Zero element *) - Instance zero_localization_type : Zero Localization_type + Instance zero_rng_localization : Zero (Quotient fraction_eq) := loc_frac (Build_Fraction 0 1 mss_one). (** *** One element *) - Instance one_localization_type : One Localization_type + Instance one_rng_localization : One (Quotient fraction_eq) := loc_frac (Build_Fraction 1 1 mss_one). (** *** Negation operation *) @@ -281,9 +261,9 @@ Section Localization. f_ap. Defined. - Instance negate_localization_type : Negate Localization_type. + Instance negate_rng_localization : Negate (Quotient fraction_eq). Proof. - srapply Localization_type_rec. + srapply Quotient_rec. - intros f. apply loc_frac. exact (frac_negate f). @@ -294,21 +274,20 @@ Section Localization. (** *** Ring laws *) (** Commutativity of addition *) - Instance commutative_plus_localization_type - : Commutative plus_localization_type. + Instance commutative_plus_rng_localization + : Commutative plus_rng_localization. Proof. - intros x; srapply Localization_type_ind_hprop; intros y; revert x. - srapply Localization_type_ind_hprop; intros x. + srapply Quotient_ind2_hprop; intros x y. apply loc_frac_eq, fraction_eq_simple; simpl. rewrite (rng_mult_comm (denominator y) (denominator x)). f_ap; apply rng_plus_comm. Defined. (** Left additive identity *) - Instance leftidentity_plus_localization_type - : LeftIdentity plus_localization_type zero_localization_type. + Instance leftidentity_plus_rng_localization + : LeftIdentity plus_rng_localization zero_rng_localization. Proof. - srapply Localization_type_ind_hprop; intros f. + srapply Quotient_ind_hprop; intros f. apply loc_frac_eq, fraction_eq_simple; simpl. f_ap. - rewrite rng_mult_zero_l. @@ -318,10 +297,10 @@ Section Localization. apply rng_mult_one_l. Defined. - Instance leftinverse_plus_localization_type - : LeftInverse plus_localization_type negate_localization_type zero_localization_type. + Instance leftinverse_plus_rng_localization + : LeftInverse plus_rng_localization negate_rng_localization zero_rng_localization. Proof. - srapply Localization_type_ind_hprop; intros f. + srapply Quotient_ind_hprop; intros f. apply loc_frac_eq, fraction_eq_simple; simpl. refine (rng_mult_one_r _ @ _). refine (_ @ (rng_mult_zero_l _)^). @@ -329,12 +308,10 @@ Section Localization. apply rng_plus_negate_l. Defined. - Instance associative_plus_localization_type - : Associative plus_localization_type. + Instance associative_plus_rng_localization + : Associative plus_rng_localization. Proof. - intros x y; srapply Localization_type_ind_hprop; intros z; revert y. - srapply Localization_type_ind_hprop; intros y; revert x. - srapply Localization_type_ind_hprop; intros x. + srapply Quotient_ind3_hprop; intros x y z. apply loc_frac_eq, fraction_eq_simple. simpl. rewrite ? rng_dist_r. @@ -348,39 +325,34 @@ Section Localization. apply rng_mult_comm. Defined. - Instance leftidentity_mult_localization_type - : LeftIdentity mult_localization_type one_localization_type. + Instance leftidentity_mult_rng_localization + : LeftIdentity mult_rng_localization one_rng_localization. Proof. - srapply Localization_type_ind_hprop; intros f. + srapply Quotient_ind_hprop; intros f. apply loc_frac_eq, fraction_eq_simple; simpl. f_ap; [|symmetry]; apply rng_mult_one_l. Defined. - Instance associative_mult_localization_type - : Associative mult_localization_type. + Instance associative_mult_rng_localization + : Associative mult_rng_localization. Proof. - intros x y; srapply Localization_type_ind_hprop; intros z; revert y. - srapply Localization_type_ind_hprop; intros y; revert x. - srapply Localization_type_ind_hprop; intros x. + srapply Quotient_ind3_hprop; intros x y z. apply loc_frac_eq, fraction_eq_simple. f_ap; [|symmetry]; apply rng_mult_assoc. Defined. - Instance commutative_mult_localization_type - : Commutative mult_localization_type. + Instance commutative_mult_rng_localization + : Commutative mult_rng_localization. Proof. - intros x; srapply Localization_type_ind_hprop; intros y; revert x. - srapply Localization_type_ind_hprop; intros x. + srapply Quotient_ind2_hprop; intros x y. apply loc_frac_eq, fraction_eq_simple; simpl. f_ap; rapply rng_mult_comm. Defined. - Instance leftdistribute_localization_type - : LeftDistribute mult_localization_type plus_localization_type. + Instance leftdistribute_rng_localization + : LeftDistribute mult_rng_localization plus_rng_localization. Proof. - intros x y; srapply Localization_type_ind_hprop; intros z; revert y. - srapply Localization_type_ind_hprop; intros y; revert x. - srapply Localization_type_ind_hprop; intros x. + srapply Quotient_ind3_hprop; intros x y z. apply loc_frac_eq, fraction_eq_simple. simpl. rewrite ? rng_dist_l, ? rng_dist_r. @@ -400,7 +372,7 @@ Section Localization. Definition rng_localization : CRing. Proof. snrapply Build_CRing'. - 1: rapply (Build_AbGroup' Localization_type). + 1: rapply (Build_AbGroup' (Quotient fraction_eq)). all: exact _. Defined. @@ -430,7 +402,7 @@ Section Localization. Definition rng_localization_rec_map : rng_localization -> T. Proof. - srapply Localization_type_rec. + srapply Quotient_rec. - intros [n d sd]. refine (f n * inverse_elem (f d)). exact (H d sd). @@ -460,9 +432,8 @@ Section Localization. Proof. snrapply Build_IsSemiRingPreserving. - snrapply Build_IsMonoidPreserving. - + intros x; rapply Localization_type_ind_hprop. - intros y; revert x; rapply Localization_type_ind_hprop; intros x. - simpl. + + srapply Quotient_ind2_hprop. + intros x y; simpl. apply rng_inv_moveR_rV. rhs nrapply rng_dist_r. rewrite rng_homo_plus. @@ -481,9 +452,8 @@ Section Localization. + hnf; simpl. rewrite rng_homo_zero. nrapply rng_mult_zero_l. - snrapply Build_IsMonoidPreserving. - + intros x; rapply Localization_type_ind_hprop. - intros y; revert x; rapply Localization_type_ind_hprop; intros x. - simpl. + + srapply Quotient_ind2_hprop. + intros x y; simpl. apply rng_inv_moveR_rV. lhs nrapply rng_homo_mult. rhs_V nrapply rng_mult_assoc. @@ -557,7 +527,7 @@ Section Localization. (Hmul : forall x y, P x -> P y -> P (x * y)) : forall x, P x. Proof. - srapply Localization_type_ind. + srapply Quotient_ind. - intros f. refine (transport P (fraction_decompose f)^ _). apply Hmul. From ad3d7461e203370c5f70af3386cc00de206dc225 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 19 Sep 2024 22:57:10 +0200 Subject: [PATCH 24/28] remove loc_frac and loc_frac_eq Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/Localization.v | 63 +++++++++++---------------- 1 file changed, 25 insertions(+), 38 deletions(-) diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v index e3800379b0f..94721b42c70 100644 --- a/theories/Algebra/Rings/Localization.v +++ b/theories/Algebra/Rings/Localization.v @@ -104,19 +104,6 @@ Section Localization. reflexivity. Defined. - - (** Given any fraction, we have an obvious inclusion into the localization type. *) - Definition loc_frac : Fraction -> Quotient fraction_eq - := class_of fraction_eq. - - (** In order to give an equality of included fractions, it suffices to show that the fractions are equal under fraction equality. *) - Definition loc_frac_eq {f1 f2 : Fraction} (p : fraction_eq f1 f2) - : loc_frac f1 = loc_frac f2 - := qglue p. - - Arguments loc_frac : simpl never. - Arguments loc_frac_eq : simpl never. - (** Elements of [R] can be considered fractions. *) Definition frac_in : R -> Fraction := fun r => Build_Fraction r 1 mss_one. @@ -183,10 +170,10 @@ Section Localization. - rapply fraction_eq_refl. - cbn. intros f1 f2. - exact (loc_frac (frac_add f1 f2)). + exact (class_of _ (frac_add f1 f2)). - cbn beta. intros f1 f1' p f2 f2' q. - by apply loc_frac_eq, frac_add_wd. + by apply qglue, frac_add_wd. Defined. (** *** Multiplication operation *) @@ -229,23 +216,23 @@ Section Localization. - rapply fraction_eq_refl. - cbn. intros f1 f2. - exact (loc_frac (frac_mult f1 f2)). + exact (class_of _ (frac_mult f1 f2)). - cbn beta. intros f1 f1' p f2 f2' q. - transitivity (loc_frac (frac_mult f1' f2)). - + by apply loc_frac_eq, frac_mult_wd_l. - + by apply loc_frac_eq, frac_mult_wd_r. + transitivity (class_of fraction_eq (frac_mult f1' f2)). + + by apply qglue, frac_mult_wd_l. + + by apply qglue, frac_mult_wd_r. Defined. (** *** Zero element *) Instance zero_rng_localization : Zero (Quotient fraction_eq) - := loc_frac (Build_Fraction 0 1 mss_one). + := class_of _ (Build_Fraction 0 1 mss_one). (** *** One element *) Instance one_rng_localization : One (Quotient fraction_eq) - := loc_frac (Build_Fraction 1 1 mss_one). + := class_of _(Build_Fraction 1 1 mss_one). (** *** Negation operation *) @@ -265,10 +252,10 @@ Section Localization. Proof. srapply Quotient_rec. - intros f. - apply loc_frac. + apply class_of. exact (frac_negate f). - intros f1 f2 p. - by apply loc_frac_eq, frac_negate_wd. + by apply qglue, frac_negate_wd. Defined. (** *** Ring laws *) @@ -278,7 +265,7 @@ Section Localization. : Commutative plus_rng_localization. Proof. srapply Quotient_ind2_hprop; intros x y. - apply loc_frac_eq, fraction_eq_simple; simpl. + apply qglue, fraction_eq_simple; simpl. rewrite (rng_mult_comm (denominator y) (denominator x)). f_ap; apply rng_plus_comm. Defined. @@ -288,7 +275,7 @@ Section Localization. : LeftIdentity plus_rng_localization zero_rng_localization. Proof. srapply Quotient_ind_hprop; intros f. - apply loc_frac_eq, fraction_eq_simple; simpl. + apply qglue, fraction_eq_simple; simpl. f_ap. - rewrite rng_mult_zero_l. rewrite rng_plus_zero_l. @@ -301,7 +288,7 @@ Section Localization. : LeftInverse plus_rng_localization negate_rng_localization zero_rng_localization. Proof. srapply Quotient_ind_hprop; intros f. - apply loc_frac_eq, fraction_eq_simple; simpl. + apply qglue, fraction_eq_simple; simpl. refine (rng_mult_one_r _ @ _). refine (_ @ (rng_mult_zero_l _)^). rewrite rng_mult_negate_l. @@ -312,7 +299,7 @@ Section Localization. : Associative plus_rng_localization. Proof. srapply Quotient_ind3_hprop; intros x y z. - apply loc_frac_eq, fraction_eq_simple. + apply qglue, fraction_eq_simple. simpl. rewrite ? rng_dist_r. rewrite ? rng_mult_assoc. @@ -329,7 +316,7 @@ Section Localization. : LeftIdentity mult_rng_localization one_rng_localization. Proof. srapply Quotient_ind_hprop; intros f. - apply loc_frac_eq, fraction_eq_simple; simpl. + apply qglue, fraction_eq_simple; simpl. f_ap; [|symmetry]; apply rng_mult_one_l. Defined. @@ -337,7 +324,7 @@ Section Localization. : Associative mult_rng_localization. Proof. srapply Quotient_ind3_hprop; intros x y z. - apply loc_frac_eq, fraction_eq_simple. + apply qglue, fraction_eq_simple. f_ap; [|symmetry]; apply rng_mult_assoc. Defined. @@ -345,7 +332,7 @@ Section Localization. : Commutative mult_rng_localization. Proof. srapply Quotient_ind2_hprop; intros x y. - apply loc_frac_eq, fraction_eq_simple; simpl. + apply qglue, fraction_eq_simple; simpl. f_ap; rapply rng_mult_comm. Defined. @@ -353,7 +340,7 @@ Section Localization. : LeftDistribute mult_rng_localization plus_rng_localization. Proof. srapply Quotient_ind3_hprop; intros x y z. - apply loc_frac_eq, fraction_eq_simple. + apply qglue, fraction_eq_simple. simpl. rewrite ? rng_dist_l, ? rng_dist_r. rewrite ? rng_mult_assoc. @@ -379,17 +366,17 @@ Section Localization. Definition loc_in : R $-> rng_localization. Proof. snrapply Build_RingHomomorphism. - 1: exact (loc_frac o frac_in). + 1: exact (class_of _ o frac_in). snrapply Build_IsSemiRingPreserving. - snrapply Build_IsMonoidPreserving. + intros x y. - snrapply loc_frac_eq. + snrapply qglue. apply fraction_eq_simple. by simpl; rewrite 5 rng_mult_one_r. + reflexivity. - snrapply Build_IsMonoidPreserving. + intros x y. - snrapply loc_frac_eq. + snrapply qglue. apply fraction_eq_simple. by simpl; rewrite 3 rng_mult_one_r. + reflexivity. @@ -491,8 +478,8 @@ Section Localization. : IsInvertible rng_localization (loc_in x). Proof. snrapply isinvertible_cring. - - exact (loc_frac (Build_Fraction 1 x Sx)). - - apply loc_frac_eq, fraction_eq_simple. + - exact (class_of _ (Build_Fraction 1 x Sx)). + - apply qglue, fraction_eq_simple. exact (rng_mult_assoc _ _ _)^. Defined. @@ -511,10 +498,10 @@ Section Localization. (** We can factor any fraction as the multiplication of the numerator and the inverse of the denominator. *) Definition fraction_decompose (f : Fraction) - : loc_frac f + : class_of fraction_eq f = loc_in (numerator f) * inverse_elem (loc_in (denominator f)). Proof. - apply loc_frac_eq, fraction_eq_simple. + apply qglue, fraction_eq_simple. nrapply rng_mult_assoc. Defined. From 9088a7853d8af4976bc4990cdcb02ba591111fa7 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 19 Sep 2024 22:58:38 +0200 Subject: [PATCH 25/28] add comment about loc_frac and loc_frac_eq Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/Localization.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v index 94721b42c70..2e5197ca3a7 100644 --- a/theories/Algebra/Rings/Localization.v +++ b/theories/Algebra/Rings/Localization.v @@ -63,8 +63,7 @@ Section Localization. >>> along with the condition that this HIT be a set. - We will implement this HIT by writing it as a set quotient. - *) + We will implement this HIT by writing it as a set quotient. From now onwards, [loc_frac] will be implemented as [class_of fraction_eq] and [loc_frac_eq] will be implemented as [qglue]. *) Context (R : CRing) (S : R -> Type) `{!IsMultiplicativeSubset S}. From ac1dfb813fff01bc349e38d87e488a74fe518228 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Fri, 20 Sep 2024 14:16:27 +0200 Subject: [PATCH 26/28] homogenize variable naming in Quotient.v and reprhase some proofs Signed-off-by: Ali Caglayan --- theories/Colimits/Quotient.v | 185 ++++++++++++++++------------------- 1 file changed, 87 insertions(+), 98 deletions(-) diff --git a/theories/Colimits/Quotient.v b/theories/Colimits/Quotient.v index f8dfda5c1a8..3ee2c9cb201 100644 --- a/theories/Colimits/Quotient.v +++ b/theories/Colimits/Quotient.v @@ -17,7 +17,9 @@ Inductive Quotient R : Type := | qglue : forall x y, (R x y) -> class_of R x = class_of R y | ishset_quotient : IsHSet (Quotient R) >> -We do this by defining the quotient as a 0-truncated graph quotient. *) +We do this by defining the quotient as a 0-truncated graph quotient. + +Throughout this file [a], [b] and [c] are elements of [A], [R] is a relation on [A], [x], [y] and [z] are elements of [Quotient R], [p] is a proof of [R a b]. *) Definition Quotient@{i j k} {A : Type@{i}} (R : Relation@{i j} A) : Type@{k} := Trunc@{k} 0 (GraphQuotient@{i j k} R). @@ -25,39 +27,37 @@ Definition Quotient@{i j k} {A : Type@{i}} (R : Relation@{i j} A) : Type@{k} Definition class_of@{i j k} {A : Type@{i}} (R : Relation@{i j} A) : A -> Quotient@{i j k} R := tr o gq. -Definition qglue@{i j k} {A : Type@{i}} {R : Relation@{i j} A} - {x y : A} - : R x y -> class_of@{i j k} R x = class_of R y +Definition qglue@{i j k} {A : Type@{i}} {R : Relation@{i j} A} {a b : A} + : R a b -> class_of@{i j k} R a = class_of R b := fun p => ap tr (gqglue p). Global Instance ishset_quotient {A : Type} (R : Relation A) : IsHSet (Quotient R) := _. -Definition Quotient_ind@{i j k l} - {A : Type@{i}} (R : Relation@{i j} A) +Definition Quotient_ind@{i j k l} {A : Type@{i}} (R : Relation@{i j} A) (P : Quotient@{i j k} R -> Type@{l}) {sP : forall x, IsHSet (P x)} - (pclass : forall x, P (class_of R x)) - (peq : forall x y (H : R x y), qglue H # pclass x = pclass y) - : forall q, P q. + (pclass : forall a, P (class_of R a)) + (peq : forall a b (H : R a b), qglue H # pclass a = pclass b) + : forall x, P x. Proof. - eapply Trunc_ind, GraphQuotient_ind. - 1: assumption. - intros a b p. - refine (transport_compose _ _ _ _ @ _). - apply peq. + rapply Trunc_ind; srapply GraphQuotient_ind. + - exact pclass. + - intros a b p. + lhs nrapply (transport_compose P). + exact (peq a b p). Defined. Definition Quotient_ind_beta_qglue@{i j k l} {A : Type@{i}} (R : Relation@{i j} A) (P : Quotient@{i j k} R -> Type@{l}) {sP : forall x, IsHSet (P x)} - (pclass : forall x, P (class_of R x)) - (peq : forall x y (H : R x y), qglue H # pclass x = pclass y) - (x y : A) (p : R x y) - : apD (Quotient_ind@{i j k l} R P pclass peq) (qglue p) = peq x y p. + (pclass : forall a, P (class_of R a)) + (peq : forall a b (H : R a b), qglue H # pclass a = pclass b) + (a b : A) (p : R a b) + : apD (Quotient_ind@{i j k l} R P pclass peq) (qglue p) = peq a b p. Proof. - refine (apD_compose' tr _ _ @ _). + lhs nrapply apD_compose'. unfold Quotient_ind. - refine (ap _ (GraphQuotient_ind_beta_gqglue _ pclass + nrefine (ap _ (GraphQuotient_ind_beta_gqglue _ pclass (fun a b p0 => transport_compose P tr _ _ @ peq a b p0) _ _ _) @ _). rapply concat_V_pp. Defined. @@ -65,22 +65,23 @@ Defined. Definition Quotient_rec@{i j k l} {A : Type@{i}} (R : Relation@{i j} A) (P : Type@{l}) `{IsHSet P} (pclass : A -> P) - (peq : forall x y, R x y -> pclass x = pclass y) + (peq : forall a b, R a b -> pclass a = pclass b) : Quotient@{i j k} R -> P. Proof. - eapply Trunc_rec, GraphQuotient_rec. - apply peq. + srapply Trunc_rec; snrapply GraphQuotient_rec. + - exact pclass. + - exact peq. Defined. Definition Quotient_rec_beta_qglue @{i j k l} {A : Type@{i}} (R : Relation@{i j} A) (P : Type@{l}) `{IsHSet P} (pclass : A -> P) - (peq : forall x y, R x y -> pclass x = pclass y) - (x y : A) (p : R x y) - : ap (Quotient_rec@{i j k l} R P pclass peq) (qglue p) = peq x y p. + (peq : forall a b, R a b -> pclass a = pclass b) + (a b : A) (p : R a b) + : ap (Quotient_rec@{i j k l} R P pclass peq) (qglue p) = peq a b p. Proof. - refine ((ap_compose tr _ _)^ @ _). - srapply GraphQuotient_rec_beta_gqglue. + lhs_V nrapply (ap_compose tr). + snrapply GraphQuotient_rec_beta_gqglue. Defined. Arguments Quotient : simpl never. @@ -94,32 +95,31 @@ Notation "A / R" := (Quotient (A:=A) R). (* Quotient induction into a hprop. *) Definition Quotient_ind_hprop {A : Type@{i}} (R : Relation@{i j} A) (P : A / R -> Type) `{forall x, IsHProp (P x)} - (dclass : forall x, P (class_of R x)) : forall q, P q. + (dclass : forall a, P (class_of R a)) + : forall x, P x. Proof. srapply (Quotient_ind R P dclass). - all: try (intro; apply trunc_succ). - intros x y p. - apply path_ishprop. + intros x y p; apply path_ishprop. Defined. Definition Quotient_ind2_hprop {A : Type@{i}} (R : Relation@{i j} A) (P : A / R -> A / R -> Type) `{forall x y, IsHProp (P x y)} - (dclass : forall x y, P (class_of R x) (class_of R y)) + (dclass : forall a b, P (class_of R a) (class_of R b)) : forall x y, P x y. Proof. - intros x; srapply Quotient_ind_hprop; intros y. - revert x; srapply Quotient_ind_hprop; intros x. - exact (dclass x y). + intros x; srapply Quotient_ind_hprop; intros b. + revert x; srapply Quotient_ind_hprop; intros a. + exact (dclass a b). Defined. Definition Quotient_ind3_hprop {A : Type@{i}} (R : Relation@{i j} A) (P : A / R -> A / R -> A / R -> Type) `{forall x y z, IsHProp (P x y z)} - (dclass : forall x y z, P (class_of R x) (class_of R y) (class_of R z)) + (dclass : forall a b c, P (class_of R a) (class_of R b) (class_of R c)) : forall x y z, P x y z. Proof. - intros x; srapply Quotient_ind2_hprop; intros y z. - revert x; srapply Quotient_ind_hprop; intros x. - exact (dclass x y z). + intros x; srapply Quotient_ind2_hprop; intros b c. + revert x; srapply Quotient_ind_hprop; intros a. + exact (dclass a b c). Defined. Section Equiv. @@ -130,10 +130,10 @@ Section Equiv. (* The proposition of being in a given class in a quotient. *) Definition in_class : A / R -> A -> HProp. Proof. - intros a b; revert a. + intros x b; revert x. srapply Quotient_rec. 1: intro a; exact (Build_HProp (R a b)). - intros x y p; cbn beta. + intros a c p; cbn beta. apply path_hprop. srapply equiv_iff_hprop; cbn. 1: apply (transitivity (symmetry _ _ p)). @@ -141,14 +141,14 @@ Section Equiv. Defined. (* Being in a class is decidable if the Relation is decidable. *) - Global Instance decidable_in_class `{forall x y, Decidable (R x y)} + Global Instance decidable_in_class `{forall a b, Decidable (R a b)} : forall x a, Decidable (in_class x a). Proof. by srapply Quotient_ind_hprop. Defined. (* if x is in a class q, then the class of x is equal to q. *) - Lemma path_in_class_of : forall q x, in_class q x -> q = class_of R x. + Lemma path_in_class_of : forall x a, in_class x a -> x = class_of R a. Proof. srapply Quotient_ind. { intros x y p. @@ -158,59 +158,48 @@ Section Equiv. apply hset_path2. Defined. - Lemma related_quotient_paths : forall x y, - class_of R x = class_of R y -> R x y. + Lemma related_quotient_paths (a b : A) + : class_of R a = class_of R b -> R a b. Proof. - intros x y p. - change (in_class (class_of R x) y). + intros p. + change (in_class (class_of R a) b). destruct p^. cbv; reflexivity. Defined. (** Thm 10.1.8 *) - Theorem path_quotient : forall x y, - R x y <~> (class_of R x = class_of R y). + Theorem path_quotient (a b : A) + : R a b <~> (class_of R a = class_of R b). Proof. - intros ??. apply equiv_iff_hprop. - apply qglue. - apply related_quotient_paths. Defined. - Definition Quotient_rec2 {B : HSet} {dclass : A -> A -> B} - {dequiv : forall x x', R x x' -> forall y y', - R y y' -> dclass x y = dclass x' y'} + Definition Quotient_rec2 {B : Type} `{IsHSet B} {dclass : A -> A -> B} + {dequiv : forall a a', R a a' -> forall b b', + R b b' -> dclass a b = dclass a' b'} : A / R -> A / R -> B. Proof. clear H. (* Ensure that we don't use Univalence. *) - intro a. + intro x. srapply Quotient_rec. - { intro a'. - revert a. + - intro b. + revert x. srapply Quotient_rec. - { intro a. exact (dclass a a'). } - cbn beta. - intros x y p. - by apply (dequiv x y p a' a'). } - cbn beta. - intros x y p. - revert a. - srapply Quotient_ind. - { cbn; intro a. - by apply dequiv. } - intros a b q. - apply path_ishprop. - Defined. - - Definition Quotient_ind_hprop' (P : A / R -> Type) - `{forall x, IsHProp (P (class_of _ x))} - (dclass : forall x, P (class_of _ x)) : forall y, P y. - Proof. - apply Quotient_ind with dclass. - { srapply Quotient_ind. - 1: intro; apply istrunc_succ. - intros ???; apply path_ishprop. } - intros; apply path_ishprop. + + intro a. + exact (dclass a b). + + cbn beta. + intros a a' p. + by apply (dequiv a a' p b b). + - cbn beta. + intros b b' p. + revert x. + srapply Quotient_ind. + + cbn; intro a. + by apply dequiv. + + intros a a' q. + apply path_ishprop. Defined. (** The map class_of : A -> A/R is a surjection. *) @@ -218,15 +207,15 @@ Section Equiv. Proof. apply BuildIsSurjection. srapply Quotient_ind_hprop. - intro x. + intro a. apply tr. - by exists x. + by exists a. Defined. (* Universal property of quotient *) (* Lemma 6.10.3 *) - Theorem equiv_quotient_ump (B : HSet) - : (A / R -> B) <~> {f : A -> B & forall x y, R x y -> f x = f y}. + Theorem equiv_quotient_ump (B : Type) `{IsHSet B} + : (A / R -> B) <~> {f : A -> B & forall a b, R a b -> f a = f b}. Proof. srapply equiv_adjointify. + intro f. @@ -263,12 +252,12 @@ Section Functoriality. Definition Quotient_functor {A : Type} (R : Relation A) {B : Type} (S : Relation B) - (f : A -> B) (fresp : forall x y, R x y -> S (f x) (f y)) + (f : A -> B) (fresp : forall a b, R a b -> S (f a) (f b)) : Quotient R -> Quotient S. Proof. refine (Quotient_rec R _ (class_of S o f) _). - intros x y r. - apply qglue, fresp, r. + intros a b p. + apply qglue, fresp, p. Defined. Definition Quotient_functor_idmap @@ -282,9 +271,9 @@ Section Functoriality. {A : Type} {R : Relation A} {B : Type} {S : Relation B} {C : Type} {T : Relation C} - (f : A -> B) (fresp : forall x y, R x y -> S (f x) (f y)) - (g : B -> C) (gresp : forall x y, S x y -> T (g x) (g y)) - : Quotient_functor R T (g o f) (fun x y => (gresp _ _) o (fresp x y)) + (f : A -> B) (fresp : forall a b, R a b -> S (f a) (f b)) + (g : B -> C) (gresp : forall a b, S a b -> T (g a) (g b)) + : Quotient_functor R T (g o f) (fun a b => (gresp _ _) o (fresp a b)) == Quotient_functor S T g gresp o Quotient_functor R S f fresp. Proof. by srapply Quotient_ind_hprop. @@ -294,11 +283,11 @@ Section Functoriality. {B : Type} (S : Relation B). Global Instance isequiv_quotient_functor (f : A -> B) - (fresp : forall x y, R x y <-> S (f x) (f y)) `{IsEquiv _ _ f} - : IsEquiv (Quotient_functor R S f (fun x y => fst (fresp x y))). + (fresp : forall a b, R a b <-> S (f a) (f b)) `{IsEquiv _ _ f} + : IsEquiv (Quotient_functor R S f (fun a b => fst (fresp a b))). Proof. srapply (isequiv_adjointify _ (Quotient_functor S R f^-1 _)). - { intros u v s. + { intros a b s. apply (snd (fresp _ _)). abstract (do 2 rewrite eisretr; apply s). } all: srapply Quotient_ind. @@ -311,12 +300,12 @@ Section Functoriality. Defined. Definition equiv_quotient_functor (f : A -> B) `{IsEquiv _ _ f} - (fresp : forall x y, R x y <-> S (f x) (f y)) + (fresp : forall a b, R a b <-> S (f a) (f b)) : Quotient R <~> Quotient S - := Build_Equiv _ _ (Quotient_functor R S f (fun x y => fst (fresp x y))) _. + := Build_Equiv _ _ (Quotient_functor R S f (fun a b => fst (fresp a b))) _. Definition equiv_quotient_functor' (f : A <~> B) - (fresp : forall x y, R x y <-> S (f x) (f y)) + (fresp : forall a b, R a b <-> S (f a) (f b)) : Quotient R <~> Quotient S := equiv_quotient_functor f fresp. @@ -381,7 +370,7 @@ Definition quotient_kernel_factor@{a b ab ab' | a <= ab, b <= ab, ab < ab'} IsHSet C * IsSurjection e * IsEmbedding m * (f = m o e). Proof. exact (quotient_kernel_factor_general@{a b ab ab' b ab ab} - f (fun x y => f x = f y) (fun x y => equiv_idmap)). + f (fun a b => f a = f b) (fun x y => equiv_idmap)). Defined. (** If we use propositional resizing, we can replace [f x = f y] with a proposition [R x y] in universe [a], so that the universe of [C] is the same as the universe of [A]. *) @@ -392,5 +381,5 @@ Definition quotient_kernel_factor_small@{a a' b ab | a < a', a <= ab, b <= ab} IsHSet C * IsSurjection e * IsEmbedding m * (f = m o e). Proof. exact (quotient_kernel_factor_general@{a a a a' b ab ab} - f (fun x y => resize_hprop@{b a} (f x = f y)) (fun x y => equiv_resize_hprop _)). + f (fun a b => resize_hprop@{b a} (f a = f b)) (fun x y => equiv_resize_hprop _)). Defined. From 602903b8f429bcff39d04717ecf78ffe18934399 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Fri, 20 Sep 2024 14:17:42 +0200 Subject: [PATCH 27/28] Update theories/Algebra/Rings/QuotientRing.v Co-authored-by: Dan Christensen --- theories/Algebra/Rings/QuotientRing.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Algebra/Rings/QuotientRing.v b/theories/Algebra/Rings/QuotientRing.v index 24817b35ed1..404f0ab7d30 100644 --- a/theories/Algebra/Rings/QuotientRing.v +++ b/theories/Algebra/Rings/QuotientRing.v @@ -157,7 +157,7 @@ Proof. + nrapply rng_homo_one. Defined. -(** ** Quotient thoery *) +(** ** Quotient theory *) (** First isomorphism theorem for commutative rings *) Definition rng_first_iso `{Funext} {A B : Ring} (f : A $-> B) From d065e5c55b7b337cb396c195d75cd115fb9741b1 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Fri, 20 Sep 2024 14:27:56 +0200 Subject: [PATCH 28/28] simplify more things with Quotient_ind2/3 and Quotient_rec2 Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/AbelianGroup.v | 6 +--- theories/Algebra/AbSES/Core.v | 3 +- theories/Algebra/Groups/QuotientGroup.v | 26 ++++---------- theories/Algebra/Rings/QuotientRing.v | 45 +++++------------------- 4 files changed, 17 insertions(+), 63 deletions(-) diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v index 89b27f2e93e..0e84f177736 100644 --- a/theories/Algebra/AbGroups/AbelianGroup.v +++ b/theories/Algebra/AbGroups/AbelianGroup.v @@ -113,11 +113,7 @@ Global Instance isabgroup_quotient (G : AbGroup) (H : Subgroup G) Proof. nrapply Build_IsAbGroup. 1: exact _. - intro x. - srapply Quotient_ind_hprop. - intro y; revert x. - srapply Quotient_ind_hprop. - intro x. + srapply Quotient_ind2_hprop; intros x y. apply (ap (class_of _)). apply commutativity. Defined. diff --git a/theories/Algebra/AbSES/Core.v b/theories/Algebra/AbSES/Core.v index 5302a52c574..605ff4d72e3 100644 --- a/theories/Algebra/AbSES/Core.v +++ b/theories/Algebra/AbSES/Core.v @@ -731,8 +731,7 @@ Proof. - apply isequiv_surj_emb. 1: rapply cancelR_conn_map. apply isembedding_isinj_hset. - srapply Quotient_ind_hprop; intro x. - srapply Quotient_ind_hprop; intro y. + srapply Quotient_ind2_hprop; intros x y. intro p. apply qglue; cbn. refine (isexact_preimage (Tr (-1)) _ _ (-x + y) _). diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v index 9acacb0232d..91c0c3396f1 100644 --- a/theories/Algebra/Groups/QuotientGroup.v +++ b/theories/Algebra/Groups/QuotientGroup.v @@ -27,23 +27,12 @@ Section GroupCongruenceQuotient. Global Instance congquot_sgop : SgOp CongruenceQuotient. Proof. - intros x. - srapply Quotient_rec. - { intro y; revert x. - srapply Quotient_rec. - { intros x. - apply class_of. - exact (x * y). } - intros a b r. - cbn. + srapply Quotient_rec2. + - intros x y. + exact (class_of _ (x * y)). + - intros x x' p y y' q. apply qglue. - by apply iscong. } - intros a b r. - revert x. - srapply Quotient_ind_hprop. - intro x. - apply qglue. - by apply iscong. + by apply iscong. Defined. Global Instance congquot_mon_unit : MonUnit CongruenceQuotient. @@ -72,10 +61,7 @@ Section GroupCongruenceQuotient. Global Instance congquot_sgop_associative : Associative congquot_sgop. Proof. - intros x y. - srapply Quotient_ind_hprop; intro a; revert y. - srapply Quotient_ind_hprop; intro b; revert x. - srapply Quotient_ind_hprop; intro c. + srapply Quotient_ind3_hprop; intros x y z. simpl; by rewrite associativity. Qed. diff --git a/theories/Algebra/Rings/QuotientRing.v b/theories/Algebra/Rings/QuotientRing.v index 404f0ab7d30..514c3a1a99f 100644 --- a/theories/Algebra/Rings/QuotientRing.v +++ b/theories/Algebra/Rings/QuotientRing.v @@ -40,23 +40,11 @@ Section QuotientRing. Instance mult_quotient_group : Mult (QuotientAbGroup R I). Proof. - intro x. - srapply Quotient_rec. - { intro y; revert x. - srapply Quotient_rec. - { intro x. - apply class_of. - exact (x * y). } - intros x x' p. + srapply Quotient_rec2. + - exact (fun x y => class_of _ (x * y)). + - intros x x' p y y' q; simpl. apply qglue. - by rapply iscong. } - intros y y' q. - revert x. - srapply Quotient_ind_hprop. - intro x. - simpl. - apply qglue. - by rapply iscong. + by rapply iscong. Defined. Instance one_quotient_abgroup : One (QuotientAbGroup R I) := class_of _ one. @@ -68,10 +56,7 @@ Section QuotientRing. 1: repeat split. 1: exact _. (** Associativity follows from the underlying operation *) - { intros x y. - snrapply Quotient_ind_hprop; [exact _ | intro z; revert y]. - snrapply Quotient_ind_hprop; [exact _ | intro y; revert x]. - snrapply Quotient_ind_hprop; [exact _ | intro x ]. + { srapply Quotient_ind3_hprop; intros x y z. unfold sg_op, mult_is_sg_op, mult_quotient_group; simpl. apply ap. apply associativity. } @@ -82,18 +67,12 @@ Section QuotientRing. 1: apply left_identity. 1: apply right_identity. (** Finally distributivity also follows *) - { intros x y. - snrapply Quotient_ind_hprop; [exact _ | intro z; revert y]. - snrapply Quotient_ind_hprop; [exact _ | intro y; revert x]. - snrapply Quotient_ind_hprop; [exact _ | intro x ]. + { srapply Quotient_ind3_hprop; intros x y z. unfold sg_op, mult_is_sg_op, mult_quotient_group, plus, mult, plus_quotient_group; simpl. apply ap. apply simple_distribute_l. } - { intros x y. - snrapply Quotient_ind_hprop; [exact _ | intro z; revert y]. - snrapply Quotient_ind_hprop; [exact _ | intro y; revert x]. - snrapply Quotient_ind_hprop; [exact _ | intro x ]. + { srapply Quotient_ind3_hprop; intros x y z. unfold sg_op, mult_is_sg_op, mult_quotient_group, plus, mult, plus_quotient_group; simpl. apply ap. @@ -166,9 +145,7 @@ Proof. snrapply Build_RingIsomorphism''. 1: rapply abgroup_first_iso. split. - { intros x y. - revert y; srapply QuotientRing_ind_hprop; intros y. - revert x; srapply QuotientRing_ind_hprop; intros x. + { srapply QuotientRing_ind2_hprop; intros x y. srapply path_sigma_hprop. exact (rng_homo_mult _ _ _). } srapply path_sigma_hprop. @@ -185,11 +162,7 @@ Proof. intros x y; cbn. apply p. } repeat split. - 1,2: intros x; simpl. - 1,2: srapply QuotientRing_ind_hprop. - 1,2: intros y; revert x. - 1,2: srapply QuotientRing_ind_hprop. - 1,2: intros x; rapply qglue. + 1,2: srapply Quotient_ind2_hprop; intros x y; rapply qglue. 1: change (J ( - (x + y) + (x + y))). 2: change (J (- ( x * y) + (x * y))). 1,2: rewrite rng_plus_negate_l.