import Mathlib import Definitions.Def_GaloisRep_Adic import Definitions.Def_Deformations_TraceAlgebra namespace GaloisRep open Deformation CategoryTheory IsLocalRing def conditionLifts (π’ͺ : Type) [CommRing π’ͺ] [IsLocalRing π’ͺ] (π’Ÿ : βˆ€ ⦃A : Type⦄ [CommRing A] [IsLocalRing A] [Algebra π’ͺ A], GaloisRepAdic A β†’ Prop) (ρ₀ : (repnFunctor (Fin 2) (AlgebraicClosure β„š ≃ₐ[β„š] AlgebraicClosure β„š) π’ͺ).obj ProartinianCat.residueField) (A : ProartinianCat π’ͺ) : Set ((repnFunctor (Fin 2) (AlgebraicClosure β„š ≃ₐ[β„š] AlgebraicClosure β„š) π’ͺ).obj A) := {ρ' | ρ' ∈ (liftFunctor (Fin 2) (AlgebraicClosure β„š ≃ₐ[β„š] AlgebraicClosure β„š) π’ͺ ρ₀).obj A ∧ βˆ€ (B : ProartinianCat π’ͺ) [IsArtinianRing B] (f : A ⟢ B) (ρB : GaloisRepAdic B) (b : Module.Basis (Fin 2) B ρB.V), (βˆ€ Οƒ, LinearMap.toMatrix b b (ρB.ρ Οƒ) = ((mapRepn (Fin 2) (AlgebraicClosure β„š ≃ₐ[β„š] AlgebraicClosure β„š) π’ͺ f ρ' Οƒ : GL (Fin 2) B) : Matrix (Fin 2) (Fin 2) B)) β†’ π’Ÿ ρB} def conditionSubfunctor (π’ͺ : Type) [CommRing π’ͺ] [IsLocalRing π’ͺ] (π’Ÿ : βˆ€ ⦃A : Type⦄ [CommRing A] [IsLocalRing A] [Algebra π’ͺ A], GaloisRepAdic A β†’ Prop) (ρ₀ : (repnFunctor (Fin 2) (AlgebraicClosure β„š ≃ₐ[β„š] AlgebraicClosure β„š) π’ͺ).obj ProartinianCat.residueField) : Subfunctor (repnFunctor (Fin 2) (AlgebraicClosure β„š ≃ₐ[β„š] AlgebraicClosure β„š) π’ͺ) where obj A := conditionLifts π’ͺ π’Ÿ ρ₀ A map {A A'} g := by rintro ρ' ⟨hlift, hD⟩ refine ⟨(liftFunctor (Fin 2) (AlgebraicClosure β„š ≃ₐ[β„š] AlgebraicClosure β„š) π’ͺ ρ₀).map g hlift, ?_⟩ intro B _ f ρB b hb refine hD B (g ≫ f) ρB b (fun Οƒ => ?_) rw [hb Οƒ] simp only [mapRepn, Functor.map_comp, types_comp_apply] @[simp] lemma conditionSubfunctor_obj (π’ͺ : Type) [CommRing π’ͺ] [IsLocalRing π’ͺ] (π’Ÿ : βˆ€ ⦃A : Type⦄ [CommRing A] [IsLocalRing A] [Algebra π’ͺ A], GaloisRepAdic A β†’ Prop) (ρ₀ : (repnFunctor (Fin 2) (AlgebraicClosure β„š ≃ₐ[β„š] AlgebraicClosure β„š) π’ͺ).obj ProartinianCat.residueField) (A : ProartinianCat π’ͺ) : (conditionSubfunctor π’ͺ π’Ÿ ρ₀).obj A = conditionLifts π’ͺ π’Ÿ ρ₀ A := rfl end GaloisRep