CurveModel_natCard_stabilizer_pointEquivPlace_mul_natCard_ker_eq.lean

theorem semilinearAut_ext {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
    (g g' : SemilinearAut K L) (h1 : ∀ z : L, g • z = g' • z)
    (h2 : SemilinearAut.baseAut g = SemilinearAut.baseAut g') : g = g'

theorem exists_germ {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
    (M : CurveModel K L) (z : L) :
    ∃ (U : M.C.Opens) (_ : Nonempty (Scheme.Opens.toScheme U)) (f : Γ(M.C, U)),
      z = M.ffEquiv.symm (M.C.germToFunctionField U f)

theorem _root_.AlgebraicCurve.CurveModel.natCard_stabilizer_pointEquivPlace_mul_natCard_ker_eq
    {k : Type u} [Field k] [IsAlgClosed k] {L : Type v} [Field L] [Algebra k L]
    (M : CurveModel k L)
    (F : Type v) [Field F] [Algebra k F] [Algebra F L] [IsScalarTower k F L] [FiniteDimensional F L]
    (G₀ : Type u) [Group G₀] [Finite G₀] (ρ : G₀ →* Aut M.C) (hρ : ∀ g : G₀, (ρ g).hom ≫ M.toBase =
      M.toBase)
    (θ : G₀ →* (L ≃ₐ[F] L)) (hθsurj : Function.Surjective θ)
    (hθ : ∀ (g : G₀) (U : M.C.Opens) [Nonempty (Scheme.Opens.toScheme U)]
        [Nonempty (Scheme.Opens.toScheme ((ρ g).inv ⁻¹ᵁ U))] (f : Γ(M.C, U)),
        θ g (M.ffEquiv.symm (M.C.germToFunctionField U f)) =
          M.ffEquiv.symm (M.C.germToFunctionField ((ρ g).inv ⁻¹ᵁ U) ((ρ g).inv.app U f)))
    (hθker : ∀ g : G₀, θ g = 1 ↔ ρ g = 1)
    (x : {p : Spec (CommRingCat.of k) ⟶ M.C // p ≫ M.toBase = 𝟙 _}) :
    Nat.card {σ : L ≃ₐ[F] L // SemilinearAut.ofAlgAut (σ.restrictScalars k) • M.pointEquivPlace x =
      M.pointEquivPlace x} *
        Nat.card θ.ker =
      Nat.card {g : G₀ // x.1 ≫ (ρ g).hom = x.1}