{-# OPTIONS --safe #-} module Cubical.Algebra.CommRing.FiberedProduct where open import Cubical.Foundations.Prelude open import Cubical.Foundations.Function open import Cubical.Foundations.HLevels open import Cubical.Data.Sigma open import Cubical.Algebra.Ring open import Cubical.Algebra.CommRing private variable ℓ : Level module _ (A B C : CommRing ℓ) (α : CommRingHom A C) (β : CommRingHom B C) where private module A = CommRingStr (snd A) module B = CommRingStr (snd B) module C = CommRingStr (snd C) module α = IsRingHom (snd α) module β = IsRingHom (snd β) open CommRingStr open IsRingHom fbT : Type ℓ fbT = Σ[ ab ∈ fst A × fst B ] (fst α (fst ab) ≡ fst β (snd ab)) fbT≡ : {x y : fbT} → fst (fst x) ≡ fst (fst y) → snd (fst x) ≡ snd (fst y) → x ≡ y fbT≡ h1 h2 = Σ≡Prop (λ _ → is-set (snd C) _ _) λ i → (h1 i) , (h2 i) 0fbT : fbT 0fbT = (A.0r , B.0r) , α.pres0 ∙ sym β.pres0 1fbT : fbT 1fbT = (A.1r , B.1r) , α.pres1 ∙ sym β.pres1 _+fbT_ : fbT → fbT → fbT ((a1 , b1) , hab1) +fbT ((a2 , b2) , hab2) = (a1 A.+ a2 , b1 B.+ b2) , α.pres+ a1 a2 ∙∙ (λ i → hab1 i C.+ hab2 i) ∙∙ sym (β.pres+ b1 b2) _·fbT_ : fbT → fbT → fbT ((a1 , b1) , hab1) ·fbT ((a2 , b2) , hab2) = (a1 A.· a2 , b1 B.· b2) , α.pres· a1 a2 ∙∙ (λ i → hab1 i C.· hab2 i) ∙∙ sym (β.pres· b1 b2) -fbT_ : fbT → fbT -fbT ((a , b) , hab) = (A.- a , B.- b) , α.pres- a ∙∙ cong C.-_ hab ∙∙ sym (β.pres- b) fiberedProduct : CommRing ℓ fst fiberedProduct = fbT 0r (snd fiberedProduct) = 0fbT 1r (snd fiberedProduct) = 1fbT _+_ (snd fiberedProduct) = _+fbT_ _·_ (snd fiberedProduct) = _·fbT_ -_ (snd fiberedProduct) = -fbT_ isCommRing (snd fiberedProduct) = makeIsCommRing (isSetΣSndProp (isSet× (is-set (snd A)) (is-set (snd B))) λ x → is-set (snd C) _ _) (λ _ _ _ → fbT≡ (A.+Assoc _ _ _) (B.+Assoc _ _ _)) (λ _ → fbT≡ (A.+IdR _) (B.+IdR _)) (λ _ → fbT≡ (A.+InvR _) (B.+InvR _)) (λ _ _ → fbT≡ (A.+Comm _ _) (B.+Comm _ _)) (λ _ _ _ → fbT≡ (A.·Assoc _ _ _) (B.·Assoc _ _ _)) (λ _ → fbT≡ (A.·IdR _) (B.·IdR _)) (λ _ _ _ → fbT≡ (A.·DistR+ _ _ _) (B.·DistR+ _ _ _)) (λ _ _ → fbT≡ (A.·Comm _ _) (B.·Comm _ _)) fiberedProductPr₁ : CommRingHom fiberedProduct A fst fiberedProductPr₁ = fst ∘ fst snd fiberedProductPr₁ = makeIsRingHom refl (λ _ _ → refl) (λ _ _ → refl) fiberedProductPr₂ : CommRingHom fiberedProduct B fst fiberedProductPr₂ = snd ∘ fst snd fiberedProductPr₂ = makeIsRingHom refl (λ _ _ → refl) (λ _ _ → refl) fiberedProductPr₁₂Commutes : compCommRingHom fiberedProduct A C fiberedProductPr₁ α ≡ compCommRingHom fiberedProduct B C fiberedProductPr₂ β fiberedProductPr₁₂Commutes = RingHom≡ (funExt (λ x → x .snd)) fiberedProductUnivProp : (D : CommRing ℓ) (h : CommRingHom D A) (k : CommRingHom D B) → compCommRingHom D A C h α ≡ compCommRingHom D B C k β → ∃![ l ∈ CommRingHom D fiberedProduct ] (h ≡ compCommRingHom D fiberedProduct A l fiberedProductPr₁) × (k ≡ compCommRingHom D fiberedProduct B l fiberedProductPr₂) fiberedProductUnivProp D (h , hh) (k , hk) H = uniqueExists f (RingHom≡ refl , RingHom≡ refl) (λ _ → isProp× (isSetRingHom _ _ _ _) (isSetRingHom _ _ _ _)) (λ { (g , _) (Hh , Hk) → RingHom≡ (funExt (λ d → fbT≡ (funExt⁻ (cong fst Hh) d) (funExt⁻ (cong fst Hk) d))) }) where f : CommRingHom D fiberedProduct fst f d = (h d , k d) , funExt⁻ (cong fst H) d snd f = makeIsRingHom (fbT≡ (hh .pres1) (hk .pres1)) (λ _ _ → fbT≡ (hh .pres+ _ _) (hk .pres+ _ _)) (λ _ _ → fbT≡ (hh .pres· _ _) (hk .pres· _ _))