Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.FunctionFieldNormalClosureOriginalCompositum

The original function field after enlarging the normal-closure constants #

Let F / K(t) be finite separable, let N be the chosen normal closure, and let C be the full algebraic constant field of N. If K is already the exact constant field of F, linear disjointness identifies the scalar extension C ⊗[K] F with its multiplication image CF inside N.

This file constructs that image as an intermediate field, equips it with the C(t)-structure inherited from the constant base inside N, and records the two structural facts needed downstream: N / CF is finite Galois and C is the exact constant field of CF.

source
@[instance_reducible]
noncomputable def BGS.HasseWeil.originalCompositumNormalClosureSMul (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
SMul K ↥(FunctionFieldNormalClosure K F)

The scalar action of K on (FunctionFieldNormalClosure K F) used in the function field normal closure original compositum construction.

Equations
Instances For
    source
    @[instance_reducible]
    noncomputable def BGS.HasseWeil.originalCompositumNormalClosureModule (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
    Module K ↥(FunctionFieldNormalClosure K F)

    The module structure of (FunctionFieldNormalClosure K F) over K used in the function field normal closure original compositum construction.

    Equations
    Instances For
      source
      theorem BGS.HasseWeil.originalCompositumNormalClosureSelfTower (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
      IsScalarTower K K ↥(FunctionFieldNormalClosure K F)
      source
      @[instance_reducible]
      noncomputable def BGS.HasseWeil.originalCompositumBaseConstantSMul (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
      SMul K ↥(FunctionFieldNormalClosureConstantField K F)

      The scalar action of K on (FunctionFieldNormalClosureConstantField K F) used in the function field normal closure original compositum construction.

      Equations
      Instances For
        source
        @[instance_reducible]
        noncomputable def BGS.HasseWeil.originalCompositumBaseConstantModule (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
        Module K ↥(FunctionFieldNormalClosureConstantField K F)

        The module structure of (FunctionFieldNormalClosureConstantField K F) over K used in the function field normal closure original compositum construction.

        Equations
        Instances For
          source
          @[instance_reducible]
          noncomputable def BGS.HasseWeil.originalCompositumConstantBaseSMul (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
          SMul ↥(FunctionFieldNormalClosureConstantField K F) ↥(FunctionFieldNormalClosureConstantBase K F)

          The scalar action of (FunctionFieldNormalClosureConstantField K F) on (FunctionFieldNormalClosureConstantBase K F) used in the function field normal closure original compositum construction.

          Equations
          Instances For
            source
            @[instance_reducible]
            noncomputable def BGS.HasseWeil.originalCompositumConstantBaseModule (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
            Module ↥(FunctionFieldNormalClosureConstantField K F) ↥(FunctionFieldNormalClosureConstantBase K F)

            The module structure of (FunctionFieldNormalClosureConstantBase K F) over (FunctionFieldNormalClosureConstantField K F) used in the function field normal closure original compositum construction.

            Equations
            Instances For
              source
              noncomputable def BGS.HasseWeil.functionFieldNormalClosureOriginalMultiplication (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
              ExactConstantExtension K F ↥(FunctionFieldNormalClosureConstantField K F) →ₐ[K] ↥(FunctionFieldNormalClosure K F)

              Multiplication of the two embedded factors C and F inside the normal closure. Before exactness is imposed this is merely an algebra homomorphism from the tensor product; exactness will make its source a field and hence the map injective.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem BGS.HasseWeil.functionFieldNormalClosureOriginalMultiplication_tmul (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (c : ↥(FunctionFieldNormalClosureConstantField K F)) (x : F) :
                (functionFieldNormalClosureOriginalMultiplication K F) (c ⊗ₜ[K] x) = ↑c * (functionFieldToNormalClosure K F) x
                source
                noncomputable def BGS.HasseWeil.FunctionFieldNormalClosureOriginalCompositum (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) :
                IntermediateField K ↥(FunctionFieldNormalClosure K F)

                The compositum CF inside the chosen normal closure, realized as the field range of tensor multiplication.

                Equations
                Instances For
                  source
                  noncomputable def BGS.HasseWeil.exactConstantExtensionOriginalCompositumAlgEquiv (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) :
                  ExactConstantExtension K F ↥(FunctionFieldNormalClosureConstantField K F) ≃ₐ[K] ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact)

                  Tensor scalar extension is the same field as the compositum CF inside the normal closure.

                  Equations
                  Instances For
                    source
                    theorem BGS.HasseWeil.functionFieldNormalClosureConstant_mem_originalCompositum (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) (c : ↥(FunctionFieldNormalClosureConstantField K F)) :
                    ↑c ∈ FunctionFieldNormalClosureOriginalCompositum K F hExact

                    Every algebraic constant of the normal closure belongs to CF.

                    source
                    theorem BGS.HasseWeil.functionFieldNormalClosureRatFunc_mem_originalCompositum (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) (r : RatFunc K) :
                    (algebraMap (RatFunc K) ↥(FunctionFieldNormalClosure K F)) r ∈ FunctionFieldNormalClosureOriginalCompositum K F hExact

                    The original rational-function field belongs to CF.

                    source
                    noncomputable def BGS.HasseWeil.functionFieldNormalClosureConstantToOriginalCompositum (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) :
                    ↥(FunctionFieldNormalClosureConstantField K F) →ₐ[K] ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact)

                    The inclusion of the full constant field into CF.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[reducible]
                      noncomputable instance BGS.HasseWeil.functionFieldNormalClosureOriginalCompositumConstantAlgebra (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) :
                      Algebra ↥(FunctionFieldNormalClosureConstantField K F) ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact)

                      The compositum is naturally an algebra over the full constant field.

                      Equations
                      source
                      @[instance_reducible]
                      noncomputable def BGS.HasseWeil.originalCompositumConstantSMul (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) :
                      SMul ↥(FunctionFieldNormalClosureConstantField K F) ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact)

                      The constant-field scalar action on the original compositum.

                      Equations
                      Instances For
                        source
                        @[instance_reducible]
                        noncomputable def BGS.HasseWeil.originalCompositumConstantModule (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) :
                        Module ↥(FunctionFieldNormalClosureConstantField K F) ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact)

                        The corresponding module structure on the original compositum.

                        Equations
                        Instances For
                          source
                          noncomputable def BGS.HasseWeil.exactConstantExtensionOriginalCompositumConstantAlgEquiv (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) :
                          have this := exactConstantExtensionField K F (↥(FunctionFieldNormalClosureConstantField K F)) hExact; have this := Algebra.TensorProduct.leftAlgebra; ExactConstantExtension K F ↥(FunctionFieldNormalClosureConstantField K F) ≃ₐ[↥(FunctionFieldNormalClosureConstantField K F)] ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact)

                          The tensor/compositum equivalence respects the enlarged constants.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            instance BGS.HasseWeil.functionFieldNormalClosureOriginalCompositumConstantTower (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) :
                            IsScalarTower ↥(FunctionFieldNormalClosureConstantField K F) ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact) ↥(FunctionFieldNormalClosure K F)

                            The constant embedding into CF agrees with its embedding into N.

                            source
                            noncomputable def BGS.HasseWeil.functionFieldNormalClosureRatFuncToOriginalCompositum (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) :
                            RatFunc K →ₐ[K] ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact)

                            The inclusion of K(t) into CF.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              @[reducible]
                              noncomputable instance BGS.HasseWeil.functionFieldNormalClosureOriginalCompositumRatFuncAlgebra (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) :
                              Algebra (RatFunc K) ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact)

                              The compositum is naturally a K(t)-algebra.

                              Equations
                              source
                              instance BGS.HasseWeil.functionFieldNormalClosureOriginalCompositumRatFuncTower (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) :
                              IsScalarTower (RatFunc K) ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact) ↥(FunctionFieldNormalClosure K F)

                              The K(t) embedding into CF agrees with its embedding into N.

                              source
                              theorem BGS.HasseWeil.functionFieldNormalClosureConstantBase_le_originalCompositum (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) (b : ↥(FunctionFieldNormalClosureConstantBase K F)) :
                              ↑b ∈ FunctionFieldNormalClosureOriginalCompositum K F hExact

                              The constant base C(t) inside N is contained in the larger compositum CF.

                              source
                              noncomputable def BGS.HasseWeil.functionFieldNormalClosureConstantBaseToOriginalCompositum (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) :
                              ↥(FunctionFieldNormalClosureConstantBase K F) →ₐ[↥(FunctionFieldNormalClosureConstantField K F)] ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact)

                              Inclusion of the constant base C(t) into CF, linear over C.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                @[reducible, instance 2000]
                                noncomputable instance BGS.HasseWeil.functionFieldNormalClosureConstantFieldRatFuncAlgebraForOriginalCompositum (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
                                Algebra (↥(FunctionFieldNormalClosureConstantField K F)) (RatFunc ↥(FunctionFieldNormalClosureConstantField K F))

                                The standard coefficient algebra structure on C(t) used by the rational-function equivalence.

                                Equations
                                source
                                noncomputable def BGS.HasseWeil.functionFieldNormalClosureOriginalCompositumConstantRatFuncAlgHom (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) :
                                RatFunc ↥(FunctionFieldNormalClosureConstantField K F) →ₐ[↥(FunctionFieldNormalClosureConstantField K F)] ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact)

                                The C(t)-algebra structure on CF, transported through the canonical equivalence C(t) ≃ C K(t) inside the normal closure.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  @[reducible]
                                  noncomputable instance BGS.HasseWeil.functionFieldNormalClosureOriginalCompositumConstantRatFuncAlgebra (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) :
                                  Algebra (RatFunc ↥(FunctionFieldNormalClosureConstantField K F)) ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact)

                                  CF as an algebra over the enlarged rational-function field C(t).

                                  Equations
                                  source
                                  instance BGS.HasseWeil.functionFieldNormalClosureOriginalCompositumBaseConstantTower (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) :
                                  IsScalarTower K ↥(FunctionFieldNormalClosureConstantField K F) ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact)

                                  The two embeddings of K into CF, directly and through C, agree.

                                  source
                                  instance BGS.HasseWeil.functionFieldNormalClosure_finiteDimensional_over_originalCompositum (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) :
                                  FiniteDimensional ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact) ↥(FunctionFieldNormalClosure K F)

                                  The chosen normal closure is finite over the original compositum CF.

                                  source
                                  instance BGS.HasseWeil.functionFieldNormalClosure_isGalois_over_originalCompositum (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) :
                                  IsGalois ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact) ↥(FunctionFieldNormalClosure K F)

                                  The chosen normal closure remains Galois after enlarging the base from K(t) to the intermediate field CF.

                                  source
                                  theorem BGS.HasseWeil.functionFieldNormalClosureOriginalCompositumConstantField_isExact (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) :
                                  algebraicClosure ↥(FunctionFieldNormalClosureConstantField K F) ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact) = ⊥

                                  Enlarging the original function field to CF introduces exactly the constants C and no others.

                                  source
                                  @[reducible]
                                  noncomputable def BGS.HasseWeil.functionFieldCanonicalConstantAlgebra (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] :
                                  Algebra K F

                                  The constant algebra on F obtained by restricting the given K(t)-algebra. This named definition is useful when applying constructions whose constant algebra is definitionally this restriction.

                                  Equations
                                  Instances For
                                    source
                                    noncomputable def BGS.HasseWeil.exactConstantExtensionOriginalCompositumCanonicalRatFuncAlgEquiv (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
                                    let this := functionFieldCanonicalConstantAlgebra K F; have this_1 := ⋯; (hExact : algebraicClosure K F = ⊥) → let C := FunctionFieldNormalClosureConstantField K F; let E := ExactConstantExtension K F ↥C; let M := FunctionFieldNormalClosureOriginalCompositum K F hExact; have this_2 := exactConstantExtensionField K F (↥C) hExact; have this_3 := Algebra.TensorProduct.leftAlgebra; have this_4 := ratFuncExactConstantExtensionAlgebra K (↥C) F hExact; E ≃ₐ[RatFunc ↥C] ↥M

                                    For the canonical restricted constant algebra, the tensor/compositum equivalence is linear over C(t), not merely over K.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For