OriginalFiniteNormalizationDecomposition.lean

def originalFiniteNormalizationDecompositionMorphism
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F] [IsGalois K F]
    (Q : Ideal (normalizationCommAlgCat A F)) :
    GrpCat.Hom (normalizationDecompositionGroup A K F Q)
      (nativeResidueStabilizer (normalizationCommAlgCat A F)
        (normalizationCommAlgCat A F ≃ₐ[A] normalizationCommAlgCat A F) Q) where
  hom' :=
    { toFun := fun d =>
        ⟨(normalizationGaloisGroupMap A K F).hom'.toFun d.val, by
          change Q.map (normalizationGaloisRingHom A K F d.val) = Q
          rw [normalizationGaloisRingHom_eq_original]
          exact d.property⟩
      map_one' := Subtype.ext (normalizationGaloisGroupMap A K F).hom'.map_one
      map_mul' := fun d e => Subtype.ext
        ((normalizationGaloisGroupMap A K F).hom'.map_mul d.val e.val) }

theorem originalFiniteNormalizationDecompositionMorphism_value
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F] [IsGalois K F]
    (Q : Ideal (normalizationCommAlgCat A F))
    (d : normalizationDecompositionGroup A K F Q) :
    ((originalFiniteNormalizationDecompositionMorphism A K F Q).hom'.toFun d).val =
      (normalizationGaloisGroupMap A K F).hom'.toFun d.val

theorem originalFiniteNormalizationDecompositionMorphism_ringHom
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F] [IsGalois K F]
    (Q : Ideal (normalizationCommAlgCat A F))
    (d : normalizationDecompositionGroup A K F Q) :
    (stabilizerCoefficientRingEquiv (normalizationCommAlgCat A F)
        (normalizationCommAlgCat A F ≃ₐ[A] normalizationCommAlgCat A F) Q
        ((originalFiniteNormalizationDecompositionMorphism A K F Q).hom'.toFun d)).toRingHom =
      normalizationGaloisRingHom A K F d.val