{-# OPTIONS --cubical-compatible --safe #-}
open import Tactic.RingSolver.Core.Polynomial.Parameters
module Tactic.RingSolver.Core.Polynomial.Homomorphism.Variables
{r₁ r₂ r₃ r₄}
(homo : Homomorphism r₁ r₂ r₃ r₄)
where
open import Data.Product.Base using (_,_)
open import Data.Vec.Base as Vec using (Vec)
open import Data.Fin using (Fin)
open import Data.List.Kleene
open Homomorphism homo
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Lemmas homo
open import Tactic.RingSolver.Core.Polynomial.Base (Homomorphism.from homo)
open import Tactic.RingSolver.Core.Polynomial.Reasoning (Homomorphism.to homo)
open import Tactic.RingSolver.Core.Polynomial.Semantics homo
ι-hom : ∀ {n} (i : Fin n) (Ρ : Vec Carrier n) → ⟦ ι i ⟧ Ρ ≈ Vec.lookup Ρ i
ι-hom i Ρ′ = let (ρ , Ρ) = drop-1 (space≤′n i) Ρ′ in begin
⟦ (κ Raw.1# Δ 1 ∷↓ []) ⊐↓ space≤′n i ⟧ Ρ′ ≈⟨ ⊐↓-hom (κ Raw.1# Δ 1 ∷↓ []) (space≤′n i) Ρ′ ⟩
⅀?⟦ κ Raw.1# Δ 1 ∷↓ [] ⟧ (ρ , Ρ) ≈⟨ ∷↓-hom-s (κ Raw.1#) 0 [] ρ Ρ ⟩
ρ * ⟦ κ Raw.1# ⟧ Ρ ≈⟨ *≫ 1-homo ⟩
ρ * 1# ≈⟨ *-identityʳ ρ ⟩
ρ ≡⟨ drop-1⇒lookup i Ρ′ ⟩
Vec.lookup Ρ′ i ∎