LeanPool.BrauerGroupNew.ToSecond #
Imported Lean Pool material for LeanPool.BrauerGroupNew.ToSecond.
structure
GoodRep
{F : Type}
(K : Type)
[Field K]
[Field F]
[Algebra F K]
(X : BrauerGroup F)
extends CSA F :
Type 1
A relative Brauer class representative with a splitting-field embedding.
- isCentral : Algebra.IsCentral F ↑self.toAlgCat
- isSimple : IsSimpleRing ↑self.toAlgCat
- fin_dim : FiniteDimensional F ↑self.toAlgCat
The underlying central simple algebra represents the chosen Brauer class.
The chosen algebra embedding of the splitting field into the representative.
The representative has the expected square dimension over the base field.
Instances For
@[instance_reducible]
noncomputable instance
GoodRep.instAlgebraCarrier
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
(A : GoodRep K X)
:
Equations
instance
GoodRep.instIsSimpleOrderTwoSidedIdealSubtypeCarrierMemSubalgebraRangeι
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
(A : GoodRep K X)
:
IsSimpleOrder (TwoSidedIdeal ↥A.ι.range)
theorem
GoodRep.centralizerιRange
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
(A : GoodRep K X)
:
@[instance_reducible]
noncomputable instance
GoodRep.instModuleCarrier
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
(A : GoodRep K X)
:
Equations
- A.instModuleCarrier = A.ι.toModule
instance
GoodRep.instFiniteDimensionalCarrier
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
(A : GoodRep K X)
:
instance
GoodRep.instIsScalarTowerCarrier
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
(A : GoodRep K X)
:
IsScalarTower F K ↑A.toAlgCat
instance
GoodRep.instFiniteDimensionalCarrier_1
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
(A : GoodRep K X)
:
theorem
GoodRep.dim_eq'
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
(A : GoodRep K X)
[FiniteDimensional F K]
:
noncomputable def
GoodRep.conjFactor
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
(A : GoodRep K X)
(σ : Gal(K/F))
:
A unit implementing the Galois action by conjugation on the embedded splitting field.
Instances For
noncomputable def
GoodRep.arbitraryConjFactor
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
(A : GoodRep K X)
(σ : Gal(K/F))
:
A.conjFactor σ
A chosen conjugating unit for each Galois automorphism, supplied by Skolem-Noether.
Equations
- A.arbitraryConjFactor σ = ⟨⋯.choose, ⋯⟩
Instances For
@[simp]
theorem
GoodRep.conjFactor_prop
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ : Gal(K/F)}
(x : A.conjFactor σ)
(c : K)
:
noncomputable def
GoodRep.mul'
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ τ : Gal(K/F)}
(x : A.conjFactor σ)
(y : A.conjFactor τ)
:
A.conjFactor (σ * τ)
The product of two conjugating units as a conjugating unit for the product automorphism.
Equations
- GoodRep.mul' x y = ⟨↑x * ↑y, ⋯⟩
Instances For
@[simp]
theorem
GoodRep.mul'_coe
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ τ : Gal(K/F)}
(x : A.conjFactor σ)
(y : A.conjFactor τ)
:
theorem
GoodRep.conjFactor_rel_aux
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ : Gal(K/F)}
(x y : A.conjFactor σ)
:
theorem
GoodRep.conjFactor_rel
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ : Gal(K/F)}
(x y : A.conjFactor σ)
:
noncomputable def
GoodRep.conjFactorTwistCoeff
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ : Gal(K/F)}
(x y : A.conjFactor σ)
:
K
The scalar comparing two conjugating units for the same automorphism.
Equations
Instances For
theorem
GoodRep.conjFactorTwistCoeff_spec
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ : Gal(K/F)}
(x y : A.conjFactor σ)
:
theorem
GoodRep.conjFactorTwistCoeff_unique
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ : Gal(K/F)}
(x y : A.conjFactor σ)
(c : K)
(h : ↑↑x = ↑↑y * A.ι c)
:
@[simp]
theorem
GoodRep.conjFactorTwistCoeff_self
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ : Gal(K/F)}
(x : A.conjFactor σ)
:
noncomputable def
GoodRep.conjFactorTwistCoeffAsUnit
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ : Gal(K/F)}
(x y : A.conjFactor σ)
:
Kˣ
The twist coefficient packaged as a unit.
Equations
- GoodRep.conjFactorTwistCoeffAsUnit x y = { val := GoodRep.conjFactorTwistCoeff x y, inv := GoodRep.conjFactorTwistCoeff y x, val_inv := ⋯, inv_val := ⋯ }
Instances For
theorem
GoodRep.val_inv_conjFactorTwistCoeffAsUnit
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ : Gal(K/F)}
(x y : A.conjFactor σ)
:
theorem
GoodRep.val_conjFactorTwistCoeffAsUnit
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ : Gal(K/F)}
(x y : A.conjFactor σ)
:
@[simp]
theorem
GoodRep.conjFactorTwistCoeff_swap
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ : Gal(K/F)}
(x y : A.conjFactor σ)
:
theorem
GoodRep.conjFactorTwistCoeff_inv
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ : Gal(K/F)}
(x y : A.conjFactor σ)
:
theorem
GoodRep.conjFactorTwistCoeff_swap'
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ : Gal(K/F)}
(x y : A.conjFactor σ)
:
@[simp]
theorem
GoodRep.conjFactorTwistCoeff_swap''
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ : Gal(K/F)}
(x y : A.conjFactor σ)
:
theorem
GoodRep.conjFactorTwistCoeff_swap'''
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ : Gal(K/F)}
(x y : A.conjFactor σ)
:
theorem
GoodRep.conjFactorTwistCoeff_spec'
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ : Gal(K/F)}
(x y : A.conjFactor σ)
:
noncomputable def
GoodRep.conjFactorCompCoeff
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ τ : Gal(K/F)}
(x : A.conjFactor σ)
(y : A.conjFactor τ)
(z : A.conjFactor (σ * τ))
:
K
The scalar measuring the defect of the chosen conjugating units from being multiplicative.
Equations
- GoodRep.conjFactorCompCoeff x y z = σ (τ (GoodRep.conjFactorTwistCoeff (GoodRep.mul' x y) z))
Instances For
noncomputable def
GoodRep.conjFactorCompCoeffAsUnit
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ τ : Gal(K/F)}
(x : A.conjFactor σ)
(y : A.conjFactor τ)
(z : A.conjFactor (σ * τ))
:
Kˣ
The composition coefficient packaged as a unit.
Equations
- GoodRep.conjFactorCompCoeffAsUnit x y z = { val := GoodRep.conjFactorCompCoeff x y z, inv := σ (τ (GoodRep.conjFactorTwistCoeff z (GoodRep.mul' x y))), val_inv := ⋯, inv_val := ⋯ }
Instances For
theorem
GoodRep.val_conjFactorCompCoeffAsUnit
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ τ : Gal(K/F)}
(x : A.conjFactor σ)
(y : A.conjFactor τ)
(z : A.conjFactor (σ * τ))
:
theorem
GoodRep.val_inv_conjFactorCompCoeffAsUnit
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ τ : Gal(K/F)}
(x : A.conjFactor σ)
(y : A.conjFactor τ)
(z : A.conjFactor (σ * τ))
:
theorem
GoodRep.conjFactorCompCoeff_spec
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ τ : Gal(K/F)}
(x : A.conjFactor σ)
(y : A.conjFactor τ)
(z : A.conjFactor (σ * τ))
:
theorem
GoodRep.conjFactorCompCoeff_spec'_
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ τ : Gal(K/F)}
(x : A.conjFactor σ)
(y : A.conjFactor τ)
(z : A.conjFactor (σ * τ))
:
theorem
GoodRep.conjFactorCompCoeff_spec'
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ τ : Gal(K/F)}
(x : A.conjFactor σ)
(y : A.conjFactor τ)
(z : A.conjFactor (σ * τ))
:
theorem
GoodRep.conjFactorCompCoeff_spec''
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ τ : Gal(K/F)}
(x : A.conjFactor σ)
(y : A.conjFactor τ)
(z : A.conjFactor (σ * τ))
:
theorem
GoodRep.conjFactorCompCoeff_inv
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ τ : Gal(K/F)}
(x : A.conjFactor σ)
(y : A.conjFactor τ)
(z : A.conjFactor (σ * τ))
:
theorem
GoodRep.conjFactorCompCoeff_comp_comp₁
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{ρ σ τ : Gal(K/F)}
(xρ : A.conjFactor ρ)
(xσ : A.conjFactor σ)
(xτ : A.conjFactor τ)
(xρσ : A.conjFactor (ρ * σ))
(xρστ : A.conjFactor (ρ * σ * τ))
:
↑↑xρ * ↑↑xσ * ↑↑xτ = A.ι (conjFactorCompCoeff xρ xσ xρσ) * A.ι (conjFactorCompCoeff xρσ xτ xρστ) * ↑↑xρστ
theorem
GoodRep.conjFactorCompCoeff_eq
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{σ τ : Gal(K/F)}
(x : A.conjFactor σ)
(y : A.conjFactor τ)
(z : A.conjFactor (σ * τ))
:
theorem
GoodRep.conjFactorCompCoeff_comp_comp₂
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{ρ σ τ : Gal(K/F)}
(xρ : A.conjFactor ρ)
(xσ : A.conjFactor σ)
(xτ : A.conjFactor τ)
(xστ : A.conjFactor (σ * τ))
(xρστ : A.conjFactor (ρ * σ * τ))
:
↑↑xρ * (↑↑xσ * ↑↑xτ) = A.ι (ρ (conjFactorCompCoeff xσ xτ xστ)) * A.ι (conjFactorCompCoeff xρ xστ xρστ) * ↑↑xρστ
theorem
GoodRep.conjFactorCompCoeff_comp_comp₃
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{ρ σ τ : Gal(K/F)}
(xρ : A.conjFactor ρ)
(xσ : A.conjFactor σ)
(xτ : A.conjFactor τ)
(xρσ : A.conjFactor (ρ * σ))
(xστ : A.conjFactor (σ * τ))
(xρστ : A.conjFactor (ρ * σ * τ))
:
A.ι (conjFactorCompCoeff xρ xσ xρσ) * A.ι (conjFactorCompCoeff xρσ xτ xρστ) * ↑↑xρστ = A.ι (ρ (conjFactorCompCoeff xσ xτ xστ)) * A.ι (conjFactorCompCoeff xρ xστ xρστ) * ↑↑xρστ
theorem
GoodRep.conjFactorCompCoeff_comp_comp
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
{ρ σ τ : Gal(K/F)}
(xρ : A.conjFactor ρ)
(xσ : A.conjFactor σ)
(xτ : A.conjFactor τ)
(xρσ : A.conjFactor (ρ * σ))
(xστ : A.conjFactor (σ * τ))
(xρστ : A.conjFactor (ρ * σ * τ))
:
conjFactorCompCoeff xρ xσ xρσ * conjFactorCompCoeff xρσ xτ xρστ = ρ (conjFactorCompCoeff xσ xτ xστ) * conjFactorCompCoeff xρ xστ xρστ
noncomputable def
GoodRep.toCocycles₂
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
(A : GoodRep K X)
(x_ : (σ : Gal(K/F)) → A.conjFactor σ)
:
The two-cocycle associated to a system of conjugating units.
Equations
- A.toCocycles₂ x_ p = GoodRep.conjFactorCompCoeffAsUnit (x_ p.1) (x_ p.2) (x_ (p.1 * p.2))
Instances For
theorem
GoodRep.toCocycles₂_cond
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
(ρ σ τ : Gal(K/F))
(x_ : (σ : Gal(K/F)) → A.conjFactor σ)
:
theorem
GoodRep.isMulCocycle₂
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
(x_ : (σ : Gal(K/F)) → A.conjFactor σ)
:
noncomputable def
GoodRep.isoConjCoeff
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
(B : GoodRep K X)
:
The unit conjugating the transported splitting-field embedding to the target embedding.
Equations
Instances For
theorem
GoodRep.isoConjCoeff_spec
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
(B : GoodRep K X)
(r : K)
:
theorem
GoodRep.isoConjCoeff_spec'
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
(B : GoodRep K X)
(r : K)
:
theorem
GoodRep.isoConjCoeff_spec''
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
(B : GoodRep K X)
{σ : Gal(K/F)}
(c : K)
(x : A.conjFactor σ)
:
B.ι (σ c) = ↑(isoConjCoeff B) * (iso B) ↑↑x * ↑(isoConjCoeff B)⁻¹ * B.ι c * (↑(isoConjCoeff B) * (iso B) ↑(↑x)⁻¹ * ↑(isoConjCoeff B)⁻¹)
noncomputable def
GoodRep.pushConjFactor
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
(B : GoodRep K X)
{σ : Gal(K/F)}
(x : A.conjFactor σ)
:
B.conjFactor σ
Transport a conjugating unit across the chosen algebra equivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
GoodRep.pushConjFactor_coe
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
(B : GoodRep K X)
{σ : Gal(K/F)}
(x : A.conjFactor σ)
:
noncomputable def
GoodRep.pushConjFactorCoeff
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
(B : GoodRep K X)
{σ : Gal(K/F)}
(x : A.conjFactor σ)
(y : B.conjFactor σ)
:
K
The scalar comparing a transported conjugating unit with a chosen target unit.
Equations
- GoodRep.pushConjFactorCoeff B x y = σ (GoodRep.conjFactorTwistCoeff y (GoodRep.pushConjFactor B x))
Instances For
theorem
GoodRep.pushConjFactorCoeff_spec
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
(B : GoodRep K X)
{σ : Gal(K/F)}
(x : A.conjFactor σ)
(y : B.conjFactor σ)
:
theorem
GoodRep.pushConjFactorCoeff_spec'
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
(B : GoodRep K X)
{σ : Gal(K/F)}
(x : A.conjFactor σ)
(y : B.conjFactor σ)
:
B.ι (pushConjFactorCoeff B x y) = ↑(isoConjCoeff B) * (iso B) (A.ι (pushConjFactorCoeff B x y)) * ↑(isoConjCoeff B)⁻¹
@[reducible, inline]
noncomputable abbrev
GoodRep.pushConjFactorCoeffAsUnit
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
(B : GoodRep K X)
{σ : Gal(K/F)}
(x : A.conjFactor σ)
(y : B.conjFactor σ)
:
Kˣ
The transported-unit comparison scalar packaged as a unit.
Equations
- GoodRep.pushConjFactorCoeffAsUnit B x y = { val := GoodRep.pushConjFactorCoeff B x y, inv := σ (GoodRep.conjFactorTwistCoeff (GoodRep.pushConjFactor B x) y), val_inv := ⋯, inv_val := ⋯ }
Instances For
@[simp]
theorem
GoodRep.val_inv_pushConjFactorCoeffAsUnit
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
(B : GoodRep K X)
{σ : Gal(K/F)}
(x : A.conjFactor σ)
(y : B.conjFactor σ)
:
@[simp]
theorem
GoodRep.val_pushConjFactorCoeffAsUnit
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
(B : GoodRep K X)
{σ : Gal(K/F)}
(x : A.conjFactor σ)
(y : B.conjFactor σ)
:
theorem
GoodRep.compare_conjFactorCompCoeff
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
(B : GoodRep K X)
{σ τ : Gal(K/F)}
(xσ : A.conjFactor σ)
(yσ : B.conjFactor σ)
(xτ : A.conjFactor τ)
(yτ : B.conjFactor τ)
(xστ : A.conjFactor (σ * τ))
(yστ : B.conjFactor (σ * τ))
:
conjFactorCompCoeff yσ yτ yστ * pushConjFactorCoeff B xστ yστ = pushConjFactorCoeff B xσ yσ * σ (pushConjFactorCoeff B xτ yτ) * conjFactorCompCoeff xσ xτ xστ
noncomputable def
GoodRep.trivialFactorSet
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
(c : Gal(K/F) → Kˣ)
:
The multiplicative two-coboundary associated to a one-cochain.
Equations
- GoodRep.trivialFactorSet c p = c p.1 * (Units.map ↑p.1.toRingEquiv.toRingHom) (c p.2) * (c (p.1 * p.2))⁻¹
Instances For
theorem
GoodRep.compare_toCocycles₂
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
(B : GoodRep K X)
{σ τ : Gal(K/F)}
(x_ : (σ : Gal(K/F)) → A.conjFactor σ)
(y_ : (σ : Gal(K/F)) → B.conjFactor σ)
:
B.toCocycles₂ y_ (σ, τ) * pushConjFactorCoeffAsUnit B (x_ (σ * τ)) (y_ (σ * τ)) = pushConjFactorCoeffAsUnit B (x_ σ) (y_ σ) * (Units.map ↑σ) (pushConjFactorCoeffAsUnit B (x_ τ) (y_ τ)) * A.toCocycles₂ x_ (σ, τ)
theorem
GoodRep.compare_toCocycles₂'
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
{A : GoodRep K X}
(B : GoodRep K X)
(x_ : (σ : Gal(K/F)) → A.conjFactor σ)
(y_ : (σ : Gal(K/F)) → B.conjFactor σ)
:
groupCohomology.IsMulCoboundary₂ (B.toCocycles₂ y_ / A.toCocycles₂ x_)
noncomputable def
Amelia.toAdditive
(M G : Type)
[Monoid M]
[CommGroup G]
[MulDistribMulAction M G]
:
The additive form of a multiplicative-distribution representation.
Equations
- Amelia.toAdditive M G = AddEquiv.refl ↑(Rep.ofMulDistribMulAction M G)
Instances For
@[simp]
theorem
Amelia.toAdditive_symm_apply
(M G : Type)
[Monoid M]
[CommGroup G]
[MulDistribMulAction M G]
(a : ↑(Rep.ofMulDistribMulAction M G))
:
@[simp]
theorem
Amelia.toAdditive_apply
(M G : Type)
[Monoid M]
[CommGroup G]
[MulDistribMulAction M G]
(a : ↑(Rep.ofMulDistribMulAction M G))
:
theorem
mem_relativeBrGroup_iff_nonempty_goodRep
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
[FiniteDimensional F K]
{X : BrauerGroup F}
:
noncomputable def
RelativeBrGroup.goodRep
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
[FiniteDimensional F K]
(X : ↥(RelativeBrGroup K F))
:
GoodRep K ↑X
Choose a good representative for an element of the relative Brauer group.
Equations
Instances For
noncomputable def
GoodRep.toH2
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
(A : GoodRep K X)
(x_ : (σ : Gal(K/F)) → A.conjFactor σ)
:
↑(groupCohomology.H2 (galAct F K))
The cohomology class attached to a good representative and a system of conjugating units.
Equations
Instances For
noncomputable def
RelativeBrGroup.toSnd
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
[FiniteDimensional F K]
:
↥(RelativeBrGroup K F) → ↑(groupCohomology.H2 (galAct F K))
Send a relative Brauer class to its degree-two Galois cohomology class.
Equations
Instances For
theorem
RelativeBrGroup.toSnd_wd
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
[FiniteDimensional F K]
(X : ↥(RelativeBrGroup K F))
(A : GoodRep K ↑X)
(x_ : (σ : Gal(K/F)) → A.conjFactor σ)
:
theorem
GoodRep.conjFactor_linearIndependent
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
{X : BrauerGroup F}
(A : GoodRep K X)
(x_ : (σ : Gal(K/F)) → A.conjFactor σ)
:
LinearIndependent K fun (i : Gal(K/F)) => ↑↑(x_ i)
noncomputable def
GoodRep.conjFactorBasis
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
[FiniteDimensional F K]
{X : BrauerGroup F}
(A : GoodRep K X)
[IsGalois F K]
(x_ : (σ : Gal(K/F)) → A.conjFactor σ)
:
Module.Basis Gal(K/F) K ↑A.toAlgCat
The basis of a good representative obtained from conjugating units.
Equations
Instances For
noncomputable def
RelativeBrGroup.fromCocycles₂
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
[FiniteDimensional F K]
[IsGalois F K]
(f : ↥(groupCohomology.cocycles₂ (galAct F K)))
:
↥(RelativeBrGroup K F)
Build a relative Brauer class from a two-cocycle via the cross-product algebra.
Equations
Instances For
noncomputable def
RelativeBrGroup.fromSnd
(F K : Type)
[Field K]
[Field F]
[Algebra F K]
[FiniteDimensional F K]
[IsGalois F K]
:
↑(groupCohomology.shortComplexH2 (galAct F K)).moduleCatLeftHomologyData.H → ↥(RelativeBrGroup K F)
Descend the cross-product construction to second cohomology.
Equations
Instances For
theorem
RelativeBrGroup.fromSnd_wd
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
[FiniteDimensional F K]
[IsGalois F K]
(a : ↥(groupCohomology.cocycles₂ (galAct F K)))
:
fromSnd F K (Quotient.mk'' a) = ⟨Quotient.mk'' (CrossProductAlgebra.asCSA (⇑Additive.toMul ∘ ⇑a)), ⋯⟩
noncomputable def
Amfix.coboundariesOfIsMulCoboundary₂
{G M : Type}
[Group G]
[CommGroup M]
[MulDistribMulAction G M]
{f : G × G → M}
(hf : groupCohomology.IsMulCoboundary₂ f)
:
Convert a multiplicative two-coboundary witness into an additive cohomology coboundary.
Equations
Instances For
theorem
RelativeBrGroup.toSnd_fromSnd
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
[FiniteDimensional F K]
[IsGalois F K]
:
toSnd ∘ fromSnd F K ∘ ⇑(CategoryTheory.ConcreteCategory.hom (groupCohomology.H2Iso (galAct F K)).hom) = id
theorem
RelativeBrGroup.fromSnd_toSnd
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
[FiniteDimensional F K]
[IsGalois F K]
:
(fromSnd F K ∘ ⇑(CategoryTheory.ConcreteCategory.hom (groupCohomology.H2Iso (galAct F K)).hom)) ∘ toSnd = id
noncomputable def
RelativeBrGroup.equivSnd
{F K : Type}
[Field K]
[Field F]
[Algebra F K]
[FiniteDimensional F K]
[IsGalois F K]
:
The equivalence between the relative Brauer group and second Galois cohomology.
Equations
- One or more equations did not get rendered due to their size.